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

Mathlib/Algebra/BigOperators/Group/Multiset.lean

@@ -22,7 +22,7 @@ and sums indexed by finite sets.
 
 assert_not_exists MonoidWithZero
 
-variable {F ι α β γ : Type*}
+variable {F ι α β β' γ : Type*}
 
 namespace Multiset
 
@@ -124,27 +124,27 @@ theorem pow_count [DecidableEq α] (a : α) : a ^ s.count a = (s.filter (Eq a)).
   rw [filter_eq, prod_replicate]
 
 @[to_additive]
-theorem prod_hom [CommMonoid β] (s : Multiset α) {F : Type*} [FunLike F α β]
+theorem prod_hom (s : Multiset α) {F : Type*} [FunLike F α β]
     [MonoidHomClass F α β] (f : F) :
     (s.map f).prod = f s.prod :=
   Quotient.inductionOn s fun l => by simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]
 
 @[to_additive]
-theorem prod_hom' [CommMonoid β] (s : Multiset ι) {F : Type*} [FunLike F α β]
+theorem prod_hom' (s : Multiset ι) {F : Type*} [FunLike F α β]
     [MonoidHomClass F α β] (f : F)
     (g : ι → α) : (s.map fun i => f <| g i).prod = f (s.map g).prod := by
   convert (s.map g).prod_hom f
   exact (map_map _ _ _).symm
 
 @[to_additive]
-theorem prod_hom₂ [CommMonoid β] [CommMonoid γ] (s : Multiset ι) (f : α → β → γ)
+theorem prod_hom₂ [CommMonoid γ] (s : Multiset ι) (f : α → β → γ)
     (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → α)
     (f₂ : ι → β) : (s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod :=
   Quotient.inductionOn s fun l => by
     simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]
 
 @[to_additive]
-theorem prod_hom_rel [CommMonoid β] (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β}
+theorem prod_hom_rel (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β}
     (h₁ : r 1 1) (h₂ : ∀ ⦃a b c⦄, r b c → r (f a * b) (g a * c)) :
     r (s.map f).prod (s.map g).prod :=
   Quotient.inductionOn s fun l => by
@@ -163,7 +163,7 @@ theorem prod_map_pow {n : ℕ} : (m.map fun i => f i ^ n).prod = (m.map f).prod
   m.prod_hom' (powMonoidHom n : α →* α) f
 
 @[to_additive]
-theorem prod_map_prod_map (m : Multiset β) (n : Multiset γ) {f : β → γ → α} :
+theorem prod_map_prod_map (m : Multiset β') (n : Multiset γ) {f : β' → γ → α} :
     prod (m.map fun a => prod <| n.map fun b => f a b) =
       prod (n.map fun b => prod <| m.map fun a => f a b) :=
   Multiset.induction_on m (by simp) fun a m ih => by simp [ih]

Mathlib/Algebra/Module/Basic.lean

@@ -148,7 +148,7 @@ end Function
 
 namespace Set
 section SMulZeroClass
-variable [Zero R] [Zero M] [SMulZeroClass R M]
+variable [Zero M] [SMulZeroClass R M]
 
 lemma indicator_smul_apply (s : Set α) (r : α → R) (f : α → M) (a : α) :
     indicator s (fun a ↦ r a • f a) a = r a • indicator s f a := by

Mathlib/Algebra/Module/Defs.lean

@@ -546,11 +546,12 @@ end AddCommGroup
 
 section Module
 
-variable [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
+variable [Ring R] [AddCommGroup M] [Module R M]
 
 section SMulInjective
 
 variable (R)
+variable [NoZeroSMulDivisors R M]
 
 theorem smul_left_injective {x : M} (hx : x ≠ 0) : Function.Injective fun c : R => c • x :=
   fun c d h =>

Mathlib/Algebra/Order/Group/Lattice.lean

@@ -40,50 +40,65 @@ open Function
 variable {α β : Type*}
 
 section Group
-variable [Lattice α] [Group α] [CovariantClass α α (· * ·) (· ≤ ·)]
-  [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
+variable [Lattice α] [Group α]
 
 -- Special case of Bourbaki A.VI.9 (1)
 @[to_additive]
-lemma mul_sup (a b c : α) : c * (a ⊔ b) = c * a ⊔ c * b := (OrderIso.mulLeft _).map_sup _ _
+lemma mul_sup [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) :
+    c * (a ⊔ b) = c * a ⊔ c * b :=
+  (OrderIso.mulLeft _).map_sup _ _
 
 @[to_additive]
-lemma sup_mul (a b c : α) : (a ⊔ b) * c = a * c ⊔ b * c := (OrderIso.mulRight _).map_sup _ _
+lemma sup_mul [CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a b c : α) :
+    (a ⊔ b) * c = a * c ⊔ b * c :=
+  (OrderIso.mulRight _).map_sup _ _
 
 @[to_additive]
-lemma mul_inf (a b c : α) : c * (a ⊓ b) = c * a ⊓ c * b := (OrderIso.mulLeft _).map_inf _ _
+lemma mul_inf [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) :
+    c * (a ⊓ b) = c * a ⊓ c * b :=
+  (OrderIso.mulLeft _).map_inf _ _
 
 @[to_additive]
-lemma inf_mul (a b c : α) : (a ⊓ b) * c = a * c ⊓ b * c := (OrderIso.mulRight _).map_inf _ _
+lemma inf_mul [CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a b c : α) :
+    (a ⊓ b) * c = a * c ⊓ b * c :=
+  (OrderIso.mulRight _).map_inf _ _
+
+@[to_additive]
+lemma sup_div [CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a b c : α) :
+    (a ⊔ b) / c = a / c ⊔ b / c :=
+  (OrderIso.divRight _).map_sup _ _
+
+@[to_additive]
+lemma inf_div [CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a b c : α) :
+    (a ⊓ b) / c = a / c ⊓ b / c :=
+  (OrderIso.divRight _).map_inf _ _
+
+section
+variable [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
 
--- Special case of Bourbaki A.VI.9 (2)
 @[to_additive] lemma inv_sup (a b : α) : (a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹ := (OrderIso.inv α).map_sup _ _
 
 @[to_additive] lemma inv_inf (a b : α) : (a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹ := (OrderIso.inv α).map_inf _ _
 
 @[to_additive]
 lemma div_sup (a b c : α) : c / (a ⊔ b) = c / a ⊓ c / b := (OrderIso.divLeft c).map_sup _ _
 
-@[to_additive]
-lemma sup_div (a b c : α) : (a ⊔ b) / c = a / c ⊔ b / c := (OrderIso.divRight _).map_sup _ _
-
 @[to_additive]
 lemma div_inf (a b c : α) : c / (a ⊓ b) = c / a ⊔ c / b := (OrderIso.divLeft c).map_inf _ _
 
-@[to_additive]
-lemma inf_div (a b c : α) : (a ⊓ b) / c = a / c ⊓ b / c := (OrderIso.divRight _).map_inf _ _
-
 -- In fact 0 ≤ n•a implies 0 ≤ a, see L. Fuchs, "Partially ordered algebraic systems"
 -- Chapter V, 1.E
 -- See also `one_le_pow_iff` for the existing version in linear orders
 @[to_additive]
 lemma pow_two_semiclosed
-    [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a := by
+    {a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a := by
   suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
     rwa [← inf_eq_right, ← mul_right_eq_self]
   rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm,
     inf_assoc, inf_of_le_left ha]
 
+end
+
 end Group
 
 variable [Lattice α] [CommGroup α]

Mathlib/Algebra/Order/Group/Unbundled/Abs.lean

@@ -203,6 +203,8 @@ variable [Group α] [LinearOrder α] {a b : α}
 @[to_additive] lemma isSquare_mabs : IsSquare |a|ₘ ↔ IsSquare a :=
   mabs_by_cases (IsSquare · ↔ _) Iff.rfl isSquare_inv
 
+@[to_additive] lemma lt_of_mabs_lt : |a|ₘ < b → a < b := (le_mabs_self _).trans_lt
+
 variable [CovariantClass α α (· * ·) (· ≤ ·)] {a b c : α}
 
 @[to_additive (attr := simp) abs_pos] lemma one_lt_mabs : 1 < |a|ₘ ↔ a ≠ 1 := by
@@ -245,8 +247,6 @@ variable [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
 
 @[to_additive] lemma inv_lt_of_mabs_lt (h : |a|ₘ < b) : b⁻¹ < a := (mabs_lt.mp h).1
 
-@[to_additive] lemma lt_of_mabs_lt : |a|ₘ < b → a < b := (le_mabs_self _).trans_lt
-
 @[to_additive] lemma max_div_min_eq_mabs' (a b : α) : max a b / min a b = |a / b|ₘ := by
   rcases le_total a b with ab | ba
   · rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]

Mathlib/Algebra/Order/Group/Unbundled/Basic.lean

@@ -210,9 +210,21 @@ end TypeclassesRightLT
 
 section TypeclassesLeftRightLE
 
-variable [LE α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
+variable [LE α] [CovariantClass α α (· * ·) (· ≤ ·)]
   {a b c d : α}
 
+@[to_additive (attr := simp)]
+theorem div_le_self_iff (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b := by
+  simp [div_eq_mul_inv]
+
+@[to_additive (attr := simp)]
+theorem le_div_self_iff (a : α) {b : α} : a ≤ a / b ↔ b ≤ 1 := by
+  simp [div_eq_mul_inv]
+
+alias ⟨_, sub_le_self⟩ := sub_le_self_iff
+
+variable [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
+
 @[to_additive (attr := simp)]
 theorem inv_le_inv_iff : a⁻¹ ≤ b⁻¹ ↔ b ≤ a := by
   rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b]
@@ -225,23 +237,21 @@ theorem mul_inv_le_inv_mul_iff : a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b :
   rw [← mul_le_mul_iff_left d, ← mul_le_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
     inv_mul_cancel_right]
 
-@[to_additive (attr := simp)]
-theorem div_le_self_iff (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b := by
-  simp [div_eq_mul_inv]
-
-@[to_additive (attr := simp)]
-theorem le_div_self_iff (a : α) {b : α} : a ≤ a / b ↔ b ≤ 1 := by
-  simp [div_eq_mul_inv]
-
-alias ⟨_, sub_le_self⟩ := sub_le_self_iff
-
 end TypeclassesLeftRightLE
 
 section TypeclassesLeftRightLT
 
-variable [LT α] [CovariantClass α α (· * ·) (· < ·)] [CovariantClass α α (swap (· * ·)) (· < ·)]
+variable [LT α] [CovariantClass α α (· * ·) (· < ·)]
   {a b c d : α}
 
+@[to_additive (attr := simp)]
+theorem div_lt_self_iff (a : α) {b : α} : a / b < a ↔ 1 < b := by
+  simp [div_eq_mul_inv]
+
+alias ⟨_, sub_lt_self⟩ := sub_lt_self_iff
+
+variable [CovariantClass α α (swap (· * ·)) (· < ·)]
+
 @[to_additive (attr := simp)]
 theorem inv_lt_inv_iff : a⁻¹ < b⁻¹ ↔ b < a := by
   rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b]
@@ -266,12 +276,6 @@ theorem mul_inv_lt_inv_mul_iff : a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b := by
   rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
     inv_mul_cancel_right]
 
-@[to_additive (attr := simp)]
-theorem div_lt_self_iff (a : α) {b : α} : a / b < a ↔ 1 < b := by
-  simp [div_eq_mul_inv]
-
-alias ⟨_, sub_lt_self⟩ := sub_lt_self_iff
-
 end TypeclassesLeftRightLT
 
 section Preorder
@@ -796,5 +800,3 @@ theorem StrictAntiOn.inv (hf : StrictAntiOn f s) : StrictMonoOn (fun x => (f x)
   fun _ hx _ hy hxy => inv_lt_inv_iff.2 (hf hx hy hxy)
 
 end
-
-

Mathlib/Algebra/Order/Hom/Monoid.lean

@@ -205,7 +205,7 @@ theorem antitone_iff_map_nonneg : Antitone (f : α → β) ↔ ∀ a ≤ 0, 0 
 
 variable [CovariantClass β β (· + ·) (· < ·)]
 
-theorem strictMono_iff_map_pos [iamhc : AddMonoidHomClass F α β]  :
+theorem strictMono_iff_map_pos :
     StrictMono (f : α → β) ↔ ∀ a, 0 < a → 0 < f a := by
   refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
   · rw [← map_zero f]

Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean

@@ -18,7 +18,7 @@ variable {α β : Type*}
   rules relating them. -/
 
 section CommSemigroup
-variable [LinearOrder α] [CommSemigroup α] [CommSemigroup β]
+variable [LinearOrder α] [CommSemigroup β]
 
 @[to_additive]
 lemma fn_min_mul_fn_max  (f : α → β) (a b : α) : f (min a b) * f (max a b) = f a * f b := by
@@ -28,6 +28,8 @@ lemma fn_min_mul_fn_max  (f : α → β) (a b : α) : f (min a b) * f (max a b)
 lemma fn_max_mul_fn_min (f : α → β) (a b : α) : f (max a b) * f (min a b) = f a * f b := by
   obtain h | h := le_total a b <;> simp [h, mul_comm]
 
+variable [CommSemigroup α]
+
 @[to_additive (attr := simp)]
 lemma min_mul_max (a b : α) : min a b * max a b = a * b := fn_min_mul_fn_max id _ _
 

Mathlib/Algebra/Order/Sub/Canonical.lean

@@ -247,7 +247,7 @@ theorem tsub_tsub_tsub_cancel_left (h : b ≤ a) : a - c - (a - b) = b - c :=
 
 -- note: not generalized to `AddLECancellable` because `add_tsub_add_eq_tsub_left` isn't
 /-- The `tsub` version of `sub_sub_eq_add_sub`. -/
-theorem tsub_tsub_eq_add_tsub_of_le [ContravariantClass α α HAdd.hAdd LE.le]
+theorem tsub_tsub_eq_add_tsub_of_le
     (h : c ≤ b) : a - (b - c) = a + c - b := by
   obtain ⟨d, rfl⟩ := exists_add_of_le h
   rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_left]
@@ -433,7 +433,7 @@ theorem tsub_add_min : a - b + min a b = a := by
   apply min_le_left
 
 -- `Odd.tsub` requires `CanonicallyLinearOrderedSemiring`, which we don't have
-lemma Even.tsub [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α]
+lemma Even.tsub
     [ContravariantClass α α (· + ·) (· ≤ ·)] {m n : α} (hm : Even m) (hn : Even n) :
     Even (m - n) := by
   obtain ⟨a, rfl⟩ := hm

Mathlib/Data/Finset/Basic.lean

@@ -2292,6 +2292,7 @@ theorem filter_cons {a : α} (s : Finset α) (ha : a ∉ s) :
   · rw [filter_cons_of_pos _ _ _ ha h, singleton_disjUnion]
   · rw [filter_cons_of_neg _ _ _ ha h, empty_disjUnion]
 
+section
 variable [DecidableEq α]
 
 theorem filter_union (s₁ s₂ : Finset α) : (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p :=
@@ -2425,6 +2426,8 @@ theorem filter_union_filter_neg_eq [∀ x, Decidable (¬p x)] (s : Finset α) :
     (s.filter p ∪ s.filter fun a => ¬p a) = s :=
   filter_union_filter_of_codisjoint _ _ _ <| @codisjoint_hnot_right _ _ p
 
+end
+
 lemma filter_inj : s.filter p = t.filter p ↔ ∀ ⦃a⦄, p a → (a ∈ s ↔ a ∈ t) := by simp [ext_iff]
 
 lemma filter_inj' : s.filter p = s.filter q ↔ ∀ ⦃a⦄, a ∈ s → (p a ↔ q a) := by simp [ext_iff]

Mathlib/Data/Finset/Pi.lean

@@ -33,7 +33,10 @@ def Pi.empty (β : α → Sort*) (a : α) (h : a ∈ (∅ : Finset α)) : β a :
   Multiset.Pi.empty β a h
 
 universe u v
-variable {β : α → Type u} {δ : α → Sort v} [DecidableEq α] {s : Finset α} {t : ∀ a, Finset (β a)}
+variable {β : α → Type u} {δ : α → Sort v} {s : Finset α} {t : ∀ a, Finset (β a)}
+
+section
+variable [DecidableEq α]
 
 /-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `δ a`, then one can define the
 finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
@@ -128,6 +131,8 @@ theorem pi_disjoint_of_disjoint {δ : α → Type*} {s : Finset α} (t₁ t₂ :
     disjoint_iff_ne.1 h (f₁ a ha) (mem_pi.mp hf₁ a ha) (f₂ a ha) (mem_pi.mp hf₂ a ha) <|
       congr_fun (congr_fun eq₁₂ a) ha
 
+end
+
 /-! ### Diagonal -/
 
 variable {ι : Type*} [DecidableEq (ι → α)] {s : Finset α} {f : ι → α}

Mathlib/Data/Fintype/Basic.lean

@@ -282,6 +282,11 @@ theorem univ_filter_mem_range (f : α → β) [Fintype β] [DecidablePred fun y
 theorem coe_filter_univ (p : α → Prop) [DecidablePred p] :
     (univ.filter p : Set α) = { x | p x } := by simp
 
+end Finset
+
+namespace Finset
+variable  {s t : Finset α}
+
 @[simp] lemma subtype_eq_univ {p : α → Prop} [DecidablePred p] [Fintype {a // p a}] :
     s.subtype p = univ ↔ ∀ ⦃a⦄, p a → a ∈ s := by simp [ext_iff]
 

Mathlib/Data/Multiset/Basic.lean

@@ -2249,7 +2249,7 @@ theorem count_map_eq_count' [DecidableEq β] (f : α → β) (s : Multiset α) (
     contradiction
 
 @[simp]
-theorem sub_filter_eq_filter_not [DecidableEq α] (p) [DecidablePred p] (s : Multiset α) :
+theorem sub_filter_eq_filter_not (p) [DecidablePred p] (s : Multiset α) :
     s - s.filter p = s.filter (fun a ↦ ¬ p a) := by
   ext a; by_cases h : p a <;> simp [h]