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

Mathlib/Algebra/Ring/InjSurj.lean

@@ -11,12 +11,13 @@ import Mathlib.Algebra.GroupWithZero.InjSurj
 # Pulling back rings along injective maps, and pushing them forward along surjective maps
 -/
 
-variable {α β : Type*} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β]
-  [Pow β ℕ] [NatCast β] [IntCast β]
+variable {α β : Type*}
 
 namespace Function.Injective
 variable (f : β → α) (hf : Injective f)
 
+variable [Add β] [Mul β]
+
 /-- Pullback a `LeftDistribClass` instance along an injective function. -/
 theorem leftDistribClass [Mul α] [Add α] [LeftDistribClass α] (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass β where
@@ -27,6 +28,9 @@ theorem rightDistribClass [Mul α] [Add α] [RightDistribClass α] (add : ∀ x
     (mul : ∀ x y, f (x * y) = f x * f y) : RightDistribClass β where
   right_distrib x y z := hf <| by simp only [*, right_distrib]
 
+variable [Zero β] [One β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β]
+  [Pow β ℕ] [NatCast β] [IntCast β]
+
 /-- Pullback a `Distrib` instance along an injective function. -/
 -- See note [reducible non-instances]
 protected abbrev distrib [Distrib α] (add : ∀ x y, f (x + y) = f x + f y)
@@ -191,6 +195,8 @@ end Function.Injective
 namespace Function.Surjective
 variable (f : α → β) (hf : Surjective f)
 
+variable [Add β] [Mul β]
+
 /-- Pushforward a `LeftDistribClass` instance along a surjective function. -/
 theorem leftDistribClass [Mul α] [Add α] [LeftDistribClass α] (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass β where
@@ -208,6 +214,9 @@ protected abbrev distrib [Distrib α] (add : ∀ x y, f (x + y) = f x + f y)
   __ := hf.leftDistribClass f add mul
   __ := hf.rightDistribClass f add mul
 
+variable [Zero β] [One β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β]
+  [Pow β ℕ] [NatCast β] [IntCast β]
+
 /-- A type endowed with `-` and `*` has distributive negation, if it admits a surjective map that
 preserves `-` and `*` from a type which has distributive negation. -/
 -- See note [reducible non-instances]

Mathlib/Data/FunLike/Equiv.lean

@@ -149,7 +149,7 @@ class EquivLike (E : Sort*) (α β : outParam (Sort*)) where
 
 namespace EquivLike
 
-variable {E F α β γ : Sort*} [iE : EquivLike E α β] [iF : EquivLike F β γ]
+variable {E F α β γ : Sort*} [EquivLike E α β] [EquivLike F β γ]
 
 theorem inv_injective : Function.Injective (EquivLike.inv : E → β → α) := fun e g h ↦
   coe_injective' e g ((right_inv e).eq_rightInverse (h.symm ▸ left_inv g)) h
@@ -218,7 +218,7 @@ theorem comp_bijective (f : α → β) (e : F) : Function.Bijective (e ∘ f) 
   (EquivLike.bijective e).of_comp_iff' f
 
 /-- This is not an instance to avoid slowing down every single `Subsingleton` typeclass search. -/
-lemma subsingleton_dom [Subsingleton β] : Subsingleton F :=
+lemma subsingleton_dom [FunLike F β γ] [Subsingleton β] : Subsingleton F :=
   ⟨fun f g ↦ DFunLike.ext f g fun _ ↦ (right_inv f).injective <| Subsingleton.elim _ _⟩
 
 end EquivLike

Mathlib/Data/List/Basic.lean

@@ -1568,6 +1568,8 @@ section FoldlEqFoldlr'
 variable {f : α → β → α}
 variable (hf : ∀ a b c, f (f a b) c = f (f a c) b)
 
+include hf
+
 theorem foldl_eq_of_comm' : ∀ a b l, foldl f a (b :: l) = f (foldl f a l) b
   | a, b, [] => rfl
   | a, b, c :: l => by rw [foldl, foldl, foldl, ← foldl_eq_of_comm' .., foldl, hf]
@@ -1581,17 +1583,17 @@ end FoldlEqFoldlr'
 section FoldlEqFoldlr'
 
 variable {f : α → β → β}
-variable (hf : ∀ a b c, f a (f b c) = f b (f a c))
 
-theorem foldr_eq_of_comm' : ∀ a b l, foldr f a (b :: l) = foldr f (f b a) l
+theorem foldr_eq_of_comm' (hf : ∀ a b c, f a (f b c) = f b (f a c)) :
+    ∀ a b l, foldr f a (b :: l) = foldr f (f b a) l
   | a, b, [] => rfl
-  | a, b, c :: l => by rw [foldr, foldr, foldr, hf, ← foldr_eq_of_comm' ..]; rfl
+  | a, b, c :: l => by rw [foldr, foldr, foldr, hf, ← foldr_eq_of_comm' hf ..]; rfl
 
 end FoldlEqFoldlr'
 
 section
 
-variable {op : α → α → α} [ha : Std.Associative op] [hc : Std.Commutative op]
+variable {op : α → α → α} [ha : Std.Associative op]
 
 /-- Notation for `op a b`. -/
 local notation a " ⋆ " b => op a b
@@ -1612,6 +1614,8 @@ theorem foldl_op_eq_op_foldr_assoc :
   | a :: l, a₁, a₂ => by
     simp only [foldl_cons, foldr_cons, foldl_assoc, ha.assoc]; rw [foldl_op_eq_op_foldr_assoc]
 
+variable [hc : Std.Commutative op]
+
 theorem foldl_assoc_comm_cons {l : List α} {a₁ a₂} : ((a₁ :: l) <*> a₂) = a₁ ⋆ l <*> a₂ := by
   rw [foldl_cons, hc.comm, foldl_assoc]
 

Mathlib/Data/Nat/Find.lean

@@ -71,8 +71,6 @@ protected theorem find_min : ∀ {m : ℕ}, m < Nat.find H → ¬p m :=
 protected theorem find_min' {m : ℕ} (h : p m) : Nat.find H ≤ m :=
   Nat.le_of_not_lt fun l => Nat.find_min H l h
 
-variable [DecidablePred p] [DecidablePred q]
-
 lemma find_eq_iff (h : ∃ n : ℕ, p n) : Nat.find h = m ↔ p m ∧ ∀ n < m, ¬ p n := by
   constructor
   · rintro rfl
@@ -95,6 +93,7 @@ lemma find_eq_iff (h : ∃ n : ℕ, p n) : Nat.find h = m ↔ p m ∧ ∀ n < m,
 
 @[simp] lemma find_eq_zero (h : ∃ n : ℕ, p n) : Nat.find h = 0 ↔ p 0 := by simp [find_eq_iff]
 
+variable [DecidablePred q] in
 lemma find_mono (h : ∀ n, q n → p n) {hp : ∃ n, p n} {hq : ∃ n, q n} : Nat.find hp ≤ Nat.find hq :=
   Nat.find_min' _ (h _ (Nat.find_spec hq))
 

Mathlib/Logic/Basic.lean

@@ -951,6 +951,9 @@ either branch to `a`. -/
 theorem ite_apply (f g : ∀ a, σ a) (a : α) : (ite P f g) a = ite P (f a) (g a) :=
   dite_apply P (fun _ ↦ f) (fun _ ↦ g) a
 
+section
+variable [Decidable Q]
+
 theorem ite_and : ite (P ∧ Q) a b = ite P (ite Q a b) b := by
   by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]
 
@@ -966,6 +969,8 @@ theorem ite_ite_comm (h : P → ¬Q) :
      if Q then b else if P then a else c :=
   dite_dite_comm P Q h
 
+end
+
 variable {P Q}
 
 theorem ite_prop_iff_or : (if P then Q else R) ↔ (P ∧ Q ∨ ¬ P ∧ R) := by