From b5976308db991f3b87743accc444e61a093d876a Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Mon, 20 Apr 2026 09:57:40 +0000 Subject: [PATCH] feat(Logic/Equiv/Defs): add coe_ofBijective simp lemma --- Mathlib/Logic/Equiv/Defs.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean index 199ebcf10c5c2c..097ab048b88779 100644 --- a/Mathlib/Logic/Equiv/Defs.lean +++ b/Mathlib/Logic/Equiv/Defs.lean @@ -818,6 +818,8 @@ noncomputable def ofBijective (f : α → β) (hf : Bijective f) : α ≃ β whe left_inv := leftInverse_surjInv hf right_inv := rightInverse_surjInv _ +@[simp] lemma coe_ofBijective (f : α → β) (hf : Bijective f) : ⇑(ofBijective f hf) = f := rfl + lemma ofBijective_apply_symm_apply (f : α → β) (hf : Bijective f) (x : β) : f ((ofBijective f hf).symm x) = x := (ofBijective f hf).apply_symm_apply x