[Merged by Bors] - chore: backports for leanprover/lean4#4814 (part 5)

Mathlib/Algebra/Group/Pi/Lemmas.lean

@@ -239,25 +239,6 @@ theorem Pi.mulSingle_div [∀ i, Group <| f i] (i : I) (x y : f i) :
     mulSingle i (x / y) = mulSingle i x / mulSingle i y :=
   (MonoidHom.mulSingle f i).map_div x y
 
-section
-variable [∀ i, Mul <| f i]
-
-@[to_additive]
-theorem SemiconjBy.pi {x y z : ∀ i, f i} (h : ∀ i, SemiconjBy (x i) (y i) (z i)) :
-    SemiconjBy x y z :=
-  funext h
-
-@[to_additive]
-theorem Pi.semiconjBy_iff {x y z : ∀ i, f i} :
-    SemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i) := Function.funext_iff
-
-@[to_additive]
-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
-
-end
 
 /-- The injection into a pi group at different indices commutes.
 
@@ -328,6 +309,26 @@ theorem Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {M : Type*} [CommM
 
 end Single
 
+section
+variable [∀ i, Mul <| f i]
+
+@[to_additive]
+theorem SemiconjBy.pi {x y z : ∀ i, f i} (h : ∀ i, SemiconjBy (x i) (y i) (z i)) :
+    SemiconjBy x y z :=
+  funext h
+
+@[to_additive]
+theorem Pi.semiconjBy_iff {x y z : ∀ i, f i} :
+    SemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i) := Function.funext_iff
+
+@[to_additive]
+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
+
+end
+
 namespace Function
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/Group/Support.lean

@@ -19,7 +19,7 @@ open Set
 
 namespace Function
 
-variable {α β A B M N P G : Type*}
+variable {α β A B M M' N P G : Type*}
 
 section One
 variable [One M] [One N] [One P]
@@ -82,7 +82,7 @@ theorem mulSupport_update_eq_ite [DecidableEq α] [DecidableEq M] (f : α → M)
   rcases eq_or_ne y 1 with rfl | hy <;> simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]
 
 @[to_additive]
-theorem mulSupport_extend_one_subset {f : α → M} {g : α → N} :
+theorem mulSupport_extend_one_subset {f : α → M'} {g : α → N} :
     mulSupport (f.extend g 1) ⊆ f '' mulSupport g :=
   mulSupport_subset_iff'.mpr fun x hfg ↦ by
     by_cases hf : ∃ a, f a = x
@@ -92,7 +92,7 @@ theorem mulSupport_extend_one_subset {f : α → M} {g : α → N} :
     · rw [extend_apply' _ _ _ hf]; rfl
 
 @[to_additive]
-theorem mulSupport_extend_one {f : α → M} {g : α → N} (hf : f.Injective) :
+theorem mulSupport_extend_one {f : α → M'} {g : α → N} (hf : f.Injective) :
     mulSupport (f.extend g 1) = f '' mulSupport g :=
   mulSupport_extend_one_subset.antisymm <| by
     rintro _ ⟨x, hx, rfl⟩; rwa [mem_mulSupport, hf.extend_apply]

Mathlib/Algebra/Module/Defs.lean

@@ -471,24 +471,22 @@ end SMulWithZero
 
 section Module
 
-variable [Semiring R] [AddCommMonoid M] [Module R M]
-
 section Nat
 
-variable [NoZeroSMulDivisors R M] [CharZero R]
-variable (R) (M)
-
-theorem Nat.noZeroSMulDivisors : NoZeroSMulDivisors ℕ M where
+theorem Nat.noZeroSMulDivisors
+    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] :
+    NoZeroSMulDivisors ℕ M where
   eq_zero_or_eq_zero_of_smul_eq_zero {c x} := by rw [← Nat.cast_smul_eq_nsmul R, smul_eq_zero]; simp
 
--- Porting note: left-hand side never simplifies when using simp on itself
---@[simp]
-theorem two_nsmul_eq_zero {v : M} : 2 • v = 0 ↔ v = 0 := by
+theorem two_nsmul_eq_zero
+    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : 2 • v = 0 ↔ v = 0 := by
   haveI := Nat.noZeroSMulDivisors R M
   simp [smul_eq_zero]
 
 end Nat
 
+variable [Semiring R] [AddCommMonoid M] [Module R M]
 variable (R M)
 
 /-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic
@@ -522,18 +520,24 @@ end SMulInjective
 
 section Nat
 
-variable [NoZeroSMulDivisors R M] [CharZero R]
-variable (R M)
-
-theorem self_eq_neg {v : M} : v = -v ↔ v = 0 := by
+theorem self_eq_neg
+    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : v = -v ↔ v = 0 := by
   rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]
 
-theorem neg_eq_self {v : M} : -v = v ↔ v = 0 := by rw [eq_comm, self_eq_neg R M]
+theorem neg_eq_self
+    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : -v = v ↔ v = 0 := by
+  rw [eq_comm, self_eq_neg R M]
 
-theorem self_ne_neg {v : M} : v ≠ -v ↔ v ≠ 0 :=
+theorem self_ne_neg
+    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : v ≠ -v ↔ v ≠ 0 :=
   (self_eq_neg R M).not
 
-theorem neg_ne_self {v : M} : -v ≠ v ↔ v ≠ 0 :=
+theorem neg_ne_self
+    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+    {v : M} : -v ≠ v ↔ v ≠ 0 :=
   (neg_eq_self R M).not
 
 end Nat
@@ -565,7 +569,9 @@ instance [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
 
 variable (R M)
 
-theorem NoZeroSMulDivisors.int_of_charZero [CharZero R] : NoZeroSMulDivisors ℤ M :=
+theorem NoZeroSMulDivisors.int_of_charZero
+    (R) (M) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] :
+    NoZeroSMulDivisors ℤ M :=
   ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩
 
 /-- Only a ring of characteristic zero can can have a non-trivial module without additive or

Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

@@ -236,10 +236,10 @@ instance [L.IsEquivalence] : IsIso h.counit := by
   have := fun X => isIso_counit_app_of_iso h (L.objObjPreimageIso X).symm
   apply NatIso.isIso_of_isIso_app
 
-lemma isEquivalence_left_of_isEquivalence_right [R.IsEquivalence] : L.IsEquivalence :=
+lemma isEquivalence_left_of_isEquivalence_right (h : L ⊣ R) [R.IsEquivalence] : L.IsEquivalence :=
   h.toEquivalence.isEquivalence_functor
 
-lemma isEquivalence_right_of_isEquivalence_left [L.IsEquivalence] : R.IsEquivalence :=
+lemma isEquivalence_right_of_isEquivalence_left (h : L ⊣ R) [L.IsEquivalence] : R.IsEquivalence :=
   h.toEquivalence.isEquivalence_inverse
 
 instance [L.IsEquivalence] : IsIso h.unit := by

Mathlib/CategoryTheory/Localization/Predicate.lean

@@ -231,7 +231,7 @@ def functorEquivalence : D ⥤ E ≌ W.FunctorsInverting E :=
 /-- The functor `(D ⥤ E) ⥤ (C ⥤ E)` given by the composition with a localization
 functor `L : C ⥤ D` with respect to `W : MorphismProperty C`. -/
 @[nolint unusedArguments]
-def whiskeringLeftFunctor' (_ : MorphismProperty C) (E : Type*) [Category E] :
+def whiskeringLeftFunctor' [L.IsLocalization W] (E : Type*) [Category E] :
     (D ⥤ E) ⥤ C ⥤ E :=
   (whiskeringLeft C D E).obj L
 
@@ -256,15 +256,17 @@ instance : (whiskeringLeftFunctor' L W E).Faithful := by
   · infer_instance
   apply InducedCategory.faithful -- why is it not found automatically ???
 
-lemma full_whiskeringLeft : ((whiskeringLeft C D E).obj L).Full :=
+lemma full_whiskeringLeft (L : C ⥤ D) (W) [L.IsLocalization W] (E : Type*) [Category E] :
+    ((whiskeringLeft C D E).obj L).Full :=
   inferInstanceAs (whiskeringLeftFunctor' L W E).Full
 
-lemma faithful_whiskeringLeft : ((whiskeringLeft C D E).obj L).Faithful :=
+lemma faithful_whiskeringLeft (L : C ⥤ D) (W) [L.IsLocalization W] (E : Type*) [Category E] :
+    ((whiskeringLeft C D E).obj L).Faithful :=
   inferInstanceAs (whiskeringLeftFunctor' L W E).Faithful
 
 variable {E}
 
-theorem natTrans_ext {F₁ F₂ : D ⥤ E} (τ τ' : F₁ ⟶ F₂)
+theorem natTrans_ext (L : C ⥤ D) (W) [L.IsLocalization W] {F₁ F₂ : D ⥤ E} (τ τ' : F₁ ⟶ F₂)
     (h : ∀ X : C, τ.app (L.obj X) = τ'.app (L.obj X)) : τ = τ' := by
   haveI := essSurj L W
   ext Y
@@ -363,7 +365,7 @@ instance id : Lifting L W L (𝟭 D) :=
 instance compLeft (F : D ⥤ E) : Localization.Lifting L W (L ⋙ F) F := ⟨Iso.refl _⟩
 
 @[simp]
-lemma compLeft_iso (F : D ⥤ E) : Localization.Lifting.iso L W (L ⋙ F) F = Iso.refl _ := rfl
+lemma compLeft_iso (W) (F : D ⥤ E) : Localization.Lifting.iso L W (L ⋙ F) F = Iso.refl _ := rfl
 
 /-- Given a localization functor `L : C ⥤ D` for `W : MorphismProperty C`,
 if `F₁' : D ⥤ E` lifts a functor `F₁ : C ⥤ D`, then a functor `F₂'` which
@@ -488,9 +490,9 @@ lemma mk (L : C ⥤ D) [L.IsLocalization W] (h : L.map f = L.map g) :
   (areEqualizedByLocalization_iff L W f g).2 h
 
 variable {W f g}
-variable (h : AreEqualizedByLocalization W f g)
 
-lemma map_eq (L : C ⥤ D) [L.IsLocalization W] : L.map f = L.map g :=
+lemma map_eq (h : AreEqualizedByLocalization W f g) (L : C ⥤ D) [L.IsLocalization W] :
+    L.map f = L.map g :=
   (areEqualizedByLocalization_iff L W f g).1 h
 
 end AreEqualizedByLocalization

Mathlib/Order/Booleanisation.lean

@@ -42,15 +42,24 @@ namespace Booleanisation
 instance instDecidableEq [DecidableEq α] : DecidableEq (Booleanisation α) :=
   inferInstanceAs <| DecidableEq (α ⊕ α)
 
-variable [GeneralizedBooleanAlgebra α] {x y : Booleanisation α} {a b : α}
-
 /-- The natural inclusion `a ↦ a` from a generalized Boolean algebra to its generated Boolean
 algebra. -/
 @[match_pattern] def lift : α → Booleanisation α := Sum.inl
 
 /-- The inclusion `a ↦ aᶜ from a generalized Boolean algebra to its generated Boolean algebra. -/
 @[match_pattern] def comp : α → Booleanisation α := Sum.inr
 
+/-- The complement operator on `Booleanisation α` sends `a` to `aᶜ` and `aᶜ` to `a`, for `a : α`. -/
+instance instCompl : HasCompl (Booleanisation α) where
+  compl x := match x with
+    | lift a => comp a
+    | comp a => lift a
+
+@[simp] lemma compl_lift (a : α) : (lift a)ᶜ = comp a := rfl
+@[simp] lemma compl_comp (a : α) : (comp a)ᶜ = lift a := rfl
+
+variable [GeneralizedBooleanAlgebra α] {x y : Booleanisation α} {a b : α}
+
 /-- The order on `Booleanisation α` is as follows: For `a b : α`,
 * `a ≤ b` iff `a ≤ b` in `α`
 * `a ≤ bᶜ` iff `a` and `b` are disjoint in `α`
@@ -111,12 +120,6 @@ instance instBot : Bot (Booleanisation α) where
 instance instTop : Top (Booleanisation α) where
   top := comp ⊥
 
-/-- The complement operator on `Booleanisation α` sends `a` to `aᶜ` and `aᶜ` to `a`, for `a : α`. -/
-instance instCompl : HasCompl (Booleanisation α) where
-  compl x := match x with
-    | lift a => comp a
-    | comp a => lift a
-
 /-- The difference operator on `Booleanisation α` is as follows: For `a b : α`,
 * `a \ b` is `a \ b`
 * `a \ bᶜ` is `a ⊓ b`
@@ -152,9 +155,6 @@ instance instSDiff : SDiff (Booleanisation α) where
 @[simp] lemma lift_bot : lift (⊥ : α) = ⊥ := rfl
 @[simp] lemma comp_bot : comp (⊥ : α) = ⊤ := rfl
 
-@[simp] lemma compl_lift (a : α) : (lift a)ᶜ = comp a := rfl
-@[simp] lemma compl_comp (a : α) : (comp a)ᶜ = lift a := rfl
-
 @[simp] lemma lift_sdiff_lift (a b : α) : lift a \ lift b = lift (a \ b) := rfl
 @[simp] lemma lift_sdiff_comp (a b : α) : lift a \ comp b = lift (a ⊓ b) := rfl
 @[simp] lemma comp_sdiff_lift (a b : α) : comp a \ lift b = comp (a ⊔ b) := rfl

Mathlib/Order/Monotone/Basic.lean

@@ -961,7 +961,8 @@ theorem strictAnti_int_of_succ_lt {f : ℤ → α} (hf : ∀ n, f (n + 1) < f n)
 
 namespace Int
 
-variable (α) [Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α]
+variable (α)
+variable [Nonempty α] [NoMinOrder α] [NoMaxOrder α]
 
 /-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
 monotone function `f : ℤ → α`. -/