avoid nonrec for leanprover/lean4#6602

leanprover-community · Jan 12, 2025 · 89f6ddc · 89f6ddc
1 parent ea80df0
commit 89f6ddc
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 11 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]
-nonrec theorem Commute.pi {x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y := .pi h
+theorem Commute.pi {x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y := SemiconjBy.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,9 +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]
-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
+theorem Commute.prod {x y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y :=
+  SemiconjBy.prod hm hn
 
 @[to_additive]
 theorem Prod.commute_iff {x y : M × N} :

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

diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
@@ -716,9 +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 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⟩⟩
+protected def Away.mk {d : ι} (hf : f ∈ 𝒜 d) (n : ℕ) (x : A) (hx : x ∈ 𝒜 (n • d)) : Away 𝒜 f :=
+  HomogeneousLocalization.mk ⟨n • d, ⟨x, hx⟩, ⟨f ^ n, SetLike.pow_mem_graded n hf⟩, ⟨n, rfl⟩⟩
 
 @[simp]
 lemma Away.val_mk {d : ι} (n : ℕ) (hf : f ∈ 𝒜 d) (x : A) (hx : x ∈ 𝒜 (n • d)) :

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -61,11 +61,11 @@
    "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/batteries",
+  {"url": "https://github.com/cppio/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0b8bfa6400ad2af013fadd42c2e04ebc3e5eaf0a",
+   "rev": "4eb73047bf9795adb772e82c9611b7f8d76e7c1a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "lean-pr-testing-6602",