Porting note: removed `@[ext]`

[pitmonticone]

Classifies porting notes claiming:

removed @[ext]

Links

• Porting note: ext does not look through definitions, so we need more ext lemmas #5229: categorises adding ext lemmas.
• Porting note: broken ext #11041: categorises other failures of ext.

Examples

mathlib4/Mathlib/CategoryTheory/Subobject/Basic.lean

Lines 288 to 310 in 2a65c8d

	-- Porting note: removed @[ext]
	/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
	the arrows. -/
	theorem eq_mk_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : (X : C) ≅ A)
	(w : i.hom ≫ f = X.arrow) : X = mk f :=
	eq_of_comm (i.trans (underlyingIso f).symm) <| by simp [w]
	#align category_theory.subobject.eq_mk_of_comm CategoryTheory.Subobject.eq_mk_of_comm
	-- Porting note: removed @[ext]
	/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
	the arrows. -/
	theorem mk_eq_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : A ≅ (X : C))
	(w : i.hom ≫ X.arrow = f) : mk f = X :=
	Eq.symm <| eq_mk_of_comm _ i.symm <| by rw [Iso.symm_hom, Iso.inv_comp_eq, w]
	#align category_theory.subobject.mk_eq_of_comm CategoryTheory.Subobject.mk_eq_of_comm
	-- Porting note: removed @[ext]
	/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
	the arrows. -/
	theorem mk_eq_mk_of_comm {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B) [Mono f] [Mono g] (i : A₁ ≅ A₂)
	(w : i.hom ≫ g = f) : mk f = mk g :=
	eq_mk_of_comm _ ((underlyingIso f).trans i) <| by simp [w]
	#align category_theory.subobject.mk_eq_mk_of_comm CategoryTheory.Subobject.mk_eq_mk_of_comm