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

see #15245

Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean

@@ -33,8 +33,8 @@ complexes. Here, we follow the original definitions in [Verdiers's thesis, I.3][
 open CategoryTheory Category Limits CochainComplex.HomComplex Pretriangulated
 
 variable {C D : Type*} [Category C] [Category D]
-  [Preadditive C] [HasZeroObject C] [HasBinaryBiproducts C]
-  [Preadditive D] [HasZeroObject D] [HasBinaryBiproducts D]
+  [Preadditive C] [HasBinaryBiproducts C]
+  [Preadditive D] [HasBinaryBiproducts D]
   {K L : CochainComplex C ℤ} (φ : K ⟶ L)
 
 namespace CochainComplex
@@ -420,6 +420,7 @@ lemma isomorphic_distinguished (T₁ : Triangle (HomotopyCategory C (ComplexShap
   obtain ⟨X, Y, f, ⟨e'⟩⟩ := hT₁
   exact ⟨X, Y, f, ⟨e ≪≫ e'⟩⟩
 
+variable [HasZeroObject C] in
 lemma contractible_distinguished (X : HomotopyCategory C (ComplexShape.up ℤ)) :
     Pretriangulated.contractibleTriangle X ∈ distinguishedTriangles C := by
   obtain ⟨X⟩ := X
@@ -491,6 +492,8 @@ lemma complete_distinguished_triangle_morphism
 
 end Pretriangulated
 
+variable [HasZeroObject C]
+
 instance : Pretriangulated (HomotopyCategory C (ComplexShape.up ℤ)) where
   distinguishedTriangles := Pretriangulated.distinguishedTriangles C
   isomorphic_distinguished := Pretriangulated.isomorphic_distinguished
@@ -506,6 +509,8 @@ lemma mappingCone_triangleh_distinguished {X Y : CochainComplex C ℤ} (f : X 
     CochainComplex.mappingCone.triangleh f ∈ distTriang (HomotopyCategory _ _) :=
   ⟨_, _, f, ⟨Iso.refl _⟩⟩
 
+variable [HasZeroObject D]
+
 instance (G : C ⥤ D) [G.Additive] :
     (G.mapHomotopyCategory (ComplexShape.up ℤ)).IsTriangulated where
   map_distinguished := by

Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean

@@ -16,7 +16,7 @@ the pretriangulated category `HomotopyCategory C (ComplexShape.up ℤ)` is trian
 
 open CategoryTheory Category Limits Pretriangulated ComposableArrows
 
-variable {C : Type*} [Category C] [Preadditive C] [HasZeroObject C] [HasBinaryBiproducts C]
+variable {C : Type*} [Category C] [Preadditive C] [HasBinaryBiproducts C]
   {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
 
 namespace CochainComplex
@@ -176,6 +176,8 @@ end CochainComplex
 
 namespace HomotopyCategory
 
+variable [HasZeroObject C]
+
 lemma mappingConeCompTriangleh_distinguished :
     (CochainComplex.mappingConeCompTriangleh f g) ∈
       distTriang (HomotopyCategory C (ComplexShape.up ℤ)) := by

Mathlib/Algebra/Module/Torsion.lean

@@ -357,10 +357,10 @@ variable {R M}
 section Coprime
 
 variable {ι : Type*} {p : ι → Ideal R} {S : Finset ι}
-variable (hp : (S : Set ι).Pairwise fun i j => p i ⊔ p j = ⊤)
 
 -- Porting note: mem_iSup_finset_iff_exists_sum now requires DecidableEq ι
-theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf :
+theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf
+    (hp : (S : Set ι).Pairwise fun i j => p i ⊔ p j = ⊤) :
     ⨆ i ∈ S, torsionBySet R M (p i) = torsionBySet R M ↑(⨅ i ∈ S, p i) := by
   rcases S.eq_empty_or_nonempty with h | h
   · simp only [h]
@@ -396,7 +396,8 @@ theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf :
     · rw [← Finset.sum_smul, hμ, one_smul]
 
 -- Porting note: iSup_torsionBySet_ideal_eq_torsionBySet_iInf now requires DecidableEq ι
-theorem supIndep_torsionBySet_ideal : S.SupIndep fun i => torsionBySet R M <| p i :=
+theorem supIndep_torsionBySet_ideal (hp : (S : Set ι).Pairwise fun i j => p i ⊔ p j = ⊤) :
+    S.SupIndep fun i => torsionBySet R M <| p i :=
   fun T hT i hi hiT => by
   rw [disjoint_iff, Finset.sup_eq_iSup,
     iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij]
@@ -406,9 +407,9 @@ theorem supIndep_torsionBySet_ideal : S.SupIndep fun i => torsionBySet R M <| p
   rw [← this, Ideal.sup_iInf_eq_top, top_coe, torsionBySet_univ]
   intro j hj; apply hp hi (hT hj); rintro rfl; exact hiT hj
 
-variable {q : ι → R} (hq : (S : Set ι).Pairwise <| (IsCoprime on q))
+variable {q : ι → R}
 
-theorem iSup_torsionBy_eq_torsionBy_prod :
+theorem iSup_torsionBy_eq_torsionBy_prod (hq : (S : Set ι).Pairwise <| (IsCoprime on q)) :
     ⨆ i ∈ S, torsionBy R M (q i) = torsionBy R M (∏ i ∈ S, q i) := by
   rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ←
     Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf, ←
@@ -420,7 +421,8 @@ theorem iSup_torsionBy_eq_torsionBy_prod :
     exact (torsionBySet_span_singleton_eq _).symm
   exact fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime _ _).mpr (hq hi hj ij)
 
-theorem supIndep_torsionBy : S.SupIndep fun i => torsionBy R M <| q i := by
+theorem supIndep_torsionBy (hq : (S : Set ι).Pairwise <| (IsCoprime on q)) :
+    S.SupIndep fun i => torsionBy R M <| q i := by
   convert supIndep_torsionBySet_ideal (M := M) fun i hi j hj ij =>
       (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij
   exact (torsionBySet_span_singleton_eq (R := R) (M := M) _).symm

Mathlib/Analysis/Normed/Group/CocompactMap.lean

@@ -24,11 +24,11 @@ map is cocompact.
 open Filter Metric
 
 variable {𝕜 E F 𝓕 : Type*}
-variable [NormedAddCommGroup E] [NormedAddCommGroup F] [ProperSpace E] [ProperSpace F]
+variable [NormedAddCommGroup E] [NormedAddCommGroup F]
 variable {f : 𝓕}
 
-theorem CocompactMapClass.norm_le [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F] (ε : ℝ) :
-    ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖ := by
+theorem CocompactMapClass.norm_le [ProperSpace F] [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F]
+    (ε : ℝ) : ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖ := by
   have h := cocompact_tendsto f
   rw [tendsto_def] at h
   specialize h (Metric.closedBall 0 ε)ᶜ (mem_cocompact_of_closedBall_compl_subset 0 ⟨ε, rfl.subset⟩)
@@ -39,7 +39,7 @@ theorem CocompactMapClass.norm_le [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F
   apply hr
   simp [hx]
 
-theorem Filter.tendsto_cocompact_cocompact_of_norm {f : E → F}
+theorem Filter.tendsto_cocompact_cocompact_of_norm [ProperSpace E] {f : E → F}
     (h : ∀ ε : ℝ, ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) :
     Tendsto f (cocompact E) (cocompact F) := by
   rw [tendsto_def]
@@ -53,7 +53,7 @@ theorem Filter.tendsto_cocompact_cocompact_of_norm {f : E → F}
   apply hε
   simp [hr x hx]
 
-theorem ContinuousMapClass.toCocompactMapClass_of_norm [FunLike 𝓕 E F] [ContinuousMapClass 𝓕 E F]
-    (h : ∀ (f : 𝓕) (ε : ℝ), ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) :
+theorem ContinuousMapClass.toCocompactMapClass_of_norm [ProperSpace E] [FunLike 𝓕 E F]
+    [ContinuousMapClass 𝓕 E F] (h : ∀ (f : 𝓕) (ε : ℝ), ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) :
     CocompactMapClass 𝓕 E F where
   cocompact_tendsto := (tendsto_cocompact_cocompact_of_norm <| h ·)

Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

@@ -170,14 +170,6 @@ theorem ext {f g : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ x, f x = g x) : f = g
 
 variable [FunLike 𝓕 E E₂]
 
-protected theorem congr_arg {f : 𝓕} :
-    ∀ {x x' : E}, x = x' → f x = f x'
-  | _, _, rfl => rfl
-
-protected theorem congr_fun {f g : 𝓕} (h : f = g) (x : E) :
-    f x = g x :=
-  h ▸ rfl
-
 -- @[simp] -- Porting note (#10618): simp can prove this
 protected theorem map_zero : f 0 = 0 :=
   f.toLinearMap.map_zero

Mathlib/Analysis/Oscillation.lean

@@ -93,12 +93,12 @@ end Oscillation
 
 namespace IsCompact
 
-variable [PseudoEMetricSpace E] {K : Set E} (comp : IsCompact K)
+variable [PseudoEMetricSpace E] {K : Set E}
 variable {f : E → F} {D : Set E} {ε : ENNReal}
 
 /-- If `oscillationWithin f D x < ε` at every `x` in a compact set `K`, then there exists `δ > 0`
 such that the oscillation of `f` on `ball x δ ∩ D` is less than `ε` for every `x` in `K`. -/
-theorem uniform_oscillationWithin (hK : ∀ x ∈ K, oscillationWithin f D x < ε) :
+theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithin f D x < ε) :
     ∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε := by
   let S := fun r ↦ { x : E | ∃ (a : ℝ), (a > r ∧ diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε) }
   have S_open : ∀ r > 0, IsOpen (S r) := by
@@ -144,7 +144,7 @@ theorem uniform_oscillationWithin (hK : ∀ x ∈ K, oscillationWithin f D x < 
 
 /-- If `oscillation f x < ε` at every `x` in a compact set `K`, then there exists `δ > 0` such
 that the oscillation of `f` on `ball x δ` is less than `ε` for every `x` in `K`. -/
-theorem uniform_oscillation [PseudoEMetricSpace E] {K : Set E} (comp : IsCompact K)
+theorem uniform_oscillation {K : Set E} (comp : IsCompact K)
     {f : E → F} {ε : ENNReal} (hK : ∀ x ∈ K, oscillation f x < ε) :
     ∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ))) ≤ ε := by
   simp only [← oscillationWithin_univ_eq_oscillation] at hK

Mathlib/CategoryTheory/Sites/Discrete.lean

@@ -39,8 +39,10 @@ open CategoryTheory Limits Functor Adjunction Opposite Category Functor
 namespace CategoryTheory.Sheaf
 
 variable {C : Type*} [Category C] (J : GrothendieckTopology C) {A : Type*} [Category A]
-  [HasWeakSheafify J A] [(constantSheaf J A).Faithful] [(constantSheaf J A).Full]
-  {t : C} (ht : IsTerminal t)
+  [HasWeakSheafify J A] {t : C} (ht : IsTerminal t)
+
+section
+variable [(constantSheaf J A).Faithful] [(constantSheaf J A).Full]
 
 /--
 A sheaf is discrete if it is a discrete object of the "underlying object" functor from the sheaf
@@ -80,8 +82,6 @@ variable (G : C ⥤ D)
   [∀ (X : Dᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) A]
   [G.IsDenseSubsite J K] (ht' : IsTerminal (G.obj t))
 
-variable [(constantSheaf J A).Faithful] [(constantSheaf J A).Full]
-
 open Functor.IsDenseSubsite
 
 noncomputable example :
@@ -152,12 +152,11 @@ lemma isDiscrete_iff_of_equivalence (F : Sheaf K A) :
 
 end Equivalence
 
+end
+
 section Forget
 
-variable {B : Type*} [Category B] (U : A ⥤ B)
-  [HasWeakSheafify J A] [HasWeakSheafify J B]
-  [(constantSheaf J A).Faithful] [(constantSheaf J A).Full]
-  [(constantSheaf J B).Faithful] [(constantSheaf J B).Full]
+variable {B : Type*} [Category B] (U : A ⥤ B) [HasWeakSheafify J B]
   [J.PreservesSheafification U] [J.HasSheafCompose U] (F : Sheaf J A)
 
 open Limits
@@ -263,6 +262,9 @@ lemma sheafCompose_reflects_discrete [(sheafCompose J U).ReflectsIsomorphisms]
     apply ReflectsIsomorphisms.reflects (sheafToPresheaf J B) _
   apply ReflectsIsomorphisms.reflects (sheafCompose J U) _
 
+variable [(constantSheaf J A).Full] [(constantSheaf J A).Faithful]
+  [(constantSheaf J B).Full] [(constantSheaf J B).Faithful]
+
 instance [h : F.IsDiscrete J ht] :
     ((sheafCompose J U).obj F).IsDiscrete J ht := by
   rw [isDiscrete_iff_mem_essImage] at h ⊢

Mathlib/CategoryTheory/Sites/InducedTopology.lean

@@ -49,7 +49,7 @@ class LocallyCoverDense : Prop where
   functorPushforward_functorPullback_mem :
     ∀ ⦃X : C⦄ (T : K (G.obj X)), (T.val.functorPullback G).functorPushforward G ∈ K (G.obj X)
 
-variable [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K]
+variable [G.LocallyCoverDense K]
 
 theorem pushforward_cover_iff_cover_pullback [G.Full] [G.Faithful] {X : C} (S : Sieve X) :
     K _ (S.functorPushforward G) ↔ ∃ T : K (G.obj X), T.val.functorPullback G = S := by
@@ -59,6 +59,8 @@ theorem pushforward_cover_iff_cover_pullback [G.Full] [G.Faithful] {X : C} (S :
   · rintro ⟨T, rfl⟩
     exact LocallyCoverDense.functorPushforward_functorPullback_mem T
 
+variable [G.IsLocallyFull K] [G.IsLocallyFaithful K]
+
 /-- If a functor `G : C ⥤ (D, K)` is fully faithful and locally dense,
 then the set `{ T ∩ mor(C) | T ∈ K }` is a grothendieck topology of `C`.
 -/

Mathlib/GroupTheory/Frattini.lean

@@ -20,14 +20,15 @@ the Frattini subgroup consists of the non-generating elements of the group.
 def frattini (G : Type*) [Group G] : Subgroup G :=
   Order.radical (Subgroup G)
 
-variable {G H : Type*} [Group G] [Group H] {φ : G →* H} (hφ : Function.Surjective φ)
+variable {G H : Type*} [Group G] [Group H] {φ : G →* H}
 
 lemma frattini_le_coatom {K : Subgroup G} (h : IsCoatom K) : frattini G ≤ K :=
   Order.radical_le_coatom h
 
 open Subgroup
 
-lemma frattini_le_comap_frattini_of_surjective : frattini G ≤ (frattini H).comap φ := by
+lemma frattini_le_comap_frattini_of_surjective (hφ : Function.Surjective φ) :
+    frattini G ≤ (frattini H).comap φ := by
   simp_rw [frattini, Order.radical, comap_iInf, le_iInf_iff]
   intro M hM
   apply biInf_le

Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -38,7 +38,7 @@ variable {ι : Type w} {ι' : Type w'} {η : Type u₁'} {φ : η → Type*}
 open Cardinal Basis Submodule Function Set FiniteDimensional DirectSum
 
 variable [Ring R] [CommRing S] [AddCommGroup M] [AddCommGroup M'] [AddCommGroup M₁]
-variable [Module R M] [Module R M'] [Module R M₁]
+variable [Module R M]
 
 section Quotient
 
@@ -106,6 +106,7 @@ end ULift
 section Prod
 
 variable (R M M')
+variable [Module R M₁] [Module R M']
 
 open LinearMap in
 theorem lift_rank_add_lift_rank_le_rank_prod [Nontrivial R] :
@@ -150,7 +151,7 @@ end Prod
 section Finsupp
 
 variable (R M M')
-variable [StrongRankCondition R] [Module.Free R M] [Module.Free R M']
+variable [StrongRankCondition R] [Module.Free R M] [Module R M'] [Module.Free R M']
 
 open Module.Free
 
@@ -206,8 +207,6 @@ theorem rank_matrix' (m n : Type v) [Finite m] [Finite n] :
 theorem rank_matrix'' (m n : Type u) [Finite m] [Finite n] :
     Module.rank R (Matrix m n R) = #m * #n := by simp
 
-variable [Module.Finite R M] [Module.Finite R M']
-
 open Fintype
 
 namespace FiniteDimensional
@@ -322,9 +321,9 @@ section TensorProduct
 open TensorProduct
 
 variable [StrongRankCondition R] [StrongRankCondition S]
-variable [Module S M] [Module.Free S M] [Module S M'] [Module.Free S M']
+variable [Module S M] [Module S M'] [Module.Free S M']
 variable [Module S M₁] [Module.Free S M₁]
-variable [Algebra S R] [Module R M] [IsScalarTower S R M] [Module.Free R M]
+variable [Algebra S R] [IsScalarTower S R M] [Module.Free R M]
 
 open Module.Free
 
@@ -382,7 +381,8 @@ theorem Submodule.finrank_quotient_le [Module.Finite R M] (s : Submodule R M) :
     (rank_lt_aleph0 _ _)
 
 /-- Pushforwards of finite submodules have a smaller finrank. -/
-theorem Submodule.finrank_map_le (f : M →ₗ[R] M') (p : Submodule R M) [Module.Finite R p] :
+theorem Submodule.finrank_map_le
+    [Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) [Module.Finite R p] :
     finrank R (p.map f) ≤ finrank R p :=
   finrank_le_finrank_of_rank_le_rank (lift_rank_map_le _ _) (rank_lt_aleph0 _ _)