chore: fix some @[ext] attribute

Mathlib/Algebra/Order/Interval.lean

@@ -517,7 +517,7 @@ variable [OrderedCommGroup α] {s t : NonemptyInterval α}
 @[to_additive]
 protected theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1 := by
   refine' ⟨fun h => _, _⟩
-  · rw [ext_iff, Prod.ext_iff] at h
+  · rw [NonemptyInterval.ext_iff, Prod.ext_iff] at h
     have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le
     refine' ⟨s.fst, t.fst, _, _, h.1⟩ <;> apply NonemptyInterval.ext <;> dsimp [pure]
     · nth_rw 2 [this.1]

Mathlib/Data/Matrix/Basic.lean

@@ -74,29 +74,11 @@ theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N :=
   ⟨fun h => funext fun i => funext <| h i, fun h => by simp [h]⟩
 #align matrix.ext_iff Matrix.ext_iff
 
--- Porting note: `ext` does not like this, see new lemma below.
--- @[ext]
+@[ext]
 theorem ext : (∀ i j, M i j = N i j) → M = N :=
   ext_iff.mp
 #align matrix.ext Matrix.ext
 
--- Porting note: `ext` does not like if there are two variables introduced at once. E.g.
--- ```
--- example (A B : Matrix m n α) : A = B := by
---   ext i j
---   sorry
--- ```
--- would only introduce the first variable, so that afterwards, the state is
--- ```
--- i : m
--- ⊢ ∀ (j : n), A i j = B i j
--- ```
--- This is probably a bug in `ext`. Once it is fixed, you should delete `Matrix.ext'` below
--- and restore the `@[ext]` attribute on `Matrix.ext` above.
-@[ext]
-theorem ext' : (∀ i, M i = N i) → M = N :=
-  fun h => Matrix.ext fun i => by simp[h]
-
 end Ext
 
 /-- Cast a function into a matrix.

Mathlib/Order/Interval.lean

@@ -30,15 +30,13 @@ variable {α β γ δ : Type*} {ι : Sort*} {κ : ι → Sort*}
 
 We define intervals by the pair of endpoints `fst`, `snd`. To convert intervals to the set of
 elements between these endpoints, use the coercion `NonemptyInterval α → Set α`. -/
--- @[ext] -- Porting note: generates the wrong lemma
--- in lean3 it generated `x.toProd = y.toProd → x = y`, now it generates
--- `(x.toProd.fst = y.toProd.fst) → (x.toProd.snd = y.toProd.snd) → x = y`.
--- this is because in `Std.Tactic.Ext.withExtHyps`, the for-loop goes over
--- `getStructureFieldsFlattened` instead of `getStructureFields`.
+@[ext (flat := false)]
 structure NonemptyInterval (α : Type*) [LE α] extends Prod α α where
   /-- The starting point of an interval is smaller than the endpoint. -/
   fst_le_snd : fst ≤ snd
 #align nonempty_interval NonemptyInterval
+#align nonempty_interval.ext NonemptyInterval.ext
+#align nonempty_interval.ext_iff NonemptyInterval.ext_iff
 
 namespace NonemptyInterval
 
@@ -50,17 +48,6 @@ theorem toProd_injective : Injective (toProd : NonemptyInterval α → α × α)
   fun s t h => by cases s; cases t; congr
 #align nonempty_interval.to_prod_injective NonemptyInterval.toProd_injective
 
--- Porting note: This is the manually written old ext-lemma as it was generated in mathlib3.
--- Would be nice to fix `@[ext]` to generate them automatically.
-theorem ext (s t : NonemptyInterval α) (h : s.toProd = t.toProd) : s = t := toProd_injective h
-#align nonempty_interval.ext NonemptyInterval.ext
-
--- Porting note: This is the manually written old ext-lemma as it was generated in mathlib3.
--- Would be nice to fix `@[ext]` to generate them automatically.
-theorem ext_iff (s t : NonemptyInterval α) : s = t ↔ s.toProd = t.toProd :=
-  toProd_injective.eq_iff.symm
-#align nonempty_interval.ext_iff NonemptyInterval.ext_iff
-
 /-- The injection that induces the order on intervals. -/
 def toDualProd : NonemptyInterval α → αᵒᵈ × α :=
   toProd