Trigger CI for leanprover/lean4#3183

Mathlib/Algebra/Order/Module/Defs.lean

@@ -1091,7 +1091,7 @@ lemma PosSMulMono.lift [PosSMulMono α γ] : PosSMulMono α β where
   elim a ha b₁ b₂ hb := by simp only [← hf, smul] at *; exact smul_le_smul_of_nonneg_left hb ha
 
 lemma PosSMulStrictMono.lift [PosSMulStrictMono α γ] : PosSMulStrictMono α β where
-  elim a ha b₁ b₂ hb :=  by
+  elim a ha b₁ b₂ hb := by
     simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *; exact smul_lt_smul_of_pos_left hb ha
 
 lemma PosSMulReflectLE.lift [PosSMulReflectLE α γ] : PosSMulReflectLE α β where

Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

@@ -519,7 +519,7 @@ noncomputable def coeHom [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [Norme
   map_smul' _ _ := ext _ _ _ _ <| Prod.ext (map_smul _ _ _) (map_smul _ _ _)
   map_zero' := ext _ _ _ _ <| Prod.ext (map_zero _) (map_zero _)
   map_add' _ _ := ext _ _ _ _ <| Prod.ext (map_add _ _ _) (map_add _ _ _)
-  map_mul' _ _ :=  ext _ _ _ _ <| Prod.ext
+  map_mul' _ _ := ext _ _ _ _ <| Prod.ext
     (ContinuousLinearMap.ext fun _ => (mul_assoc _ _ _))
     (ContinuousLinearMap.ext fun _ => (mul_assoc _ _ _).symm)
   map_star' _ := ext _ _ _ _ <| Prod.ext

Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean

@@ -72,7 +72,7 @@ def liftFOne {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : Projectiv
 @[simp]
 theorem liftFOne_zero_comm {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y)
     (Q : ProjectiveResolution Z) :
-    liftFOne f P Q ≫ Q.complex.d 1 0 = P.complex.d 1 0 ≫ liftFZero f P Q :=  by
+    liftFOne f P Q ≫ Q.complex.d 1 0 = P.complex.d 1 0 ≫ liftFZero f P Q := by
   apply Q.exact₀.liftFromProjective_comp
 #align category_theory.ProjectiveResolution.lift_f_one_zero_comm CategoryTheory.ProjectiveResolution.liftFOne_zero_comm
 

Mathlib/CategoryTheory/Pi/Basic.lean

@@ -373,7 +373,7 @@ def Pi.optionEquivalence (C' : Option J → Type u₁) [∀ i, Category.{v₁} (
   inverse := Functor.pi' (fun i => match i with
     | none => Prod.fst _ _
     | some i => Prod.snd _ _ ⋙ (Pi.eval _ i))
-  unitIso :=  NatIso.pi' (fun i => match i with
+  unitIso := NatIso.pi' (fun i => match i with
     | none => Iso.refl _
     | some i => Iso.refl _)
   counitIso := by exact Iso.refl _

Mathlib/Data/Matroid/Dual.lean

@@ -68,7 +68,7 @@ section dual
     exact disjoint_of_subset_left hB''₂.2 disjoint_compl_left
   indep_maximal := by
     rintro X - I'⟨hI'E, B, hB, hI'B⟩ hI'X
-    obtain ⟨I, hI⟩ :=  M.exists_basis (M.E \ X)
+    obtain ⟨I, hI⟩ := M.exists_basis (M.E \ X)
     obtain ⟨B', hB', hIB', hB'IB⟩ := hI.indep.exists_base_subset_union_base hB
     refine' ⟨(X \ B') ∩ M.E,
       ⟨_,subset_inter (subset_diff.mpr _) hI'E, (inter_subset_left _ _).trans (diff_subset _ _)⟩, _⟩

Mathlib/Data/Matroid/IndepAxioms.lean

@@ -127,7 +127,7 @@ attribute [pp_dot] Indep E
     have hfB' : f ∉ B := by (intro hfB; obtain rfl := hf.2 hfB; exact he.2 hf.1)
 
     refine' ⟨f, ⟨hf.1, hfB'⟩, by_contra (fun hnot ↦ _)⟩
-    obtain ⟨x,hxB, hind⟩ :=  M.indep_aug hfB hnot ⟨hB, hBmax⟩
+    obtain ⟨x,hxB, hind⟩ := M.indep_aug hfB hnot ⟨hB, hBmax⟩
     simp only [mem_diff, mem_insert_iff, mem_singleton_iff, not_or, not_and, not_not] at hxB
     obtain rfl := hxB.2.2 hxB.1
     rw [insert_comm, insert_diff_singleton, insert_eq_of_mem he.1] at hind

Mathlib/Data/Nat/Digits.lean

@@ -559,7 +559,7 @@ theorem sub_one_mul_sum_div_pow_eq_sub_sum_digits
           ← Nat.one_add] at ih
         have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
         rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
-        have h₁ : 1 ≤ tl.length :=  List.length_pos.mpr h'
+        have h₁ : 1 ≤ tl.length := List.length_pos.mpr h'
         rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x in Ico _ _, ofDigits p (tl.drop x)),
             ← this, sum_Ico_consecutive _  h₁ <| le_succ tl.length, ← sum_Ico_add _ 0 tl.length 1,
             Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,

Mathlib/Data/Nat/Factorial/SuperFactorial.lean

@@ -102,7 +102,7 @@ theorem superFactorial_dvd_vandermonde_det {n : ℕ} (v : Fin (n + 1) → ℤ) :
   let m := inf' univ ⟨0, mem_univ _⟩ v
   let w' := fun i ↦ (v i - m).toNat
   have hw' : ∀ i, (w' i : ℤ) = v i - m := fun i ↦ Int.toNat_sub_of_le (inf'_le _ (mem_univ _))
-  have h :=  Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde (fun i ↦ ↑(w' i))
+  have h := Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde (fun i ↦ ↑(w' i))
       (fun i => descPochhammer ℤ i)
       (fun i => descPochhammer_natDegree ℤ i)
       (fun i => monic_descPochhammer ℤ i)

Mathlib/Data/Set/Card.lean

@@ -1055,7 +1055,7 @@ theorem one_lt_ncard (hs : s.Finite := by toFinite_tac) :
 #align set.one_lt_ncard Set.one_lt_ncard
 
 theorem one_lt_ncard_iff (hs : s.Finite := by toFinite_tac) :
-    1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=   by
+    1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b := by
   rw [one_lt_ncard hs]
   simp only [exists_prop, exists_and_left]
 #align set.one_lt_ncard_iff Set.one_lt_ncard_iff

Mathlib/Data/Sum/Interval.lean

@@ -147,7 +147,7 @@ lemma mem_sumLexLift :
           (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
             ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂ := by
   constructor
-  · obtain a | a := a <;> obtain b | b :=  b
+  · obtain a | a := a <;> obtain b | b := b
     · rw [sumLexLift, mem_map]
       rintro ⟨c, hc, rfl⟩
       exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩

Mathlib/LinearAlgebra/BilinearForm/Properties.lean

@@ -297,7 +297,7 @@ def isPairSelfAdjointSubmodule : Submodule R₂ (Module.End R₂ M₂) where
 
 @[simp]
 theorem mem_isPairSelfAdjointSubmodule (f : Module.End R₂ M₂) :
-    f ∈ isPairSelfAdjointSubmodule B₂ F₂ ↔ IsPairSelfAdjoint B₂ F₂ f :=  by rfl
+    f ∈ isPairSelfAdjointSubmodule B₂ F₂ ↔ IsPairSelfAdjoint B₂ F₂ f := Iff.rfl
 #align bilin_form.mem_is_pair_self_adjoint_submodule BilinForm.mem_isPairSelfAdjointSubmodule
 
 theorem isPairSelfAdjoint_equiv (e : M₂' ≃ₗ[R₂] M₂) (f : Module.End R₂ M₂) :

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -817,7 +817,7 @@ def associatedHom : QuadraticForm R M →ₗ[S] BilinForm R M :=
   (⟨⅟2, Set.invOf_mem_center (Set.ofNat_mem_center _ _)⟩ : Submonoid.center R) •
     { toFun := polarBilin
       map_add' := fun _x _y => BilinForm.ext <| polar_add _ _
-      map_smul' :=  fun _c _x => BilinForm.ext <| polar_smul _ _ }
+      map_smul' := fun _c _x => BilinForm.ext <| polar_smul _ _ }
 #align quadratic_form.associated_hom QuadraticForm.associatedHom
 
 variable (Q : QuadraticForm R M)

Mathlib/Order/RelSeries.lean

@@ -232,7 +232,7 @@ is another `r`-series
 @[simps]
 def insertNth (p : RelSeries r) (i : Fin p.length) (a : α)
     (prev_connect : r (p (Fin.castSucc i)) a) (connect_next : r a (p i.succ)) : RelSeries r where
-  toFun :=  (Fin.castSucc i.succ).insertNth a p
+  toFun := (Fin.castSucc i.succ).insertNth a p
   step m := by
     set x := _; set y := _; change r x y
     obtain hm | hm | hm := lt_trichotomy m.1 i.1

Mathlib/RingTheory/Ideal/Norm.lean

@@ -253,7 +253,7 @@ noncomputable def Ideal.absNorm [Nontrivial S] [IsDedekindDomain S] [Module.Free
   map_mul' I J := by dsimp only; rw [cardQuot_mul]
   map_one' := by dsimp only; rw [Ideal.one_eq_top, cardQuot_top]
   map_zero' := by
-    have : Infinite S :=  Module.Free.infinite ℤ S
+    have : Infinite S := Module.Free.infinite ℤ S
     rw [Ideal.zero_eq_bot, cardQuot_bot]
 #align ideal.abs_norm Ideal.absNorm
 

Mathlib/RingTheory/Ideal/QuotientOperations.lean

@@ -292,7 +292,7 @@ variable [Algebra R₁ A] [Algebra R₂ A]
 
 /-- The `R₁`-algebra structure on `A/I` for an `R₁`-algebra `A` -/
 instance Quotient.algebra {I : Ideal A} : Algebra R₁ (A ⧸ I) :=
-  { toRingHom :=  (Ideal.Quotient.mk I).comp (algebraMap R₁ A)
+  { toRingHom := (Ideal.Quotient.mk I).comp (algebraMap R₁ A)
     smul_def' := fun _ x =>
       Quotient.inductionOn' x fun _ =>
         ((Quotient.mk I).congr_arg <| Algebra.smul_def _ _).trans (RingHom.map_mul _ _ _)

Mathlib/Tactic/Ring/Basic.lean

@@ -390,7 +390,7 @@ partial def evalMulProd (va : ExProd sα a) (vb : ExProd sα b) : Result (ExProd
       let rc := (NormNum.evalMul.core q($a * $b) q(HMul.hMul) _ _
           q(CommSemiring.toSemiring) ra rb).get!
       let ⟨zc, hc⟩ := rc.toRatNZ.get!
-      let ⟨c, pc⟩ :=  rc.toRawEq
+      let ⟨c, pc⟩ := rc.toRawEq
       ⟨c, .const zc hc, pc⟩
   | .mul (x := a₁) (e := a₂) va₁ va₂ va₃, .const _ _ =>
     let ⟨_, vc, pc⟩ := evalMulProd va₃ vb

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -171,20 +171,24 @@ theorem strongTopology.hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGr
   strongTopology.hasBasis_nhds_zero_of_basis σ F 𝔖 h𝔖₁ h𝔖₂ (𝓝 0).basis_sets
 #align continuous_linear_map.strong_topology.has_basis_nhds_zero ContinuousLinearMap.strongTopology.hasBasis_nhds_zero
 
-theorem strongTopology.continuousConstSMul {M : Type*}
+theorem strongTopology.uniformContinuousConstSMul (M : Type*)
     [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
-    [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E))
-    (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
-    @ContinuousConstSMul M (E →SL[σ] F) (strongTopology σ F 𝔖) _ := by
-  letI := strongTopology σ F 𝔖
-  haveI : TopologicalAddGroup (E →SL[σ] F) := strongTopology.topologicalAddGroup σ F 𝔖
-  refine ⟨fun c ↦ continuous_of_continuousAt_zero (DistribSMul.toAddMonoidHom _ c) ?_⟩
-  have H₁ := strongTopology.hasBasis_nhds_zero σ F _ h𝔖₁ h𝔖₂
-  have H₂ : Filter.Tendsto (c • ·) (𝓝 0 : Filter F) (𝓝 0) :=
-    (continuous_const_smul c).tendsto' 0 _ (smul_zero _)
-  rw [ContinuousAt, map_zero, H₁.tendsto_iff H₁]
-  rintro ⟨s, t⟩ ⟨hs : s ∈ 𝔖, ht : t ∈ 𝓝 0⟩
-  exact ⟨(s, (c • ·) ⁻¹' t), ⟨hs, H₂ ht⟩, fun f  ↦ _root_.id⟩
+    [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) :
+    @UniformContinuousConstSMul M (E →SL[σ] F) (strongUniformity σ F 𝔖) _ :=
+  let _ := strongUniformity σ F 𝔖
+  (strongUniformity.uniformEmbedding_coeFn σ F 𝔖).toUniformInducing.uniformContinuousConstSMul
+    fun _ _ ↦ rfl
+
+theorem strongTopology.continuousConstSMul (M : Type*)
+    [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
+    [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) :
+    @ContinuousConstSMul M (E →SL[σ] F) (strongTopology σ F 𝔖) _ :=
+  let _ := TopologicalAddGroup.toUniformSpace F
+  have _ : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
+  let _ := strongUniformity σ F 𝔖
+  have _ := uniformContinuousConstSMul_of_continuousConstSMul M F
+  have _ := strongTopology.uniformContinuousConstSMul σ F M 𝔖
+  inferInstance
 
 end General
 
@@ -239,12 +243,16 @@ protected theorem hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGroup F
   ContinuousLinearMap.hasBasis_nhds_zero_of_basis (𝓝 0).basis_sets
 #align continuous_linear_map.has_basis_nhds_zero ContinuousLinearMap.hasBasis_nhds_zero
 
+instance uniformContinuousConstSMul
+    {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
+    [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] :
+    UniformContinuousConstSMul M (E →SL[σ] F) :=
+  strongTopology.uniformContinuousConstSMul σ F _ _
+
 instance continuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
     [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] :
     ContinuousConstSMul M (E →SL[σ] F) :=
-  strongTopology.continuousConstSMul σ F {S | Bornology.IsVonNBounded 𝕜₁ S}
-    ⟨∅, Bornology.isVonNBounded_empty 𝕜₁ E⟩
-    (directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union)
+  strongTopology.continuousConstSMul σ F _ _
 
 variable (G) [TopologicalSpace F] [TopologicalSpace G]
 

Mathlib/Topology/Algebra/UniformConvergence.lean

@@ -292,6 +292,22 @@ protected theorem UniformOnFun.hasBasis_nhds_one (𝔖 : Set <| Set α) (h𝔖
 
 end Group
 
+section ConstSMul
+
+variable (M α X : Type*) [SMul M X] [UniformSpace X] [UniformContinuousConstSMul M X]
+
+instance UniformFun.uniformContinuousConstSMul :
+    UniformContinuousConstSMul M (α →ᵤ X) where
+  uniformContinuous_const_smul c := UniformFun.postcomp_uniformContinuous <|
+    uniformContinuous_const_smul c
+
+instance UniformFunOn.uniformContinuousConstSMul {𝔖 : Set (Set α)} :
+    UniformContinuousConstSMul M (α →ᵤ[𝔖] X) where
+  uniformContinuous_const_smul c := UniformOnFun.postcomp_uniformContinuous <|
+    uniformContinuous_const_smul c
+
+end ConstSMul
+
 section Module
 
 variable (𝕜 α E H : Type*) {hom : Type*} [NormedField 𝕜] [AddCommGroup H] [Module 𝕜 H]

Mathlib/Topology/Algebra/UniformMulAction.lean

@@ -99,6 +99,14 @@ theorem UniformContinuous.const_smul [UniformContinuousConstSMul M X] {f : Y →
 #align uniform_continuous.const_smul UniformContinuous.const_smul
 #align uniform_continuous.const_vadd UniformContinuous.const_vadd
 
+@[to_additive]
+lemma UniformInducing.uniformContinuousConstSMul [SMul M Y] [UniformContinuousConstSMul M Y]
+    {f : X → Y} (hf : UniformInducing f) (hsmul : ∀ (c : M) x, f (c • x) = c • f x) :
+    UniformContinuousConstSMul M X where
+  uniformContinuous_const_smul c := by
+    simpa only [hf.uniformContinuous_iff, Function.comp_def, hsmul]
+      using hf.uniformContinuous.const_smul c
+
 /-- If a scalar action is central, then its right action is uniform continuous when its left action
 is. -/
 @[to_additive "If an additive action is central, then its right action is uniform

Mathlib/Topology/PartialHomeomorph.lean

@@ -819,7 +819,7 @@ protected def trans' (h : e.target = e'.source) : PartialHomeomorph α γ where
   toPartialEquiv := PartialEquiv.trans' e.toPartialEquiv e'.toPartialEquiv h
   open_source := e.open_source
   open_target := e'.open_target
-  continuousOn_toFun :=  e'.continuousOn.comp e.continuousOn <| h ▸ e.mapsTo
+  continuousOn_toFun := e'.continuousOn.comp e.continuousOn <| h ▸ e.mapsTo
   continuousOn_invFun := e.continuousOn_symm.comp e'.continuousOn_symm <| h.symm ▸ e'.symm_mapsTo
 #align local_homeomorph.trans' PartialHomeomorph.trans'
 

Mathlib/Topology/UniformSpace/Basic.lean

@@ -1993,7 +1993,7 @@ lemma exists_is_open_mem_uniformity_of_forall_mem_eq
     have B : {z | (g x, g z) ∈ t} ∈ 𝓝 x := (hg x hx).preimage_mem_nhds (mem_nhds_left (g x) ht)
     rcases _root_.mem_nhds_iff.1 (inter_mem A B) with ⟨u, hu, u_open, xu⟩
     refine ⟨u, u_open, xu, fun y hy ↦ ?_⟩
-    have I1 : (f y, f x) ∈ t :=  (htsymm.mk_mem_comm).2 (hu hy).1
+    have I1 : (f y, f x) ∈ t := (htsymm.mk_mem_comm).2 (hu hy).1
     have I2 : (g x, g y) ∈ t := (hu hy).2
     rw [hfg hx] at I1
     exact htr (prod_mk_mem_compRel I1 I2)