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

Co-authored-by: blizzard_inc <edegeltje@gmail.com>

Mathlib/Algebra/MonoidAlgebra/Degree.lean

@@ -205,7 +205,7 @@ variable [Semiring R] [Ring R']
 
 section SupDegree
 
-variable [AddZeroClass A] [SemilatticeSup B] [Add B] [OrderBot B] (D : A → B)
+variable [SemilatticeSup B] [OrderBot B] (D : A → B)
 
 /-- Let `R` be a semiring, let `A` be an `AddZeroClass`, let `B` be an `OrderBot`,
 and let `D : A → B` be a "degree" function.
@@ -246,7 +246,12 @@ theorem supDegree_single (a : A) (r : R) :
     (single a r).supDegree D = if r = 0 then ⊥ else D a := by
   split_ifs with hr <;> simp [supDegree_single_ne_zero, hr]
 
-variable {p q : R[A]}
+theorem apply_eq_zero_of_not_le_supDegree {p : R[A]} {a : A} (hlt : ¬ D a ≤ p.supDegree D) :
+    p a = 0 := by
+  contrapose! hlt
+  exact Finset.le_sup (Finsupp.mem_support_iff.2 hlt)
+
+variable [AddZeroClass A] {p q : R[A]}
 
 @[simp]
 theorem supDegree_zero : (0 : R[A]).supDegree D = ⊥ := by simp [supDegree]
@@ -256,11 +261,7 @@ theorem ne_zero_of_supDegree_ne_bot : p.supDegree D ≠ ⊥ → p ≠ 0 := mt (f
 theorem ne_zero_of_not_supDegree_le {b : B} (h : ¬ p.supDegree D ≤ b) : p ≠ 0 :=
   ne_zero_of_supDegree_ne_bot (fun he => h <| he ▸ bot_le)
 
-theorem apply_eq_zero_of_not_le_supDegree {a : A} (hlt : ¬ D a ≤ p.supDegree D) : p a = 0 := by
-  contrapose! hlt
-  exact Finset.le_sup (Finsupp.mem_support_iff.2 hlt)
-
-variable (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2)
+variable [Add B] (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2)
 
 theorem supDegree_mul_le [CovariantClass B B (· + ·) (· ≤ ·)]
     [CovariantClass B B (Function.swap (· + ·)) (· ≤ ·)] :

Mathlib/Algebra/Star/Subalgebra.lean

@@ -650,30 +650,11 @@ namespace StarAlgHom
 open StarSubalgebra StarAlgebra
 
 variable {F R A B : Type*} [CommSemiring R] [StarRing R]
-variable [Semiring A] [Algebra R A] [StarRing A] [StarModule R A]
-variable [Semiring B] [Algebra R B] [StarRing B] [StarModule R B]
-variable [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] (f g : F)
+variable [Semiring A] [Algebra R A] [StarRing A]
+variable [Semiring B] [Algebra R B] [StarRing B]
 
-/-- The equalizer of two star `R`-algebra homomorphisms. -/
-def equalizer : StarSubalgebra R A :=
-  { toSubalgebra := AlgHom.equalizer (f : A →ₐ[R] B) g
-    star_mem' := @fun a (ha : f a = g a) => by simpa only [← map_star] using congrArg star ha }
--- Porting note: much like `StarSubalgebra.copy` the old proof was broken and hard to fix
-
-@[simp]
-theorem mem_equalizer (x : A) : x ∈ StarAlgHom.equalizer f g ↔ f x = g x :=
-  Iff.rfl
-
-theorem adjoin_le_equalizer {s : Set A} (h : s.EqOn f g) : adjoin R s ≤ StarAlgHom.equalizer f g :=
-  adjoin_le h
-
-theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃f g : F⦄ (hs : s.EqOn f g) : f = g :=
-  DFunLike.ext f g fun _x => StarAlgHom.adjoin_le_equalizer f g hs <| h.symm ▸ trivial
-
-theorem map_adjoin (f : A →⋆ₐ[R] B) (s : Set A) :
-    map f (adjoin R s) = adjoin R (f '' s) :=
-  GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarAlgebra.gc
-    StarAlgebra.gc fun _ => rfl
+section
+variable [StarModule R A]
 
 theorem ext_adjoin {s : Set A} [FunLike F (adjoin R s) B]
     [AlgHomClass F R (adjoin R s) B] [StarAlgHomClass F R (adjoin R s) B] {f g : F}
@@ -696,6 +677,32 @@ theorem ext_adjoin_singleton {a : A} [FunLike F (adjoin R ({a} : Set A)) B]
           Subtype.ext <| Set.mem_singleton_iff.mp hx).symm ▸
       h
 
+variable [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] (f g : F)
+
+/-- The equalizer of two star `R`-algebra homomorphisms. -/
+def equalizer : StarSubalgebra R A :=
+  { toSubalgebra := AlgHom.equalizer (f : A →ₐ[R] B) g
+    star_mem' := @fun a (ha : f a = g a) => by simpa only [← map_star] using congrArg star ha }
+-- Porting note: much like `StarSubalgebra.copy` the old proof was broken and hard to fix
+
+@[simp]
+theorem mem_equalizer (x : A) : x ∈ StarAlgHom.equalizer f g ↔ f x = g x :=
+  Iff.rfl
+
+theorem adjoin_le_equalizer {s : Set A} (h : s.EqOn f g) : adjoin R s ≤ StarAlgHom.equalizer f g :=
+  adjoin_le h
+
+theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃f g : F⦄ (hs : s.EqOn f g) : f = g :=
+  DFunLike.ext f g fun _x => StarAlgHom.adjoin_le_equalizer f g hs <| h.symm ▸ trivial
+
+
+variable [StarModule R B]
+
+theorem map_adjoin (f : A →⋆ₐ[R] B) (s : Set A) :
+    map f (adjoin R s) = adjoin R (f '' s) :=
+  GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarAlgebra.gc
+    StarAlgebra.gc fun _ => rfl
+
 /-- Range of a `StarAlgHom` as a star subalgebra. -/
 protected def range
     (φ : A →⋆ₐ[R] B) : StarSubalgebra R B where
@@ -706,6 +713,9 @@ theorem range_eq_map_top (φ : A →⋆ₐ[R] B) : φ.range = (⊤ : StarSubalge
   StarSubalgebra.ext fun x =>
     ⟨by rintro ⟨a, ha⟩; exact ⟨a, by simp, ha⟩, by rintro ⟨a, -, ha⟩; exact ⟨a, ha⟩⟩
 
+end
+
+variable [StarModule R B]
 /-- Restriction of the codomain of a `StarAlgHom` to a star subalgebra containing the range. -/
 protected def codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ x, f x ∈ S) :
     A →⋆ₐ[R] S where

Mathlib/LinearAlgebra/Dimension/Basic.lean

@@ -66,10 +66,9 @@ lemma nonempty_linearIndependent_set : Nonempty {s : Set M // LinearIndependent
 
 end
 
-variable [Ring R] [Ring R'] [AddCommGroup M] [AddCommGroup M'] [AddCommGroup M₁]
-variable [Module R M] [Module R M'] [Module R M₁] [Module R' M'] [Module R' M₁]
 
 namespace LinearIndependent
+variable [Ring R] [AddCommGroup M] [Module R M]
 
 variable [Nontrivial R]
 
@@ -106,6 +105,10 @@ alias cardinal_le_rank_of_linearIndependent' := LinearIndependent.cardinal_le_ra
 section SurjectiveInjective
 
 section Module
+variable [Ring R] [AddCommGroup M] [Module R M] [Ring R']
+
+section
+variable [AddCommGroup M'] [Module R' M']
 
 /-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map which sends non-zero elements to
 non-zero elements, `j : M →+ M'` is an injective group homomorphism, such that the scalar
@@ -144,6 +147,10 @@ theorem lift_rank_eq_of_equiv_equiv (i : ZeroHom R R') (j : M ≃+ M')
   (lift_rank_le_of_surjective_injective i j hi.2 j.injective hc).antisymm <|
     lift_rank_le_of_injective_injective i j.symm (fun _ _ ↦ hi.1 <| by rwa [i.map_zero])
       j.symm.injective fun _ _ ↦ j.symm_apply_eq.2 <| by erw [hc, j.apply_symm_apply]
+end
+
+section
+variable [AddCommGroup M₁] [Module R' M₁]
 
 /-- The same-universe version of `lift_rank_le_of_injective_injective`. -/
 theorem rank_le_of_injective_injective (i : R' → R) (j : M →+ M₁)
@@ -165,6 +172,7 @@ theorem rank_eq_of_equiv_equiv (i : ZeroHom R R') (j : M ≃+ M₁)
     Module.rank R M = Module.rank R' M₁ := by
   simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hi hc
 
+end
 end Module
 
 namespace Algebra
@@ -208,7 +216,7 @@ theorem lift_rank_eq_of_equiv_equiv (i : R ≃+* R') (j : S ≃+* S')
   simp only [RingEquiv.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe, comp_apply] at this
   simp only [smul_def, RingEquiv.coe_toAddEquiv, map_mul, ZeroHom.coe_coe, this]
 
-variable {S' : Type v} [CommRing R'] [Ring S'] [Algebra R' S']
+variable {S' : Type v} [Ring S'] [Algebra R' S']
 
 /-- The same-universe version of `Algebra.lift_rank_le_of_injective_injective`. -/
 theorem rank_le_of_injective_injective
@@ -234,6 +242,11 @@ end Algebra
 
 end SurjectiveInjective
 
+variable [Ring R] [AddCommGroup M] [Module R M]
+  [Ring R']
+  [AddCommGroup M'] [AddCommGroup M₁]
+  [Module R M'] [Module R M₁] [Module R' M'] [Module R' M₁]
+
 section
 
 theorem LinearMap.lift_rank_le_of_injective (f : M →ₗ[R] M') (i : Injective f) :

Mathlib/LinearAlgebra/Matrix/ToLin.lean

@@ -82,10 +82,10 @@ def Matrix.vecMulLinear [Fintype m] (M : Matrix m n R) : (m → R) →ₗ[R] n 
 theorem Matrix.coe_vecMulLinear [Fintype m] (M : Matrix m n R) :
     (M.vecMulLinear : _ → _) = M.vecMul := rfl
 
-variable [Fintype m] [DecidableEq m]
+variable [Fintype m]
 
 @[simp]
-theorem Matrix.vecMul_stdBasis (M : Matrix m n R) (i j) :
+theorem Matrix.vecMul_stdBasis [DecidableEq m] (M : Matrix m n R) (i j) :
     (LinearMap.stdBasis R (fun _ ↦ R) i 1 ᵥ* M) j = M i j := by
   have : (∑ i', (if i = i' then 1 else 0) * M i' j) = M i j := by
     simp_rw [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true]
@@ -118,6 +118,9 @@ theorem Matrix.vecMul_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R}
     ext j
     simp [vecMul, dotProduct]
 
+section
+variable [DecidableEq m]
+
 /-- Linear maps `(m → R) →ₗ[R] (n → R)` are linearly equivalent over `Rᵐᵒᵖ` to `Matrix m n R`,
 by having matrices act by right multiplication.
  -/
@@ -140,7 +143,7 @@ def LinearMap.toMatrixRight' : ((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ]
 
 /-- A `Matrix m n R` is linearly equivalent over `Rᵐᵒᵖ` to a linear map `(m → R) →ₗ[R] (n → R)`,
 by having matrices act by right multiplication. -/
-abbrev Matrix.toLinearMapRight' : Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] n → R :=
+abbrev Matrix.toLinearMapRight' [DecidableEq m] : Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] n → R :=
   LinearEquiv.symm LinearMap.toMatrixRight'
 
 @[simp]
@@ -180,6 +183,7 @@ def Matrix.toLinearEquivRight'OfInv [Fintype n] [DecidableEq n] {M : Matrix m n
       dsimp only -- Porting note: needed due to non-flat structures
       rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply] }
 
+end
 end ToMatrixRight
 
 /-!
@@ -777,7 +781,7 @@ theorem toMatrix_distrib_mul_action_toLinearMap (x : R) :
     Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
     Pi.single_apply]
 
-lemma LinearMap.toMatrix_prodMap [DecidableEq n] [DecidableEq m] [DecidableEq (n ⊕ m)]
+lemma LinearMap.toMatrix_prodMap [DecidableEq m] [DecidableEq (n ⊕ m)]
     (φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) :
     toMatrix (v₁.prod v₂) (v₁.prod v₂) (φ₁.prodMap φ₂) =
       Matrix.fromBlocks (toMatrix v₁ v₁ φ₁) 0 0 (toMatrix v₂ v₂ φ₂) := by

Mathlib/Topology/AlexandrovDiscrete.lean

@@ -48,7 +48,9 @@ class AlexandrovDiscrete (α : Type*) [TopologicalSpace α] : Prop where
   namespace instead. -/
   protected isOpen_sInter : ∀ S : Set (Set α), (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
 
-variable {ι : Sort*} {κ : ι → Sort*} {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
+variable {ι : Sort*} {κ : ι → Sort*} {α β : Type*}
+section
+variable [TopologicalSpace α] [TopologicalSpace β]
 
 instance DiscreteTopology.toAlexandrovDiscrete [DiscreteTopology α] : AlexandrovDiscrete α where
   isOpen_sInter _ _ := isOpen_discrete _
@@ -153,7 +155,46 @@ lemma IsOpen.exterior_subset_iff (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t
 @[simp] lemma exterior_eq_empty : exterior s = ∅ ↔ s = ∅ :=
   ⟨eq_bot_mono subset_exterior, by rintro rfl; exact exterior_empty⟩
 
-variable [AlexandrovDiscrete α] [AlexandrovDiscrete β]
+lemma Inducing.alexandrovDiscrete [AlexandrovDiscrete α] {f : β → α} (h : Inducing f) :
+    AlexandrovDiscrete β where
+  isOpen_sInter S hS := by
+    simp_rw [h.isOpen_iff] at hS ⊢
+    choose U hU htU using hS
+    refine ⟨_, isOpen_iInter₂ hU, ?_⟩
+    simp_rw [preimage_iInter, htU, sInter_eq_biInter]
+
+lemma IsOpen.exterior_subset (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t :=
+  ⟨subset_exterior.trans, fun h ↦ exterior_minimal h ht⟩
+
+lemma Set.Finite.isCompact_exterior (hs : s.Finite) : IsCompact (exterior s) := by
+  classical
+  refine isCompact_of_finite_subcover fun f hf hsf ↦ ?_
+  choose g hg using fun a (ha : a ∈ exterior s) ↦ mem_iUnion.1 (hsf ha)
+  refine ⟨hs.toFinset.attach.image fun a ↦
+    g a.1 <| subset_exterior <| (Finite.mem_toFinset _).1 a.2,
+    (isOpen_iUnion fun i ↦ isOpen_iUnion ?_).exterior_subset.2 ?_⟩
+  · exact fun _ ↦ hf _
+  refine fun a ha ↦ mem_iUnion₂.2 ⟨_, ?_, hg _ <| subset_exterior ha⟩
+  simp only [Finset.mem_image, Finset.mem_attach, true_and, Subtype.exists, Finite.mem_toFinset]
+  exact ⟨a, ha, rfl⟩
+end
+
+lemma AlexandrovDiscrete.sup {t₁ t₂ : TopologicalSpace α} (_ : @AlexandrovDiscrete α t₁)
+    (_ : @AlexandrovDiscrete α t₂) :
+    @AlexandrovDiscrete α (t₁ ⊔ t₂) :=
+  @AlexandrovDiscrete.mk α (t₁ ⊔ t₂) fun _S hS ↦
+    ⟨@isOpen_sInter _ t₁ _ _ fun _s hs ↦ (hS _ hs).1, isOpen_sInter fun _s hs ↦ (hS _ hs).2⟩
+
+lemma alexandrovDiscrete_iSup {t : ι → TopologicalSpace α} (_ : ∀ i, @AlexandrovDiscrete α (t i)) :
+    @AlexandrovDiscrete α (⨆ i, t i) :=
+  @AlexandrovDiscrete.mk α (⨆ i, t i)
+    fun _S hS ↦ isOpen_iSup_iff.2
+      fun i ↦ @isOpen_sInter _ (t i) _ _
+        fun _s hs ↦ isOpen_iSup_iff.1 (hS _ hs) _
+
+section
+variable [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] [AlexandrovDiscrete β]
+  {s t : Set α} {a x y : α}
 
 @[simp] lemma isOpen_exterior : IsOpen (exterior s) := by
   rw [exterior_def]; exact isOpen_sInter fun _ ↦ And.left
@@ -176,9 +217,6 @@ lemma exterior_subset_iff_mem_nhdsSet : exterior s ⊆ t ↔ t ∈ 𝓝ˢ s :=
 lemma exterior_singleton_subset_iff_mem_nhds : exterior {a} ⊆ t ↔ t ∈ 𝓝 a := by
   simp [exterior_subset_iff_mem_nhdsSet]
 
-lemma IsOpen.exterior_subset (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t :=
-  ⟨subset_exterior.trans, fun h ↦ exterior_minimal h ht⟩
-
 lemma gc_exterior_interior : GaloisConnection (exterior : Set α → Set α) interior :=
   fun s t ↦ by simp [exterior_subset_iff, subset_interior_iff]
 
@@ -210,42 +248,11 @@ lemma isOpen_iff_forall_specializes : IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s
   refine ⟨_, fun b hb ↦ hs _ _ ?_ ha, isOpen_exterior, subset_exterior <| mem_singleton _⟩
   rwa [isOpen_exterior.exterior_subset, singleton_subset_iff]
 
-lemma Set.Finite.isCompact_exterior (hs : s.Finite) : IsCompact (exterior s) := by
-  classical
-  refine isCompact_of_finite_subcover fun f hf hsf ↦ ?_
-  choose g hg using fun a (ha : a ∈ exterior s) ↦ mem_iUnion.1 (hsf ha)
-  refine ⟨hs.toFinset.attach.image fun a ↦
-    g a.1 <| subset_exterior <| (Finite.mem_toFinset _).1 a.2,
-    (isOpen_iUnion fun i ↦ isOpen_iUnion ?_).exterior_subset.2 ?_⟩
-  · exact fun _ ↦ hf _
-  refine fun a ha ↦ mem_iUnion₂.2 ⟨_, ?_, hg _ <| subset_exterior ha⟩
-  simp only [Finset.mem_image, Finset.mem_attach, true_and, Subtype.exists, Finite.mem_toFinset]
-  exact ⟨a, ha, rfl⟩
-
-lemma Inducing.alexandrovDiscrete {f : β → α} (h : Inducing f) : AlexandrovDiscrete β where
-  isOpen_sInter S hS := by
-    simp_rw [h.isOpen_iff] at hS ⊢
-    choose U hU htU using hS
-    refine ⟨_, isOpen_iInter₂ hU, ?_⟩
-    simp_rw [preimage_iInter, htU, sInter_eq_biInter]
-
 lemma alexandrovDiscrete_coinduced {β : Type*} {f : α → β} :
     @AlexandrovDiscrete β (coinduced f ‹_›) :=
   @AlexandrovDiscrete.mk β (coinduced f ‹_›) fun S hS ↦ by
     rw [isOpen_coinduced, preimage_sInter]; exact isOpen_iInter₂ hS
 
-lemma AlexandrovDiscrete.sup {t₁ t₂ : TopologicalSpace α} (_ : @AlexandrovDiscrete α t₁)
-    (_ : @AlexandrovDiscrete α t₂) :
-    @AlexandrovDiscrete α (t₁ ⊔ t₂) :=
-  @AlexandrovDiscrete.mk α (t₁ ⊔ t₂) fun _S hS ↦
-    ⟨@isOpen_sInter _ t₁ _ _ fun _s hs ↦ (hS _ hs).1, isOpen_sInter fun _s hs ↦ (hS _ hs).2⟩
-
-lemma alexandrovDiscrete_iSup {t : ι → TopologicalSpace α} (_ : ∀ i, @AlexandrovDiscrete α (t i)) :
-    @AlexandrovDiscrete α (⨆ i, t i) :=
-  @AlexandrovDiscrete.mk α (⨆ i, t i)
-    fun _S hS ↦ isOpen_iSup_iff.2
-      fun i ↦ @isOpen_sInter _ (t i) _ _
-        fun _s hs ↦ isOpen_iSup_iff.1 (hS _ hs) _
 
 instance AlexandrovDiscrete.toFirstCountable : FirstCountableTopology α where
   nhds_generated_countable a := ⟨{exterior {a}}, countable_singleton _, by simp⟩
@@ -267,3 +274,5 @@ instance Sum.instAlexandrovDiscrete : AlexandrovDiscrete (α ⊕ β) :=
 instance Sigma.instAlexandrovDiscrete {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
     [∀ i, AlexandrovDiscrete (π i)] : AlexandrovDiscrete (Σ i, π i) :=
   alexandrovDiscrete_iSup fun _ ↦ alexandrovDiscrete_coinduced
+
+end

Mathlib/Topology/Compactness/SigmaCompact.lean

@@ -183,6 +183,7 @@ instance (priority := 100) sigmaCompactSpace_of_locally_compact_second_countable
   refine SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_
   rwa [sUnion_image]
 
+section
 -- Porting note: doesn't work on the same line
 variable (X)
 variable [SigmaCompactSpace X]
@@ -299,7 +300,7 @@ theorem countable_cover_nhds_of_sigma_compact {f : X → Set X} (hf : ∀ x, f x
   rcases countable_cover_nhdsWithin_of_sigma_compact isClosed_univ fun x _ => hf x with
     ⟨s, -, hsc, hsU⟩
   exact ⟨s, hsc, univ_subset_iff.1 hsU⟩
-
+end
 
 
 
@@ -407,7 +408,7 @@ noncomputable def choice (X : Type*) [TopologicalSpace X] [WeaklyLocallyCompactS
   · refine univ_subset_iff.1 (iUnion_compactCovering X ▸ ?_)
     exact iUnion_mono' fun n => ⟨n + 1, subset_union_right⟩
 
-noncomputable instance [LocallyCompactSpace X] :
+noncomputable instance [SigmaCompactSpace X] [LocallyCompactSpace X] :
     Inhabited (CompactExhaustion X) :=
   ⟨CompactExhaustion.choice X⟩