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