Porting note: broken ext

[pitmonticone]

Classifies porting notes claiming anything equivalent to:

• "broken ext"
• "was ext"
• "used to be ext"
• "ext fails"
• "was ext in lean 3"

Links

• Porting note: removed @[ext] #11182: categorises removed @[ext].
• Porting note: ext does not look through definitions, so we need more ext lemmas #5229: categorises adding ext lemmas.

Examples

mathlib4/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

Lines 186 to 216 in f5e8fa1

	-- In fact, it's strong monoidal, but we don't yet have a typeclass for that.
	/-- The free R-module functor is lax monoidal. -/
	@[simps]
	instance : LaxMonoidal.{u} (free R).obj := .ofTensorHom
	-- Send `R` to `PUnit →₀ R`
	(ε := ε R)
	-- Send `(α →₀ R) ⊗ (β →₀ R)` to `α × β →₀ R`
	(μ := fun X Y => (μ R X Y).hom)
	(μ_natural := fun {_} {_} {_} {_} f g ↦ μ_natural R f g)
	(left_unitality := left_unitality R)
	(right_unitality := right_unitality R)
	(associativity := associativity R)
	instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
	refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩
	· -- Porting note: broken ext
	apply LinearMap.ext_ring
	-- Porting note (#10959): simp used to be able to close this goal
	dsimp
	erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply,
	Finsupp.single_eq_same, id_apply]
	· -- Porting note: broken ext
	apply Finsupp.lhom_ext'
	intro ⟨⟩
	apply LinearMap.ext_ring
	apply Finsupp.ext
	intro ⟨⟩
	-- Porting note (#10959): simp used to be able to close this goal
	dsimp
	erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply,
	Finsupp.single_eq_same]

mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Lines 179 to 191 in f5e8fa1

	theorem rightUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
	tensorHom f (𝟙 (ModuleCat.of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f := by
	-- Porting note: broken ext
	apply TensorProduct.ext
	apply LinearMap.ext; intro x
	apply LinearMap.ext_ring
	-- Porting note (#10934): used to be dsimp
	change ((rightUnitor N).hom) ((tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] (1 : R))) =
	f (((rightUnitor M).hom) (x ⊗ₜ[R] 1))
	erw [TensorProduct.rid_tmul, TensorProduct.rid_tmul]
	rw [LinearMap.map_smul]
	rfl
	#align Module.monoidal_category.right_unitor_naturality ModuleCat.MonoidalCategory.rightUnitor_naturality