chore: backports for leanprover/lean4#4814 (part 17) (#15429)

see #15245

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Mathlib/Algebra/CharP/ExpChar.lean

@@ -91,6 +91,22 @@ theorem char_eq_expChar_iff (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p
     decide
   · exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp hq_hchar⟩
 
+/-- The exponential characteristic is a prime number or one.
+See also `CharP.char_is_prime_or_zero`. -/
+theorem expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1 := by
+  cases hq with
+  | zero => exact .inr rfl
+  | prime hp => exact .inl hp
+
+/-- The exponential characteristic is positive. -/
+theorem expChar_pos (q : ℕ) [ExpChar R q] : 0 < q := by
+  rcases expChar_is_prime_or_one R q with h | rfl
+  exacts [Nat.Prime.pos h, Nat.one_pos]
+
+/-- Any power of the exponential characteristic is positive. -/
+theorem expChar_pow_pos (q : ℕ) [ExpChar R q] (n : ℕ) : 0 < q ^ n :=
+  Nat.pos_pow_of_pos n (expChar_pos R q)
+
 section Nontrivial
 
 variable [Nontrivial R]
@@ -126,22 +142,6 @@ theorem char_prime_of_ne_zero {p : ℕ} [hp : CharP R p] (p_ne_zero : p ≠ 0) :
   · exact h
   · contradiction
 
-/-- The exponential characteristic is a prime number or one.
-See also `CharP.char_is_prime_or_zero`. -/
-theorem expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1 := by
-  cases hq with
-  | zero => exact .inr rfl
-  | prime hp => exact .inl hp
-
-/-- The exponential characteristic is positive. -/
-theorem expChar_pos (q : ℕ) [ExpChar R q] : 0 < q := by
-  rcases expChar_is_prime_or_one R q with h | rfl
-  exacts [Nat.Prime.pos h, Nat.one_pos]
-
-/-- Any power of the exponential characteristic is positive. -/
-theorem expChar_pow_pos (q : ℕ) [ExpChar R q] (n : ℕ) : 0 < q ^ n :=
-  Nat.pos_pow_of_pos n (expChar_pos R q)
-
 end NoZeroDivisors
 
 end Nontrivial

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -217,7 +217,7 @@ end CommSemiring
 section aeval
 
 variable [CommSemiring R] [Semiring A] [CommSemiring A'] [Semiring B]
-variable [Algebra R A] [Algebra R A'] [Algebra R B]
+variable [Algebra R A] [Algebra R B]
 variable {p q : R[X]} (x : A)
 
 /-- Given a valuation `x` of the variable in an `R`-algebra `A`, `aeval R A x` is

Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

@@ -305,19 +305,7 @@ end Ring
 
 section NoZeroDivisors
 
-variable [Semiring R] [NoZeroDivisors R] {p q : R[X]} {a : R}
-
-theorem degree_mul_C (a0 : a ≠ 0) : (p * C a).degree = p.degree := by
-  rw [degree_mul, degree_C a0, add_zero]
-
-theorem degree_C_mul (a0 : a ≠ 0) : (C a * p).degree = p.degree := by
-  rw [degree_mul, degree_C a0, zero_add]
-
-theorem natDegree_mul_C (a0 : a ≠ 0) : (p * C a).natDegree = p.natDegree := by
-  simp only [natDegree, degree_mul_C a0]
-
-theorem natDegree_C_mul (a0 : a ≠ 0) : (C a * p).natDegree = p.natDegree := by
-  simp only [natDegree, degree_C_mul a0]
+variable [Semiring R] {p q : R[X]} {a : R}
 
 @[simp]
 lemma nextCoeff_C_mul_X_add_C (ha : a ≠ 0) (c : R) : nextCoeff (C a * X + C c) = c := by
@@ -337,6 +325,20 @@ lemma natDegree_eq_one : p.natDegree = 1 ↔ ∃ a ≠ 0, ∃ b, C a * X + C b =
   · rintro ⟨a, ha, b, rfl⟩
     simp [ha]
 
+variable [NoZeroDivisors R]
+
+theorem degree_mul_C (a0 : a ≠ 0) : (p * C a).degree = p.degree := by
+  rw [degree_mul, degree_C a0, add_zero]
+
+theorem degree_C_mul (a0 : a ≠ 0) : (C a * p).degree = p.degree := by
+  rw [degree_mul, degree_C a0, zero_add]
+
+theorem natDegree_mul_C (a0 : a ≠ 0) : (p * C a).natDegree = p.natDegree := by
+  simp only [natDegree, degree_mul_C a0]
+
+theorem natDegree_C_mul (a0 : a ≠ 0) : (C a * p).natDegree = p.natDegree := by
+  simp only [natDegree, degree_C_mul a0]
+
 theorem natDegree_comp : natDegree (p.comp q) = natDegree p * natDegree q := by
   by_cases q0 : q.natDegree = 0
   · rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,

Mathlib/Algebra/Polynomial/Module/Basic.lean

@@ -221,7 +221,7 @@ lemma equivPolynomial_single {S : Type*} [CommRing S] [Algebra R S] (n : ℕ) (x
     equivPolynomial (single R n x) = monomial n x := rfl
 
 variable (R' : Type*) {M' : Type*} [CommRing R'] [AddCommGroup M'] [Module R' M']
-variable [Algebra R R'] [Module R M'] [IsScalarTower R R' M']
+variable [Module R M']
 
 /-- The image of a polynomial under a linear map. -/
 noncomputable def map (f : M →ₗ[R] M') : PolynomialModule R M →ₗ[R] PolynomialModule R' M' :=
@@ -231,6 +231,8 @@ noncomputable def map (f : M →ₗ[R] M') : PolynomialModule R M →ₗ[R] Poly
 theorem map_single (f : M →ₗ[R] M') (i : ℕ) (m : M) : map R' f (single R i m) = single R' i (f m) :=
   Finsupp.mapRange_single (hf := f.map_zero)
 
+variable [Algebra R R'] [IsScalarTower R R' M']
+
 theorem map_smul (f : M →ₗ[R] M') (p : R[X]) (q : PolynomialModule R M) :
     map R' f (p • q) = p.map (algebraMap R R') • map R' f q := by
   apply induction_linear q

Mathlib/Algebra/Polynomial/Smeval.lean

@@ -181,8 +181,16 @@ octonions), we replace the `[Semiring S]` with `[NonAssocSemiring S] [Pow S ℕ]
 -/
 
 variable (R : Type*) [Semiring R] {p : R[X]} (r : R) (p q : R[X]) {S : Type*}
-  [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] [Pow S ℕ]
-  [NatPowAssoc S] (x : S)
+  [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S)
+
+theorem smeval_C_mul : (C r * p).smeval x = r • p.smeval x := by
+  induction p using Polynomial.induction_on' with
+  | h_add p q ph qh =>
+    simp only [mul_add, smeval_add, ph, qh, smul_add]
+  | h_monomial n b =>
+    simp only [C_mul_monomial, smeval_monomial, mul_smul]
+
+variable [NatPowAssoc S]
 
 theorem smeval_at_natCast (q : ℕ[X]) : ∀(n : ℕ), q.smeval (n : S) = q.smeval n := by
   induction q using Polynomial.induction_on' with
@@ -206,13 +214,8 @@ theorem smeval_at_zero : p.smeval (0 : S) = (p.coeff 0) • (1 : S)  := by
     | succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
         smul_zero]
 
-theorem smeval_mul_X : (p * X).smeval x = p.smeval x * x := by
-    induction p using Polynomial.induction_on' with
-  | h_add p q ph qh =>
-    simp only [add_mul, smeval_add, ph, qh]
-  | h_monomial n a =>
-    simp only [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, mul_one, pow_succ',
-      mul_assoc, npow_add, smul_mul_assoc, npow_one]
+section
+variable [SMulCommClass R S S]
 
 theorem smeval_X_mul : (X * p).smeval x = x * p.smeval x := by
     induction p using Polynomial.induction_on' with
@@ -222,21 +225,6 @@ theorem smeval_X_mul : (X * p).smeval x = x * p.smeval x := by
     rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add,
       npow_one, ← mul_smul_comm, smeval_monomial]
 
-theorem smeval_assoc_X_pow (m n : ℕ) :
-    p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n) := by
-  induction p using Polynomial.induction_on' with
-  | h_add p q ph qh =>
-    simp only [smeval_add, ph, qh, add_mul]
-  | h_monomial n a =>
-    rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_mul_assoc]
-
-theorem smeval_mul_X_pow : ∀ (n : ℕ), (p * X^n).smeval x = p.smeval x * x^n
-  | 0 => by
-    simp only [npow_zero, mul_one]
-  | n + 1 => by
-    rw [npow_add, ← mul_assoc, npow_one, smeval_mul_X, smeval_mul_X_pow n, npow_add,
-      ← smeval_assoc_X_pow, npow_one]
-
 theorem smeval_X_pow_assoc (m n : ℕ) :
     x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x) := by
   induction p using Polynomial.induction_on' with
@@ -252,13 +240,6 @@ theorem smeval_X_pow_mul : ∀ (n : ℕ), (X^n * p).smeval x = x^n * p.smeval x
     rw [add_comm, npow_add, mul_assoc, npow_one, smeval_X_mul, smeval_X_pow_mul n, npow_add,
       smeval_X_pow_assoc, npow_one]
 
-theorem smeval_C_mul : (C r * p).smeval x = r • p.smeval x := by
-  induction p using Polynomial.induction_on' with
-  | h_add p q ph qh =>
-    simp only [mul_add, smeval_add, ph, qh, smul_add]
-  | h_monomial n b =>
-    simp only [C_mul_monomial, smeval_monomial, mul_smul]
-
 theorem smeval_monomial_mul (n : ℕ) :
     (monomial n r * p).smeval x = r • (x ^ n * p.smeval x) := by
   induction p using Polynomial.induction_on' with
@@ -268,6 +249,35 @@ theorem smeval_monomial_mul (n : ℕ) :
   | h_monomial n a =>
     rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]
 
+end
+
+variable [IsScalarTower R S S]
+
+theorem smeval_mul_X : (p * X).smeval x = p.smeval x * x := by
+    induction p using Polynomial.induction_on' with
+  | h_add p q ph qh =>
+    simp only [add_mul, smeval_add, ph, qh]
+  | h_monomial n a =>
+    simp only [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, mul_one, pow_succ',
+      mul_assoc, npow_add, smul_mul_assoc, npow_one]
+
+theorem smeval_assoc_X_pow (m n : ℕ) :
+    p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n) := by
+  induction p using Polynomial.induction_on' with
+  | h_add p q ph qh =>
+    simp only [smeval_add, ph, qh, add_mul]
+  | h_monomial n a =>
+    rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_mul_assoc]
+
+theorem smeval_mul_X_pow : ∀ (n : ℕ), (p * X^n).smeval x = p.smeval x * x^n
+  | 0 => by
+    simp only [npow_zero, mul_one]
+  | n + 1 => by
+    rw [npow_add, ← mul_assoc, npow_one, smeval_mul_X, smeval_mul_X_pow n, npow_add,
+      ← smeval_assoc_X_pow, npow_one]
+
+variable [SMulCommClass R S S]
+
 theorem smeval_mul : (p * q).smeval x  = p.smeval x * q.smeval x := by
   induction p using Polynomial.induction_on' with
   | h_add r s hr hs =>

Mathlib/Algebra/Quaternion.lean

@@ -89,11 +89,14 @@ theorem equivTuple_apply {R : Type*} (c₁ c₂ : R) (x : ℍ[R,c₁,c₂]) :
 @[simp]
 theorem mk.eta {R : Type*} {c₁ c₂} (a : ℍ[R,c₁,c₂]) : mk a.1 a.2 a.3 a.4 = a := rfl
 
-variable {S T R : Type*} [CommRing R] {c₁ c₂ : R} (r x y z : R) (a b c : ℍ[R,c₁,c₂])
+variable {S T R : Type*} {c₁ c₂ : R} (r x y z : R) (a b c : ℍ[R,c₁,c₂])
 
 instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).subsingleton
 instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).surjective.nontrivial
 
+section Zero
+variable [Zero R]
+
 /-- The imaginary part of a quaternion. -/
 def im (x : ℍ[R,c₁,c₂]) : ℍ[R,c₁,c₂] :=
   ⟨0, x.imI, x.imJ, x.imK⟩
@@ -159,6 +162,9 @@ theorem coe_zero : ((0 : R) : ℍ[R,c₁,c₂]) = 0 := rfl
 
 instance : Inhabited ℍ[R,c₁,c₂] := ⟨0⟩
 
+section One
+variable [One R]
+
 -- Porting note: removed `simps`, added simp lemmas manually
 instance : One ℍ[R,c₁,c₂] := ⟨⟨1, 0, 0, 0⟩⟩
 
@@ -175,6 +181,11 @@ instance : One ℍ[R,c₁,c₂] := ⟨⟨1, 0, 0, 0⟩⟩
 @[simp, norm_cast]
 theorem coe_one : ((1 : R) : ℍ[R,c₁,c₂]) = 1 := rfl
 
+end One
+end Zero
+section Add
+variable [Add R]
+
 -- Porting note: removed `simps`, added simp lemmas manually
 instance : Add ℍ[R,c₁,c₂] :=
   ⟨fun a b => ⟨a.1 + b.1, a.2 + b.2, a.3 + b.3, a.4 + b.4⟩⟩
@@ -187,17 +198,27 @@ instance : Add ℍ[R,c₁,c₂] :=
 
 @[simp] theorem add_imK : (a + b).imK = a.imK + b.imK := rfl
 
-@[simp] theorem add_im : (a + b).im = a.im + b.im :=
-  QuaternionAlgebra.ext (zero_add _).symm rfl rfl rfl
-
 @[simp]
 theorem mk_add_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
     (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) + mk b₁ b₂ b₃ b₄ = mk (a₁ + b₁) (a₂ + b₂) (a₃ + b₃) (a₄ + b₄) :=
   rfl
 
+end Add
+
+section AddZeroClass
+variable [AddZeroClass R]
+
+@[simp] theorem add_im : (a + b).im = a.im + b.im :=
+  QuaternionAlgebra.ext (zero_add _).symm rfl rfl rfl
+
 @[simp, norm_cast]
 theorem coe_add : ((x + y : R) : ℍ[R,c₁,c₂]) = x + y := by ext <;> simp
 
+end AddZeroClass
+
+section Neg
+variable [Neg R]
+
 -- Porting note: removed `simps`, added simp lemmas manually
 instance : Neg ℍ[R,c₁,c₂] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
 
@@ -209,13 +230,18 @@ instance : Neg ℍ[R,c₁,c₂] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
 
 @[simp] theorem neg_imK : (-a).imK = -a.imK := rfl
 
-@[simp] theorem neg_im : (-a).im = -a.im :=
-  QuaternionAlgebra.ext neg_zero.symm rfl rfl rfl
-
 @[simp]
 theorem neg_mk (a₁ a₂ a₃ a₄ : R) : -(mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) = ⟨-a₁, -a₂, -a₃, -a₄⟩ :=
   rfl
 
+end Neg
+
+section AddGroup
+variable [AddGroup R]
+
+@[simp] theorem neg_im : (-a).im = -a.im :=
+  QuaternionAlgebra.ext neg_zero.symm rfl rfl rfl
+
 @[simp, norm_cast]
 theorem coe_neg : ((-x : R) : ℍ[R,c₁,c₂]) = -x := by ext <;> simp
 
@@ -254,6 +280,11 @@ theorem sub_self_im : a - a.im = a.re :=
 theorem sub_self_re : a - a.re = a.im :=
   QuaternionAlgebra.ext (sub_self _) (sub_zero _) (sub_zero _) (sub_zero _)
 
+end AddGroup
+
+section Ring
+variable [Ring R]
+
 /-- Multiplication is given by
 
 * `1 * x = x * 1 = x`;
@@ -290,11 +321,11 @@ theorem mk_mul_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
         a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂, a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁⟩ :=
   rfl
 
-section
+end Ring
+section SMul
 
 variable [SMul S R] [SMul T R] (s : S)
 
--- Porting note: Lean 4 auto drops the unused `[Ring R]` argument
 instance : SMul S ℍ[R,c₁,c₂] where smul s a := ⟨s • a.1, s • a.2, s • a.3, s • a.4⟩
 
 instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T ℍ[R,c₁,c₂] where
@@ -311,25 +342,28 @@ instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂] where
 
 @[simp] theorem smul_imK : (s • a).imK = s • a.imK := rfl
 
-@[simp] theorem smul_im {S} [SMulZeroClass S R] (s : S) : (s • a).im = s • a.im :=
+@[simp] theorem smul_im {S} [CommRing R] [SMulZeroClass S R] (s : S) : (s • a).im = s • a.im :=
   QuaternionAlgebra.ext (smul_zero s).symm rfl rfl rfl
 
 @[simp]
 theorem smul_mk (re im_i im_j im_k : R) :
     s • (⟨re, im_i, im_j, im_k⟩ : ℍ[R,c₁,c₂]) = ⟨s • re, s • im_i, s • im_j, s • im_k⟩ :=
   rfl
 
-end
+end SMul
 
 @[simp, norm_cast]
-theorem coe_smul [SMulZeroClass S R] (s : S) (r : R) :
+theorem coe_smul [Zero R] [SMulZeroClass S R] (s : S) (r : R) :
     (↑(s • r) : ℍ[R,c₁,c₂]) = s • (r : ℍ[R,c₁,c₂]) :=
   QuaternionAlgebra.ext rfl (smul_zero s).symm (smul_zero s).symm (smul_zero s).symm
 
-instance : AddCommGroup ℍ[R,c₁,c₂] :=
+instance [AddCommGroup R] : AddCommGroup ℍ[R,c₁,c₂] :=
   (equivProd c₁ c₂).injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
     (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
 
+section AddCommGroupWithOne
+variable [AddCommGroupWithOne R]
+
 instance : AddCommGroupWithOne ℍ[R,c₁,c₂] where
   natCast n := ((n : R) : ℍ[R,c₁,c₂])
   natCast_zero := by simp
@@ -424,6 +458,11 @@ theorem coe_intCast (z : ℤ) : ↑(z : R) = (z : ℍ[R,c₁,c₂]) :=
 @[deprecated (since := "2024-04-17")]
 alias coe_int_cast := coe_intCast
 
+end AddCommGroupWithOne
+
+-- For the remainder of the file we assume `CommRing R`.
+variable [CommRing R]
+
 instance instRing : Ring ℍ[R,c₁,c₂] where
   __ := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
   left_distrib _ _ _ := by ext <;> simp <;> ring

Mathlib/GroupTheory/HNNExtension.lean

@@ -345,7 +345,7 @@ theorem unitsSMulGroup_snd (u : ℤˣ) (g : G) :
     (unitsSMulGroup φ d u g).2 = ((d.compl u).equiv g).2 := by
   rcases Int.units_eq_one_or u with rfl | rfl <;> rfl
 
-variable {d} [DecidableEq G]
+variable {d}
 
 /-- `Cancels u w` is a predicate expressing whether `t^u` cancels with some occurence
 of `t^-u` when when we multiply `t^u` by `w`. -/