Sync upstream mathlib4 (2026-07-25, +34 commits)

Mathlib.lean

@@ -1101,6 +1101,7 @@ public import Mathlib.Algebra.Order.Ring.InjSurj
 public import Mathlib.Algebra.Order.Ring.Int
 public import Mathlib.Algebra.Order.Ring.Interval
 public import Mathlib.Algebra.Order.Ring.IsNonarchimedean
+public import Mathlib.Algebra.Order.Ring.NNRat
 public import Mathlib.Algebra.Order.Ring.Nat
 public import Mathlib.Algebra.Order.Ring.Opposite
 public import Mathlib.Algebra.Order.Ring.Ordering.Basic
@@ -7321,7 +7322,6 @@ public import Mathlib.Tactic.DeriveCountable
 public import Mathlib.Tactic.DeriveEncodable
 public import Mathlib.Tactic.DeriveFintype
 public import Mathlib.Tactic.DeriveTraversable
-public import Mathlib.Tactic.Determinant.Bird
 public import Mathlib.Tactic.Determinant.Bird.Cert
 public import Mathlib.Tactic.Determinant.Bird.Meta
 public import Mathlib.Tactic.DuplicateDecls
@@ -7446,6 +7446,7 @@ public import Mathlib.Tactic.MoveAdd
 public import Mathlib.Tactic.NoncommRing
 public import Mathlib.Tactic.Nontriviality
 public import Mathlib.Tactic.Nontriviality.Core
+public import Mathlib.Tactic.NormDet
 public import Mathlib.Tactic.NormNum
 public import Mathlib.Tactic.NormNum.Abs
 public import Mathlib.Tactic.NormNum.Basic

Mathlib/Algebra/Central/End.lean

@@ -60,7 +60,7 @@ public theorem LinearEquiv.conjAlgEquiv_ext_iff' {S M₂ : Type*} [CommRing S] [
     (f g : M ≃ₗ[R] M₂) : f.conjAlgEquiv S = g.conjAlgEquiv S ↔ ∃ α : Sˣ, f = α • g := by
   refine ⟨fun h ↦ ?_, fun ⟨y, h⟩ ↦ conjAlgEquiv_ext_iff.mpr ⟨(y : S), congr($h)⟩⟩
   by_cases! Subsingleton M
-  · exact ⟨1, by ext; simp [Subsingleton.eq_zero]⟩
+  · exact ⟨1, by ext; simp [Subsingleton.eq_zero (α := M)]⟩
   obtain ⟨α, hα⟩ := conjAlgEquiv_ext_iff.mp h
   obtain ⟨β, hβ⟩ := conjAlgEquiv_ext_iff.mp h.symm
   obtain ⟨x, hx⟩ := exists_ne (0 : M)

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -236,16 +236,18 @@ end Mem
   /-- Recursor for `FreeAddMonoid` using `0` and
   `FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`. -/]
 -- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable
-def recOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C xs → C (of x * xs)) : C xs := List.rec h0 ih xs
+def recOn {motive : FreeMonoid α → Sort*} (xs : FreeMonoid α) (one : motive 1)
+    (of_mul : ∀ x xs, motive xs → motive (of x * xs)) : motive xs := List.rec one of_mul xs
 
 @[to_additive (attr := simp)]
-theorem recOn_one {C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) :
-    @recOn α C 1 h0 ih = h0 := rfl
+theorem recOn_one {motive : FreeMonoid α → Sort*} (one : motive 1)
+    (of_mul : ∀ x xs, motive xs → motive (of x * xs)) :
+    @recOn α motive 1 one of_mul = one := rfl
 
 @[to_additive (attr := simp)]
-theorem recOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C xs → C (of x * xs)) : @recOn α C (of x * xs) h0 ih = ih x xs (recOn xs h0 ih) :=
+theorem recOn_of_mul {motive : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (one : motive 1)
+    (of_mul : ∀ x xs, motive xs → motive (of x * xs)) :
+    @recOn α motive (of x * xs) one of_mul = of_mul x xs (recOn xs one of_mul) :=
   rfl
 
 /-! ### Induction -/
@@ -255,18 +257,19 @@ section induction_principles
 /-- An induction principle on free monoids, with cases for `1`, `FreeMonoid.of` and `*`. -/
 @[to_additive (attr := elab_as_elim, induction_eliminator)
 /-- An induction principle on free monoids, with cases for `0`, `FreeAddMonoid.of` and `+`. -/]
-protected theorem inductionOn {C : FreeMonoid α → Prop} (z : FreeMonoid α) (one : C 1)
-    (of : ∀ (x : α), C (FreeMonoid.of x)) (mul : ∀ (x y : FreeMonoid α), C x → C y → C (x * y)) :
-    C z :=
-  List.rec one (fun _ _ ih => mul [_] _ (of _) ih) z
+protected theorem inductionOn {motive : FreeMonoid α → Prop} (z : FreeMonoid α) (one : motive 1)
+    (of : ∀ (x : α), motive (FreeMonoid.of x))
+    (mul : ∀ (x y : FreeMonoid α), motive x → motive y → motive (x * y)) :
+    motive z :=
+  recOn z one fun x xs ih => mul (.of x) xs (of x) ih
 
 /-- An induction principle for free monoids which mirrors induction on lists, with cases analogous
 to the empty list and cons -/
 @[to_additive (attr := elab_as_elim) /-- An induction principle for free monoids which mirrors
 induction on lists, with cases analogous to the empty list and cons -/]
-protected theorem inductionOn' {p : FreeMonoid α → Prop} (a : FreeMonoid α)
-    (one : p (1 : FreeMonoid α)) (mul_of : ∀ b a, p a → p (of b * a)) : p a :=
-  List.rec one (fun _ _ tail_ih => mul_of _ _ tail_ih) a
+protected theorem inductionOn' {motive : FreeMonoid α → Prop} (a : FreeMonoid α)
+    (one : motive (1 : FreeMonoid α)) (of_mul : ∀ b a, motive a → motive (of b * a)) : motive a :=
+  recOn a one of_mul
 
 end induction_principles
 
@@ -275,16 +278,18 @@ end induction_principles
 @[to_additive (attr := elab_as_elim, cases_eliminator)
   /-- A version of `List.casesOn` for `FreeAddMonoid` using `0` and
   `FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`. -/]
-def casesOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C (of x * xs)) : C xs := List.casesOn xs h0 ih
+def casesOn {motive : FreeMonoid α → Sort*} (xs : FreeMonoid α) (one : motive 1)
+    (of_mul : ∀ x xs, motive (of x * xs)) : motive xs := List.casesOn xs one of_mul
 
 @[to_additive (attr := simp)]
-theorem casesOn_one {C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) :
-    @casesOn α C 1 h0 ih = h0 := rfl
+theorem casesOn_one {motive : FreeMonoid α → Sort*} (one : motive 1)
+    (of_mul : ∀ x xs, motive (of x * xs)) :
+    @casesOn α motive 1 one of_mul = one := rfl
 
 @[to_additive (attr := simp)]
-theorem casesOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C (of x * xs)) : @casesOn α C (of x * xs) h0 ih = ih x xs := rfl
+theorem casesOn_of_mul {motive : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (one : motive 1)
+    (of_mul : ∀ x xs, motive (of x * xs)) :
+    @casesOn α motive (of x * xs) one of_mul = of_mul x xs := rfl
 
 @[to_additive (attr := ext)]
 theorem hom_eq ⦃f g : FreeMonoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g :=
@@ -431,7 +436,7 @@ theorem map_surjective {f : α → β} : Function.Surjective (map f) ↔ Functio
     | one =>
       have H := congr_arg length hb
       simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H
-    | mul_of head _ _ =>
+    | of_mul head _ _ =>
       simp only [map_mul, map_of] at hb
       use head
       have H := congr_arg length hb
@@ -441,7 +446,7 @@ theorem map_surjective {f : α → β} : Function.Surjective (map f) ↔ Functio
   intro fs d
   induction d using FreeMonoid.inductionOn' with
   | one => use 1; rfl
-  | mul_of head tail ih =>
+  | of_mul head tail ih =>
     specialize fs head
     rcases fs with ⟨a, rfl⟩
     rcases ih with ⟨b, rfl⟩

Mathlib/Algebra/Group/Defs.lean

@@ -1068,9 +1068,13 @@ variable [DivInvMonoid G]
     ZPow.zpow n x = x ^ n :=
   rfl
 
-@[to_additive (attr := simp) zero_zsmul] theorem zpow_zero (a : G) : a ^ (0 : ℤ) = 1 :=
+@[to_additive zero_zsmul] theorem zpow_zero (a : G) : a ^ (0 : ℤ) = 1 :=
   DivInvMonoid.zpow_zero' a
 
+-- `zpow_zero` is provable by `simp` (via `zpow_ofNat`), so the `simpNF` linter rejects tagging it.
+-- We still want the additive `zero_zsmul` to be `simp`, so we tag that one manually.
+attribute [simp] zero_zsmul
+
 @[to_additive (attr := simp, norm_cast) natCast_zsmul]
 theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
   | 0 => (zpow_zero _).trans (pow_zero _).symm
@@ -1080,7 +1084,9 @@ theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
     _ = a ^ (n + 1) := (pow_succ _ _).symm
 
 
-@[to_additive ofNat_zsmul]
+-- TODO: consider also making `ofNat_zsmul` a `simp` lemma; it is currently not, because it breaks
+-- `simp`-normal forms involving `(2 : ℤ) • ·` used in the theory of oriented angles.
+@[to_additive ofNat_zsmul, simp]
 lemma zpow_ofNat (a : G) (n : ℕ) : a ^ (ofNat(n) : ℤ) = a ^ OfNat.ofNat n :=
   zpow_natCast ..
 
@@ -1117,9 +1123,13 @@ theorem mul_div_assoc (a b c : G) : a * b / c = a * (b / c) := by
 theorem one_div (a : G) : 1 / a = a⁻¹ :=
   (inv_eq_one_div a).symm
 
-@[to_additive (attr := simp) one_zsmul]
+@[to_additive one_zsmul]
 lemma zpow_one (a : G) : a ^ (1 : ℤ) = a := by rw [zpow_ofNat, pow_one]
 
+-- `zpow_one` is provable by `simp` (via `zpow_ofNat`), so the `simpNF` linter rejects tagging it.
+-- We still want the additive `one_zsmul` to be `simp`, so we tag that one manually.
+attribute [simp] one_zsmul
+
 @[to_additive two_zsmul] lemma zpow_two (a : G) : a ^ (2 : ℤ) = a * a := by rw [zpow_ofNat, pow_two]
 
 @[to_additive neg_one_zsmul]

Mathlib/Algebra/Group/End.lean

@@ -11,7 +11,6 @@ public import Mathlib.Algebra.Group.Prod
 public import Mathlib.Algebra.Group.Units.Equiv
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Tactic.Common
-
 public import Mathlib.Tactic.Attr.Register
 
 /-!

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -277,7 +277,7 @@ theorem closure_induction_left
   obtain ⟨l, rfl⟩ := h
   induction l using FreeMonoid.inductionOn' with
   | one => exact one
-  | mul_of x y ih =>
+  | of_mul x y ih =>
     simp only [map_mul, FreeMonoid.lift_eval_of]
     refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
     simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

Mathlib/Algebra/Homology/EulerCharacteristic.lean

@@ -103,7 +103,9 @@ variable (c : ComplexShape ι) [c.EulerCharSigns]
 
 /-- The support of a graded object with respect to finite rank:
 the set of indices where the rank is nonzero. -/
-def finrankSupport (X : CategoryTheory.GradedObject ι (ModuleCat R)) : Set ι :=
+-- Note: `Set` has no computational content, but Lean still attempts to compile it.
+-- See https://github.com/leanprover/lean4/issues/14084.
+noncomputable def finrankSupport (X : CategoryTheory.GradedObject ι (ModuleCat R)) : Set ι :=
   Function.support (fun i => Module.finrank R (X i))
 
 /-- The finite rank support is contained in a set if and only if

Mathlib/Algebra/Lie/Semisimple/Basic.lean

@@ -277,11 +277,11 @@ lemma booleanGenerators : BooleanGenerators {I : LieIdeal R L | IsAtom I} where
   finitelyAtomistic _ _ hs _ hIs := finitelyAtomistic _ hs _ hIs
 
 instance (priority := 100) instDistribLattice : DistribLattice (LieIdeal R L) :=
-  (booleanGenerators R L).distribLattice_of_sSup_eq_top sSup_atoms_eq_top
+  (booleanGenerators R L).distribLatticeOfSSupEqTop sSup_atoms_eq_top
 
 noncomputable
 instance (priority := 100) instBooleanAlgebra : BooleanAlgebra (LieIdeal R L) :=
-  (booleanGenerators R L).booleanAlgebra_of_sSup_eq_top sSup_atoms_eq_top
+  (booleanGenerators R L).booleanAlgebraOfSSupEqTop sSup_atoms_eq_top
 
 /-- A semisimple Lie algebra has trivial radical. -/
 instance (priority := 100) instHasTrivialRadical : HasTrivialRadical R L := by

Mathlib/Algebra/Module/Torsion/Basic.lean

@@ -938,19 +938,20 @@ theorem torsionBy_eq_span_singleton {R : Type w} [CommRing R] (a b : R) (ha : a
 
 end Ideal.Quotient
 
-namespace AddMonoid
-
-theorem isTorsion_iff_isTorsion_nat [AddCommMonoid M] :
-    AddMonoid.IsTorsion M ↔ Module.IsTorsion ℕ M := by
+theorem isAddTorsion_iff_isTorsion_nat [AddCommMonoid M] :
+    IsAddTorsion M ↔ Module.IsTorsion ℕ M := by
   refine ⟨fun h x => ?_, fun h x => ?_⟩
   · obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero
     exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩
   · rw [isOfFinAddOrder_iff_nsmul_eq_zero]
     obtain ⟨n, hn⟩ := @h x
     exact ⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩
 
-theorem isTorsion_iff_isTorsion_int [AddCommGroup M] :
-    AddMonoid.IsTorsion M ↔ Module.IsTorsion ℤ M := by
+@[deprecated (since := "2026-07-01")] alias AddMonoid.isTorsion_iff_isTorsion_nat :=
+  isAddTorsion_iff_isTorsion_nat
+
+theorem isAddTorsion_iff_isTorsion_int [AddCommGroup M] :
+    IsAddTorsion M ↔ Module.IsTorsion ℤ M := by
   refine ⟨fun h x => ?_, fun h x => ?_⟩
   · obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero
     exact
@@ -960,7 +961,8 @@ theorem isTorsion_iff_isTorsion_int [AddCommGroup M] :
     obtain ⟨n, hn⟩ := @h x
     exact ⟨_, Int.natAbs_pos.2 (nonZeroDivisors.coe_ne_zero n), natAbs_nsmul_eq_zero.2 hn⟩
 
-end AddMonoid
+@[deprecated (since := "2026-07-01")] alias AddMonoid.isTorsion_iff_isTorsion_int :=
+  isAddTorsion_iff_isTorsion_int
 
 namespace AddSubgroup
 

Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean

@@ -50,7 +50,7 @@ lemma degreeOf_prod_eq {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ
     (h : ∀ i ∈ s, f i ≠ 0) :
     degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i) := by
   rcases subsingleton_or_nontrivial (MvPolynomial σ R) with nontrivial | nontrivial
-  · simp [Subsingleton.eq_zero]
+  · simp [Subsingleton.eq_zero (α := MvPolynomial σ R)]
   · classical
     induction s using Finset.induction_on with
     | empty => simp

Mathlib/Algebra/Notation/Indicator.lean

@@ -228,6 +228,13 @@ lemma comp_mulIndicator_const (c : M) (f : M → N) (hf : f 1 = 1) :
     (fun x => f (s.mulIndicator (fun _ => c) x)) = s.mulIndicator fun _ => f c :=
   (mulIndicator_comp_of_one hf).symm
 
+/-- Evaluating the indicator of a family of functions at a point commutes with the indicator:
+`s.mulIndicator f a b = s.mulIndicator (f · b) a`. -/
+@[to_additive]
+lemma mulIndicator_apply_apply (f : α → β → M) (b : β) :
+    s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a := by
+  by_cases h : a ∈ s <;> simp [h]
+
 @[to_additive]
 lemma mulIndicator_preimage (s : Set α) (f : α → M) (B : Set M) :
     mulIndicator s f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B) :=

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -185,7 +185,7 @@ omit [Nontrivial R] in
 /-- An absolute value satisfies `f (n : R) ≤ n` for every `n : ℕ`. -/
 lemma apply_nat_le_self [IsOrderedRing S] (n : ℕ) : abv n ≤ n := by
   cases subsingleton_or_nontrivial R
-  · simp [Subsingleton.eq_zero (n : R)]
+  · simp [Subsingleton.eq_zero (α := R)]
   induction n with
   | zero => simp
   | succ n ih =>

Mathlib/Algebra/Order/Antidiag/Pi.lean

@@ -9,6 +9,7 @@ module
 public import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
 public import Mathlib.Data.Fin.Tuple.NatAntidiagonal
 public import Mathlib.Data.Finset.Sym
+public import Mathlib.Algebra.Group.Pi.Lemmas
 
 /-!
 # Antidiagonal of functions as finsets
@@ -58,7 +59,6 @@ In this section, we define the antidiagonals in `Fin d → μ` by recursion on `
 computationally efficient, although probably not as efficient as `Finset.Nat.antidiagonalTuple`.
 -/
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Auxiliary construction for `finAntidiagonal` that bundles a proof of lawfulness
 (`mem_finAntidiagonal`), as this is needed to invoke `disjiUnion`. Using `Finset.disjiUnion` makes
 this computationally much more efficient than using `Finset.biUnion`. -/
@@ -73,16 +73,10 @@ def finAntidiagonal.aux (d : ℕ) (n : μ) : {s : Finset (Fin d → μ) // ∀ f
     { val := (antidiagonal n).disjiUnion
         (fun ab => (aux d ab.2).1.map {
             toFun := Fin.cons (ab.1)
-            inj' := Fin.cons_right_injective _ })
-        (fun i _hi j _hj hij => Finset.disjoint_left.2 fun t hti htj => hij <| by
-          simp_rw [Finset.mem_map, Embedding.coeFn_mk] at hti htj
-          obtain ⟨ai, hai, hij'⟩ := hti
-          obtain ⟨aj, haj, rfl⟩ := htj
-          rw [Fin.cons_inj] at hij'
-          ext
-          · exact hij'.1
-          · obtain ⟨-, rfl⟩ := hij'
-            rw [← (aux d i.2).prop ai |>.mp hai, ← (aux d j.2).prop ai |>.mp haj])
+            inj' := Fin.cons_right_injective _ }) <| by
+        intro i _ j _ hij
+        simp only [Finset.disjoint_left, Finset.mem_map, Embedding.coeFn_mk]
+        grind [Fin.cons_inj]
       property := fun f => by
         simp_rw [mem_disjiUnion, mem_antidiagonal, mem_map, Embedding.coeFn_mk, Prod.exists,
           (aux d _).prop, Fin.sum_univ_succ]
@@ -92,7 +86,6 @@ def finAntidiagonal.aux (d : ℕ) (n : μ) : {s : Finset (Fin d → μ) // ∀ f
         · intro hf
           exact ⟨_, _, hf, _, rfl, Fin.cons_self_tail f⟩ }
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `finAntidiagonal d n` is the type of `d`-tuples with sum `n`.
 
 TODO: deduplicate with the less general `Finset.Nat.antidiagonalTuple`. -/
@@ -109,13 +102,13 @@ choosing an identification `s ≃ Fin s.card` and proving that the end result do
 choice.
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The finset of functions `ι → μ` with support contained in `s` and sum `n`. -/
 def piAntidiag (s : Finset ι) (n : μ) : Finset (ι → μ) := by
   refine (Fintype.truncEquivFinOfCardEq <| Fintype.card_coe s).lift
     (fun e ↦ (finAntidiagonal s.card n).map ⟨fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, ?_⟩)
     fun e₁ e₂ ↦ ?_
-  · rintro f g hfg
+  · rw [Injective]
+    rintro f g hfg
     ext i
     simpa using congr_fun hfg (e.symm i)
   · ext f
@@ -126,7 +119,6 @@ def piAntidiag (s : Finset ι) (n : μ) : Finset (ι → μ) := by
 
 variable {s : Finset ι} {n : μ} {f : ι → μ}
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] lemma mem_piAntidiag : f ∈ piAntidiag s n ↔ s.sum f = n ∧ ∀ i, f i ≠ 0 → i ∈ s := by
   rw [piAntidiag]
   induction Fintype.truncEquivFinOfCardEq (Fintype.card_coe s) using Trunc.ind with | _ e
@@ -181,8 +173,7 @@ lemma piAntidiag_cons (hi : i ∉ s) (n : μ) :
   constructor
   · rintro ⟨hn, hf⟩
     refine ⟨_, _, hn, update f i 0, ⟨sum_update_of_notMem hi _ _, fun j ↦ ?_⟩, by aesop⟩
-    have := fun h₁ h₂ ↦ (hf j h₁).resolve_left h₂
-    aesop (add simp [update])
+    grind
   · rintro ⟨a, _, hn, g, ⟨rfl, hg⟩, rfl⟩
     have := hg i
     aesop (add simp [sum_add_distrib])
@@ -206,16 +197,14 @@ end CanonicallyOrderedAddCommMonoid
 section Nat
 variable [DecidableEq ι]
 
-/-- Local notation for the pointwise operation `n • s := {n • a | a ∈ s}` to avoid conflict with the
-pointwise operation `n • s := s + ... + s` (`n` times). -/
-local infixr:73 " •ℕ " => @SMul.smul _ _ Finset.smulFinset
+open Pointwise
 
 lemma piAntidiag_univ_fin_eq_antidiagonalTuple (n k : ℕ) :
     piAntidiag univ n = Nat.antidiagonalTuple k n := by
   ext; simp [Nat.mem_antidiagonalTuple]
 
 lemma nsmul_piAntidiag [DecidableEq (ι → ℕ)] (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
-    n •ℕ piAntidiag s m = {f ∈ piAntidiag s (n * m) | ∀ i ∈ s, n ∣ f i} := by
+    n • piAntidiag s m = {f ∈ piAntidiag s (n * m) | ∀ i ∈ s, n ∣ f i} := by
   ext f
   refine mem_smul_finset.trans ?_
   simp only [mem_filter, mem_piAntidiag, and_assoc]
@@ -233,18 +222,16 @@ lemma nsmul_piAntidiag [DecidableEq (ι → ℕ)] (s : Finset ι) (m : ℕ) {n :
   grind
 
 lemma map_nsmul_piAntidiag (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
-    (piAntidiag s m).map
-      ⟨(n • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ hn (congr_fun h i)⟩ =
+    (piAntidiag s m).map ⟨(n • ·), nsmul_right_injective hn⟩ =
         {f ∈ piAntidiag s (n * m) | ∀ i ∈ s, n ∣ f i} := by
   classical rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn
 
 lemma nsmul_piAntidiag_univ [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
-    n •ℕ (piAntidiag univ m) = {f ∈ piAntidiag (univ : Finset ι) (n * m) | ∀ i, n ∣ f i} := by
+    n • piAntidiag univ m = {f ∈ piAntidiag (univ : Finset ι) (n * m) | ∀ i, n ∣ f i} := by
   simpa using nsmul_piAntidiag (univ : Finset ι) m hn
 
 lemma map_nsmul_piAntidiag_univ [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
-    (piAntidiag (univ : Finset ι) m).map
-        ⟨(n • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ hn (congr_fun h i)⟩ =
+    (piAntidiag (univ : Finset ι) m).map ⟨(n • ·), nsmul_right_injective hn⟩ =
       {f ∈ piAntidiag (univ : Finset ι) (n * m) | ∀ i, n ∣ f i} := by
   simpa using map_nsmul_piAntidiag (univ : Finset ι) m hn