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

Mathlib/Algebra/Algebra/Subalgebra/Rank.lean

@@ -23,9 +23,10 @@ open FiniteDimensional
 namespace Subalgebra
 
 variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
-  (A B : Subalgebra R S) [Module.Free R A] [Module.Free R B]
-  [Module.Free A (Algebra.adjoin A (B : Set S))]
-  [Module.Free B (Algebra.adjoin B (A : Set S))]
+  (A B : Subalgebra R S)
+
+section
+variable [Module.Free R A] [Module.Free A (Algebra.adjoin A (B : Set S))]
 
 theorem rank_sup_eq_rank_left_mul_rank_of_free :
     Module.rank R ↥(A ⊔ B) = Module.rank R A * Module.rank A (Algebra.adjoin A (B : Set S)) := by
@@ -40,22 +41,29 @@ theorem rank_sup_eq_rank_left_mul_rank_of_free :
   change _ = Module.rank R ((Algebra.adjoin A (B : Set S)).restrictScalars R)
   rw [Algebra.restrictScalars_adjoin]; rfl
 
-theorem rank_sup_eq_rank_right_mul_rank_of_free :
-    Module.rank R ↥(A ⊔ B) = Module.rank R B * Module.rank B (Algebra.adjoin B (A : Set S)) := by
-  rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]
-
 theorem finrank_sup_eq_finrank_left_mul_finrank_of_free :
     finrank R ↥(A ⊔ B) = finrank R A * finrank A (Algebra.adjoin A (B : Set S)) := by
   simpa only [map_mul] using congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))
 
+theorem finrank_left_dvd_finrank_sup_of_free :
+    finrank R A ∣ finrank R ↥(A ⊔ B) := ⟨_, finrank_sup_eq_finrank_left_mul_finrank_of_free A B⟩
+
+end
+
+section
+variable [Module.Free R B] [Module.Free B (Algebra.adjoin B (A : Set S))]
+
+theorem rank_sup_eq_rank_right_mul_rank_of_free :
+    Module.rank R ↥(A ⊔ B) = Module.rank R B * Module.rank B (Algebra.adjoin B (A : Set S)) := by
+  rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]
+
 theorem finrank_sup_eq_finrank_right_mul_finrank_of_free :
     finrank R ↥(A ⊔ B) = finrank R B * finrank B (Algebra.adjoin B (A : Set S)) := by
   rw [sup_comm, finrank_sup_eq_finrank_left_mul_finrank_of_free]
 
-theorem finrank_left_dvd_finrank_sup_of_free :
-    finrank R A ∣ finrank R ↥(A ⊔ B) := ⟨_, finrank_sup_eq_finrank_left_mul_finrank_of_free A B⟩
-
 theorem finrank_right_dvd_finrank_sup_of_free :
     finrank R B ∣ finrank R ↥(A ⊔ B) := ⟨_, finrank_sup_eq_finrank_right_mul_finrank_of_free A B⟩
 
+end
+
 end Subalgebra

Mathlib/Algebra/Category/Grp/Injective.lean

@@ -8,7 +8,6 @@ import Mathlib.Algebra.EuclideanDomain.Int
 import Mathlib.Algebra.Module.Injective
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.Topology.Instances.AddCircle
-import Mathlib.Topology.Instances.Rat
 
 /-!
 # Injective objects in the category of abelian groups

Mathlib/Algebra/Module/CharacterModule.lean

@@ -7,7 +7,6 @@ Authors: Jujian Zhang, Junyan Xu
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.Grp.Injective
 import Mathlib.Topology.Instances.AddCircle
-import Mathlib.Topology.Instances.Rat
 import Mathlib.LinearAlgebra.Isomorphisms
 
 /-!

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -685,7 +685,7 @@ lemma adjoin_eq_span (s : Set A) :
   rw [adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span]
 
 @[simp]
-lemma span_eq_toSubmodule (s : NonUnitalStarSubalgebra R A) :
+lemma span_eq_toSubmodule {R} [CommSemiring R] [Module R A] (s : NonUnitalStarSubalgebra R A) :
     Submodule.span R (s : Set A) = s.toSubmodule := by
   simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]
 

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

@@ -322,14 +322,16 @@ lemma cfc_cases (P : A → Prop) (a : A) (f : R → R) (h₀ : P 0)
     · rwa [cfc_apply_of_not_continuousOn _ h]
 
 variable (R) in
-lemma cfc_id : cfc (id : R → R) a = a :=
+lemma cfc_id (ha : p a := by cfc_tac) : cfc (id : R → R) a = a :=
   cfc_apply (id : R → R) a ▸ cfcHom_id (p := p) ha
 
 variable (R) in
-lemma cfc_id' : cfc (fun x : R ↦ x) a = a := cfc_id R a
+lemma cfc_id' (ha : p a := by cfc_tac) : cfc (fun x : R ↦ x) a = a := cfc_id R a
 
 /-- The **spectral mapping theorem** for the continuous functional calculus. -/
-lemma cfc_map_spectrum : spectrum R (cfc f a) = f '' spectrum R a := by
+lemma cfc_map_spectrum (ha : p a := by cfc_tac)
+    (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) :
+    spectrum R (cfc f a) = f '' spectrum R a := by
   simp [cfc_apply f a, cfcHom_map_spectrum (p := p)]
 
 lemma cfc_const (r : R) (a : A) (ha : p a := by cfc_tac) :
@@ -372,15 +374,18 @@ lemma eqOn_of_cfc_eq_cfc {f g : R → R} {a : A} (h : cfc f a = cfc g a)
   congrm($(this) ⟨x, hx⟩)
 
 variable {a f g} in
-lemma cfc_eq_cfc_iff_eqOn : cfc f a = cfc g a ↔ (spectrum R a).EqOn f g :=
+lemma cfc_eq_cfc_iff_eqOn (ha : p a := by cfc_tac)
+    (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
+    (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) :
+    cfc f a = cfc g a ↔ (spectrum R a).EqOn f g :=
   ⟨eqOn_of_cfc_eq_cfc, cfc_congr⟩
 
 variable (R)
 
-lemma cfc_one : cfc (1 : R → R) a = 1 :=
+lemma cfc_one (ha : p a := by cfc_tac) : cfc (1 : R → R) a = 1 :=
   cfc_apply (1 : R → R) a ▸ map_one (cfcHom (show p a from ha))
 
-lemma cfc_const_one : cfc (fun _ : R ↦ 1) a = 1 := cfc_one R a
+lemma cfc_const_one (ha : p a := by cfc_tac) : cfc (fun _ : R ↦ 1) a = 1 := cfc_one R a
 
 @[simp]
 lemma cfc_zero : cfc (0 : R → R) a = 0 := by
@@ -488,7 +493,7 @@ lemma cfc_smul_id {S : Type*} [SMul S R] [ContinuousConstSMul S R]
 lemma cfc_const_mul_id (r : R) (a : A) (ha : p a := by cfc_tac) : cfc (r * ·) a = r • a :=
   cfc_smul_id r a
 
-lemma cfc_star_id : cfc (star · : R → R) a = star a := by
+lemma cfc_star_id (ha : p a := by cfc_tac) : cfc (star · : R → R) a = star a := by
   rw [cfc_star .., cfc_id' ..]
 
 section Polynomial
@@ -518,6 +523,19 @@ lemma cfc_polynomial (q : R[X]) (a : A) (ha : p a := by cfc_tac) :
 
 end Polynomial
 
+lemma CFC.eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
+    (ha : p a := by cfc_tac) : a = algebraMap R A r := by
+  simpa [cfc_id R a, cfc_const r a] using
+    cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx
+
+lemma CFC.eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) :
+    a = 0 := by
+  simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec
+
+lemma CFC.eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) :
+    a = 1 := by
+  simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec
+
 variable [UniqueContinuousFunctionalCalculus R A]
 
 lemma cfc_comp (g f : R → R) (a : A) (ha : p a := by cfc_tac)
@@ -569,19 +587,6 @@ lemma cfc_comp_polynomial (q : R[X]) (f : R → R) (a : A)
     cfc (f <| q.eval ·) a = cfc f (aeval a q) := by
   rw [cfc_comp' .., cfc_polynomial ..]
 
-lemma CFC.eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
-    (ha : p a := by cfc_tac) : a = algebraMap R A r := by
-  simpa [cfc_id R a, cfc_const r a] using
-    cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx
-
-lemma CFC.eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) :
-    a = 0 := by
-  simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec
-
-lemma CFC.eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) :
-    a = 1 := by
-  simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec
-
 lemma CFC.spectrum_algebraMap_subset (r : R) : spectrum R (algebraMap R A r) ⊆ {r} := by
   rw [← cfc_const r 0 (cfc_predicate_zero R),
     cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]
@@ -637,7 +642,7 @@ end Basic
 section Inv
 
 variable {R A : Type*} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R]
-variable [TopologicalSemiring R] [ContinuousStar R] [HasContinuousInv₀ R] [TopologicalSpace A]
+variable [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A]
 variable [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p]
 variable (f : R → R) (a : A)
 
@@ -648,6 +653,8 @@ lemma isUnit_cfc_iff (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
 
 alias ⟨_, isUnit_cfc⟩ := isUnit_cfc_iff
 
+variable [HasContinuousInv₀ R]
+
 /-- Bundle `cfc f a` into a unit given a proof that `f` is nonzero on the spectrum of `a`. -/
 @[simps]
 noncomputable def cfcUnits (hf' : ∀ x ∈ spectrum R a, f x ≠ 0)

Mathlib/Analysis/CStarAlgebra/Unitization.lean

@@ -76,7 +76,7 @@ instance CStarRing.instRegularNormedAlgebra : RegularNormedAlgebra 𝕜 E where
 
 section CStarProperty
 
-variable [StarRing 𝕜] [CStarRing 𝕜] [StarModule 𝕜 E]
+variable [StarRing 𝕜] [StarModule 𝕜 E]
 variable {E}
 
 /-- This is the key lemma used to establish the instance `Unitization.instCStarRing`
@@ -122,6 +122,7 @@ theorem Unitization.norm_splitMul_snd_sq (x : Unitization 𝕜 E) :
     simp only [smul_smul, smul_mul_assoc, ← add_assoc, ← mul_assoc, mul_smul_comm]
 
 variable {𝕜}
+variable [CStarRing 𝕜]
 
 /-- The norm on `Unitization 𝕜 E` satisfies the C⋆-property -/
 instance Unitization.instCStarRing : CStarRing (Unitization 𝕜 E) where

Mathlib/Analysis/Normed/Algebra/Unitization.lean

@@ -208,7 +208,8 @@ def uniformEquivProd : (Unitization 𝕜 A) ≃ᵤ (𝕜 × A) :=
 instance instBornology : Bornology (Unitization 𝕜 A) :=
   Bornology.induced <| addEquiv 𝕜 A
 
-theorem uniformEmbedding_addEquiv : UniformEmbedding (addEquiv 𝕜 A) where
+theorem uniformEmbedding_addEquiv {𝕜} [NontriviallyNormedField 𝕜] :
+    UniformEmbedding (addEquiv 𝕜 A) where
   comap_uniformity := rfl
   inj := (addEquiv 𝕜 A).injective
 

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -90,10 +90,9 @@ theorem ContinuousMultilinearMap.continuous_eval {𝕜 ι : Type*} {E : ι → T
 section Seminorm
 
 variable {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E₁ : ι → Type wE₁}
-  {E' : ι' → Type wE'} {G : Type wG} {G' : Type wG'} [Fintype ι]
+  {E' : ι' → Type wE'} {G : Type wG} {G' : Type wG'}
   [Fintype ι'] [NontriviallyNormedField 𝕜] [∀ i, SeminormedAddCommGroup (E i)]
   [∀ i, NormedSpace 𝕜 (E i)] [∀ i, SeminormedAddCommGroup (E₁ i)] [∀ i, NormedSpace 𝕜 (E₁ i)]
-  [∀ i, SeminormedAddCommGroup (E' i)] [∀ i, NormedSpace 𝕜 (E' i)]
   [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G']
 
 /-!
@@ -121,6 +120,8 @@ lemma norm_map_coord_zero (hf : Continuous f) {m : ∀ i, E i} {i : ι} (hi : 
     (forall_update_iff m fun i a ↦ Inseparable a (m i)).2 ⟨hi.symm, fun _ _ ↦ rfl⟩
   simpa only [map_update_zero] using this.symm.map hf
 
+variable [Fintype ι]
+
 theorem bound_of_shell_of_norm_map_coord_zero (hf₀ : ∀ {m i}, ‖m i‖ = 0 → ‖f m‖ = 0)
     {ε : ι → ℝ} {C : ℝ} (hε : ∀ i, 0 < ε i) {c : ι → 𝕜} (hc : ∀ i, 1 < ‖c i‖)
     (hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖)
@@ -297,7 +298,7 @@ defines a normed space structure on `ContinuousMultilinearMap 𝕜 E G`.
 
 namespace ContinuousMultilinearMap
 
-variable (c : 𝕜) (f g : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i)
+variable [Fintype ι] (c : 𝕜) (f g : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i)
 
 theorem bound : ∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
   f.toMultilinearMap.exists_bound_of_continuous f.2
@@ -687,6 +688,8 @@ theorem norm_image_sub_le (m₁ m₂ : ∀ i, E i) :
 
 end ContinuousMultilinearMap
 
+variable [Fintype ι]
+
 /-- If a continuous multilinear map is constructed from a multilinear map via the constructor
 `mkContinuous`, then its norm is bounded by the bound given to the constructor if it is
 nonnegative. -/
@@ -990,6 +993,8 @@ theorem mkContinuousLinear_norm_le (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G')
     (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ C :=
   (mkContinuousLinear_norm_le' f C H).trans_eq (max_eq_left hC)
 
+variable [∀ i, SeminormedAddCommGroup (E' i)] [∀ i, NormedSpace 𝕜 (E' i)]
+
 /-- Given a map `f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)` and an estimate
 `H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖`, upgrade all `MultilinearMap`s in the type to
 `ContinuousMultilinearMap`s. -/
@@ -1157,10 +1162,10 @@ noncomputable def compContinuousLinearMapContinuousMultilinear :
     ContinuousMultilinearMap 𝕜 (fun i ↦ E i →L[𝕜] E₁ i)
       ((ContinuousMultilinearMap 𝕜 E₁ G) →L[𝕜] ContinuousMultilinearMap 𝕜 E G) :=
   @MultilinearMap.mkContinuous 𝕜 ι (fun i ↦ E i →L[𝕜] E₁ i)
-    ((ContinuousMultilinearMap 𝕜 E₁ G) →L[𝕜] ContinuousMultilinearMap 𝕜 E G) _ _
+    ((ContinuousMultilinearMap 𝕜 E₁ G) →L[𝕜] ContinuousMultilinearMap 𝕜 E G) _
     (fun _ ↦ ContinuousLinearMap.toSeminormedAddCommGroup)
     (fun _ ↦ ContinuousLinearMap.toNormedSpace) _ _
-    (compContinuousLinearMapMultilinear 𝕜 E E₁ G) 1
+    (compContinuousLinearMapMultilinear 𝕜 E E₁ G) _ 1
     fun f ↦ by simpa using norm_compContinuousLinearMapL_le G f
 
 variable {𝕜 E E₁}

Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

@@ -84,14 +84,14 @@ end ContinuousLinearMap
 
 namespace LinearMap
 
-variable [RingHomIsometric σ₂₃]
-
 lemma norm_mkContinuous₂_aux (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ)
     (h : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) :
     ‖(f x).mkContinuous (C * ‖x‖) (h x)‖ ≤ max C 0 * ‖x‖ :=
   (mkContinuous_norm_le' (f x) (h x)).trans_eq <| by
     rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
 
+variable [RingHomIsometric σ₂₃]
+
 /-- Create a bilinear map (represented as a map `E →L[𝕜] F →L[𝕜] G`) from the corresponding linear
 map and existence of a bound on the norm of the image. The linear map can be constructed using
 `LinearMap.mk₂`.

Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean

@@ -39,7 +39,7 @@ universe uι u𝕜 uE uF
 
 variable {ι : Type uι} [Fintype ι]
 variable {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜]
-variable {E : ι → Type uE} [∀ i, SeminormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
+variable {E : ι → Type uE} [∀ i, SeminormedAddCommGroup (E i)]
 variable {F : Type uF} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
 
 open scoped TensorProduct
@@ -81,6 +81,8 @@ theorem projectiveSeminormAux_smul (p : FreeAddMonoid (𝕜 × Π i, E i)) (a :
   simp only [Function.comp_apply, norm_mul, smul_eq_mul]
   rw [mul_assoc]
 
+variable [∀ i, NormedSpace 𝕜 (E i)]
+
 theorem bddBelow_projectiveSemiNormAux (x : ⨂[𝕜] i, E i) :
     BddBelow (Set.range (fun (p : lifts x) ↦ projectiveSeminormAux p.1)) := by
   existsi 0

Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

@@ -22,19 +22,18 @@ open GrothendieckTopology
 namespace Equivalence
 
 variable {D : Type*} [Category D]
-variable (e : C ≌ D)
 
 section Coherent
 
 variable [Precoherent C]
 
 /-- `Precoherent` is preserved by equivalence of categories. -/
-theorem precoherent : Precoherent D := e.inverse.reflects_precoherent
+theorem precoherent (e : C ≌ D) : Precoherent D := e.inverse.reflects_precoherent
 
 instance [EssentiallySmall C] :
     Precoherent (SmallModel C) := (equivSmallModel C).precoherent
 
-instance : haveI := precoherent e
+instance (e : C ≌ D) : haveI := precoherent e
     e.inverse.IsDenseSubsite (coherentTopology D) (coherentTopology C) where
   functorPushforward_mem_iff := by
     rw [coherentTopology.eq_induced e.inverse]
@@ -46,15 +45,15 @@ variable (A : Type*) [Category A]
 Equivalent precoherent categories give equivalent coherent toposes.
 -/
 @[simps!]
-def sheafCongrPrecoherent : haveI := e.precoherent
+def sheafCongrPrecoherent (e : C ≌ D) : haveI := e.precoherent
     Sheaf (coherentTopology C) A ≌ Sheaf (coherentTopology D) A := e.sheafCongr _ _ _
 
 open Presheaf
 
 /--
 The coherent sheaf condition can be checked after precomposing with the equivalence.
 -/
-theorem precoherent_isSheaf_iff (F : Cᵒᵖ ⥤ A) : haveI := e.precoherent
+theorem precoherent_isSheaf_iff (e : C ≌ D) (F : Cᵒᵖ ⥤ A) : haveI := e.precoherent
     IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology D) (e.inverse.op ⋙ F) := by
   refine ⟨fun hF ↦ ((e.sheafCongrPrecoherent A).functor.obj ⟨F, hF⟩).cond, fun hF ↦ ?_⟩
   rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]
@@ -77,12 +76,12 @@ section Regular
 variable [Preregular C]
 
 /-- `Preregular` is preserved by equivalence of categories. -/
-theorem preregular : Preregular D := e.inverse.reflects_preregular
+theorem preregular (e : C ≌ D) : Preregular D := e.inverse.reflects_preregular
 
 instance [EssentiallySmall C] :
     Preregular (SmallModel C) := (equivSmallModel C).preregular
 
-instance : haveI := preregular e
+instance (e : C ≌ D) : haveI := preregular e
     e.inverse.IsDenseSubsite (regularTopology D) (regularTopology C) where
   functorPushforward_mem_iff := by
     rw [regularTopology.eq_induced e.inverse]
@@ -94,15 +93,15 @@ variable (A : Type*) [Category A]
 Equivalent preregular categories give equivalent regular toposes.
 -/
 @[simps!]
-def sheafCongrPreregular : haveI := e.preregular
+def sheafCongrPreregular (e : C ≌ D) : haveI := e.preregular
     Sheaf (regularTopology C) A ≌ Sheaf (regularTopology D) A := e.sheafCongr _ _ _
 
 open Presheaf
 
 /--
 The regular sheaf condition can be checked after precomposing with the equivalence.
 -/
-theorem preregular_isSheaf_iff (F : Cᵒᵖ ⥤ A) : haveI := e.preregular
+theorem preregular_isSheaf_iff (e : C ≌ D) (F : Cᵒᵖ ⥤ A) : haveI := e.preregular
     IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F) := by
   refine ⟨fun hF ↦ ((e.sheafCongrPreregular A).functor.obj ⟨F, hF⟩).cond, fun hF ↦ ?_⟩
   rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]

Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

@@ -49,8 +49,8 @@ variable {k P₁ P₂ P₃ P₄ V₁ V₂ V₃ V₄ : Type*} [Ring k]
   [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂]
   [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃]
   [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄]
-  [TopologicalSpace P₁] [AddCommMonoid P₁] [Module k P₁]
-  [TopologicalSpace P₂] [AddCommMonoid P₂] [Module k P₂]
+  [TopologicalSpace P₁]
+  [TopologicalSpace P₂]
   [TopologicalSpace P₃] [TopologicalSpace P₄]
 
 namespace ContinuousAffineEquiv