fix breakage caused by leanprover/lean4#6602

leanprover-community · Jan 10, 2025 · ea80df0 · ea80df0
1 parent f45d805
commit ea80df0
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Group/Pi/Lemmas.lean b/Mathlib/Algebra/Group/Pi/Lemmas.lean
@@ -339,7 +339,7 @@ theorem Pi.semiconjBy_iff {x y z : ∀ i, f i} :
     SemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i) := funext_iff
 
 @[to_additive]
-theorem Commute.pi {x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y := .pi h
+nonrec theorem Commute.pi {x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y := .pi h
 
 @[to_additive]
 theorem Pi.commute_iff {x y : ∀ i, f i} : Commute x y ↔ ∀ i, Commute (x i) (y i) := semiconjBy_iff

diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean
@@ -260,7 +260,8 @@ theorem Prod.semiconjBy_iff {x y z : M × N} :
     SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2 := Prod.ext_iff
 
 @[to_additive AddCommute.prod]
-theorem Commute.prod {x y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y :=
+nonrec theorem Commute.prod {x y : M × N}
+    (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y :=
   .prod hm hn
 
 @[to_additive]

diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean
@@ -352,7 +352,7 @@ theorem of_eq {f g : α → β → σ} (hg : Primrec₂ f) (H : ∀ a b, f a b =
 theorem const (x : σ) : Primrec₂ fun (_ : α) (_ : β) => x :=
   Primrec.const _
 
-protected theorem pair : Primrec₂ (@Prod.mk α β) :=
+protected nonrec theorem pair : Primrec₂ (@Prod.mk α β) :=
   .pair .fst .snd
 
 theorem left : Primrec₂ fun (a : α) (_ : β) => a :=

diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
@@ -716,7 +716,8 @@ def awayMapₐ : Away 𝒜 f →ₐ[𝒜 0] Away 𝒜 x where
 
 /-- This is a convenient constructor for `Away 𝒜 f` when `f` is homogeneous.
 `Away.mk 𝒜 hf n x hx` is the fraction `x / f ^ n`. -/
-protected def Away.mk {d : ι} (hf : f ∈ 𝒜 d) (n : ℕ) (x : A) (hx : x ∈ 𝒜 (n • d)) : Away 𝒜 f :=
+protected nonrec def Away.mk {d : ι}
+    (hf : f ∈ 𝒜 d) (n : ℕ) (x : A) (hx : x ∈ 𝒜 (n • d)) : Away 𝒜 f :=
   .mk ⟨n • d, ⟨x, hx⟩, ⟨f ^ n, SetLike.pow_mem_graded n hf⟩, ⟨n, rfl⟩⟩
 
 @[simp]