[Merged by Bors] - feat: SeparatelyContinuousMul class for multiplication which is continuous in each variable

Mathlib/Analysis/Calculus/Rademacher.lean

@@ -193,11 +193,11 @@ theorem integral_lineDeriv_mul_eq
   simp_rw [_root_.sub_mul, _root_.mul_sub]
   rw [integral_sub, integral_sub, S3]
   · apply Continuous.integrable_of_hasCompactSupport
-    · exact hf.continuous.mul (hg.continuous.comp (continuous_add_right _))
+    · exact hf.continuous.mul (hg.continuous.comp (continuous_add_const _))
     · exact (h'g.comp_homeomorph (Homeomorph.addRight (t • (-v)))).mul_left
   · exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left
   · apply Continuous.integrable_of_hasCompactSupport
-    · exact (hf.continuous.comp (continuous_add_right _)).mul hg.continuous
+    · exact (hf.continuous.comp (continuous_add_const _)).mul hg.continuous
     · exact h'g.mul_left
   · exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left
 

Mathlib/Analysis/Calculus/TangentCone/Basic.lean

@@ -68,7 +68,7 @@ theorem tangentConeAt_mono_nhds (h : 𝓝[s] x ≤ 𝓝[t] x) :
   suffices Tendsto (x + ·) (𝓝[(x + ·) ⁻¹' s] 0) (𝓝[s] x) from
     this.mono_right h |> tendsto_nhdsWithin_iff.mp |>.2
   refine .inf ?_ (mapsTo_preimage _ _).tendsto
-  exact (continuous_add_left x).tendsto' 0 x (add_zero _)
+  exact (continuous_const_add x).tendsto' 0 x (add_zero _)
 
 /-- Tangent cone of `s` at `x` depends only on `𝓝[s] x`. -/
 theorem tangentConeAt_congr (h : 𝓝[s] x = 𝓝[t] x) : tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x :=

Mathlib/Analysis/Complex/Circle.lean

@@ -211,7 +211,7 @@ theorem fourierChar_apply' (x : ℝ) : 𝐞 x = Circle.exp (2 * π * x) := rfl
 theorem fourierChar_apply (x : ℝ) : 𝐞 x = Complex.exp (↑(2 * π * x) * Complex.I) := rfl
 
 @[continuity, fun_prop]
-theorem continuous_fourierChar : Continuous 𝐞 := Circle.exp.continuous.comp (continuous_mul_left _)
+theorem continuous_fourierChar : Continuous 𝐞 := Circle.exp.continuous.comp (continuous_const_mul _)
 
 theorem fourierChar_ne_one : fourierChar ≠ 1 := by
   rw [DFunLike.ne_iff]

Mathlib/Analysis/Complex/HasPrimitives.lean

@@ -203,7 +203,7 @@ private lemma hasDerivAt_wedgeIntegral_re_aux :
   let s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
   have zRe_mem_s : z.re ∈ s := by simp [s, r₁_pos]
   have f_contOn : ContinuousOn (fun (x : ℝ) ↦ f (x + z.im * I)) s :=
-    f_cont.comp ((continuous_add_right _).comp continuous_ofReal).continuousOn <|
+    f_cont.comp ((continuous_add_const _).comp continuous_ofReal).continuousOn <|
       fun _ ↦ mem_ball_re_aux
   have int1 : IntervalIntegrable (fun (x : ℝ) ↦ f (x + z.im * I)) volume z.re z.re :=
     ContinuousOn.intervalIntegrable <| f_contOn.mono <| by simpa

Mathlib/Analysis/Convex/Strict.lean

@@ -195,7 +195,7 @@ variable [AddCancelCommMonoid E] [ContinuousAdd E] [Module 𝕜 E] {s : Set E}
 theorem StrictConvex.preimage_add_right (hs : StrictConvex 𝕜 s) (z : E) :
     StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s) := by
   intro x hx y hy hxy a b ha hb hab
-  refine preimage_interior_subset_interior_preimage (continuous_add_left _) ?_
+  refine preimage_interior_subset_interior_preimage (continuous_const_add _) ?_
   have h := hs hx hy ((add_right_injective _).ne hxy) ha hb hab
   rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
 

Mathlib/Analysis/InnerProductSpace/Completion.lean

@@ -100,7 +100,7 @@ instance innerProductSpace : InnerProductSpace 𝕜 (Completion E) where
   smul_left x y c :=
     Completion.induction_on₂ x y
       (isClosed_eq (Continuous.inner (continuous_fst.const_smul c) continuous_snd)
-        ((continuous_mul_left _).comp (by fun_prop)))
+        ((continuous_const_mul _).comp (by fun_prop)))
       fun a b => by simp only [← coe_smul c a, inner_coe, inner_smul_left]
 
 end UniformSpace.Completion

Mathlib/Analysis/Normed/Field/Lemmas.lean

@@ -317,7 +317,7 @@ lemma NormedField.completeSpace_iff_isComplete_closedBall {K : Type*} [NormedFie
     rw [div_le_one (kpos.trans_lt hx)]
     exact hx.le.trans' (hk (by simp))
   obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'
-  refine ⟨a * x, (((continuous_mul_right x).tendsto a).comp ha').congr ?_⟩
+  refine ⟨a * x, (((continuous_mul_const x).tendsto a).comp ha').congr ?_⟩
   have hx' : x ≠ 0 := by
     contrapose! hx
     simp [hx, kpos]

Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean

@@ -327,7 +327,7 @@ lemma not_continuousAt_weierstrassP (x : ℂ) (hx : x ∈ L.lattice) : ¬ Contin
     (((H.sub ((L.differentiableOn_weierstrassPExcept x).differentiableAt
       (L.compl_lattice_diff_singleton_mem_nhds x)).continuousAt).add
       (continuous_const (y := 1 / x ^ 2)).continuousAt).comp_of_eq
-      (continuous_add_left x).continuousAt (add_zero _) :)
+      (continuous_const_add x).continuousAt (add_zero _) :)
 
 end weierstrassP
 
@@ -679,7 +679,7 @@ lemma summable_weierstrassPExceptSummand (l₀ z x : ℂ)
   -- We first find a `κ > 1`,
   -- such that the ball centered at `x` with radius `κ * ‖z - x‖` does not touch `L`.
   obtain ⟨κ, hκ, hκ'⟩ : ∃ κ : ℝ, 1 < κ ∧ ∀ l : L.lattice, l.1 ≠ l₀ → ‖z - x‖ * κ < ‖l - x‖ := by
-    obtain ⟨κ, hκ, hκ'⟩ := Metric.isOpen_iff.mp ((continuous_mul_right ‖z - x‖).isOpen_preimage _
+    obtain ⟨κ, hκ, hκ'⟩ := Metric.isOpen_iff.mp ((continuous_mul_const ‖z - x‖).isOpen_preimage _
       (isClosedMap_dist x _
       (L.isClosed_of_subset_lattice (Set.diff_subset (t := {l₀})))).upperClosure.isOpen_compl) 1
       (by simpa [Complex.dist_eq, @forall_comm ℝ, norm_sub_rev x] using hx)

Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean

@@ -113,7 +113,7 @@ theorem continuousAt_Gamma_one : ContinuousAt Gamma 1 :=
 theorem tendsto_self_mul_Gamma_nhds_zero : Tendsto (fun z : ℂ => z * Gamma z) (𝓝[≠] 0) (𝓝 1) := by
   rw [show 𝓝 (1 : ℂ) = 𝓝 (Gamma (0 + 1)) by simp only [zero_add, Complex.Gamma_one]]
   refine tendsto_nhdsWithin_congr Gamma_add_one (continuousAt_iff_punctured_nhds.mp ?_)
-  exact ContinuousAt.comp' (by simp [continuousAt_Gamma_one]) (continuous_add_right 1).continuousAt
+  exact ContinuousAt.comp' (by simp [continuousAt_Gamma_one]) (continuous_add_const 1).continuousAt
 
 theorem not_continuousAt_Gamma_zero : ¬ ContinuousAt Gamma 0 :=
   tendsto_self_mul_Gamma_nhds_zero.not_tendsto (by simp) ∘

Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean

@@ -43,7 +43,7 @@ lemma IsMIntegralCurveOn.comp_add (hγ : IsMIntegralCurveOn γ v s) (dt : ℝ) :
   intro t ht
   rw [comp_apply, ← ContinuousLinearMap.comp_id (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))]
   apply HasMFDerivWithinAt.comp t (hγ (t + dt) ht) _ subset_rfl
-  refine ⟨(continuous_add_right _).continuousWithinAt, ?_⟩
+  refine ⟨(continuous_add_const _).continuousWithinAt, ?_⟩
   simp only [mfld_simps]
   exact (hasFDerivWithinAt_id _ _).add_const _
 
@@ -108,7 +108,7 @@ lemma IsMIntegralCurveOn.comp_mul (hγ : IsMIntegralCurveOn γ v s) (a : ℝ) :
   rw [comp_apply, Pi.smul_apply, ← ContinuousLinearMap.one_apply (R₁ := ℝ) a,
     ← ContinuousLinearMap.smulRight_comp_smulRight]
   refine HasMFDerivWithinAt.comp t (hγ (t * a) ht)
-    ⟨(continuous_mul_right _).continuousWithinAt, ?_⟩ subset_rfl
+    ⟨(continuous_mul_const _).continuousWithinAt, ?_⟩ subset_rfl
   simp only [mfld_simps]
   exact HasFDerivWithinAt.mul_const' (hasFDerivWithinAt_id _ _) _
 

Mathlib/MeasureTheory/Group/Measure.lean

@@ -523,13 +523,13 @@ instance innerRegular_map_smul {α} [Monoid α] [MulAction α G] [ContinuousCons
 @[to_additive
 /-- The image of an inner regular measure under left addition is again inner regular. -/]
 instance innerRegular_map_mul_left [IsTopologicalGroup G] [InnerRegular μ] (g : G) :
-    InnerRegular (Measure.map (g * ·) μ) := InnerRegular.map_of_continuous (continuous_mul_left g)
+    InnerRegular (Measure.map (g * ·) μ) := InnerRegular.map_of_continuous (continuous_const_mul g)
 
 /-- The image of an inner regular measure under right multiplication is again inner regular. -/
 @[to_additive
 /-- The image of an inner regular measure under right addition is again inner regular. -/]
 instance innerRegular_map_mul_right [IsTopologicalGroup G] [InnerRegular μ] (g : G) :
-    InnerRegular (Measure.map (· * g) μ) := InnerRegular.map_of_continuous (continuous_mul_right g)
+    InnerRegular (Measure.map (· * g) μ) := InnerRegular.map_of_continuous (continuous_mul_const g)
 
 variable [IsTopologicalGroup G]
 

Mathlib/MeasureTheory/Group/ModularCharacter.lean

@@ -64,7 +64,7 @@ lemma modularCharacterFun_eq_haarScalarFactor [MeasurableSpace G] [BorelSpace G]
   apply NNReal.coe_injective
   have t : (∫ x, f (x * g) ∂ν) = (∫ x, f (x * g) ∂(haarScalarFactor ν μ • μ)) := by
     refine integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport ν μ ?_ ?_
-    · exact Continuous.comp' f_cont (continuous_mul_right g)
+    · exact Continuous.comp' f_cont (continuous_mul_const g)
     · have j : (fun x ↦ f (x * g)) = (f ∘ (Homeomorph.mulRight g)) := rfl
       rw [j]
       exact HasCompactSupport.comp_homeomorph f_comp _

Mathlib/MeasureTheory/Measure/Content.lean

@@ -203,14 +203,14 @@ theorem innerContent_comap (f : G ≃ₜ G) (h : ∀ ⦃K : Compacts G⦄, μ (K
 
 @[to_additive]
 theorem is_mul_left_invariant_innerContent [Group G] [ContinuousMul G]
-    (h : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (g : G)
+    (h : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_const_mul g) = μ K) (g : G)
     (U : Opens G) :
     μ.innerContent (Opens.comap (Homeomorph.mulLeft g) U) = μ.innerContent U := by
   convert μ.innerContent_comap (Homeomorph.mulLeft g) (fun K => h g) U
 
 @[to_additive]
 theorem innerContent_pos_of_is_mul_left_invariant [Group G] [IsTopologicalGroup G]
-    (h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (K : Compacts G)
+    (h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_const_mul g) = μ K) (K : Compacts G)
     (hK : μ K ≠ 0) (U : Opens G) (hU : (U : Set G).Nonempty) : 0 < μ.innerContent U := by
   have : (interior (U : Set G)).Nonempty := by rwa [U.isOpen.interior_eq]
   rcases compact_covered_by_mul_left_translates K.2 this with ⟨s, hs⟩
@@ -292,7 +292,7 @@ theorem outerMeasure_lt_top_of_isCompact [WeaklyLocallyCompactSpace G]
 
 @[to_additive]
 theorem is_mul_left_invariant_outerMeasure [Group G] [ContinuousMul G]
-    (h : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (g : G)
+    (h : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_const_mul g) = μ K) (g : G)
     (A : Set G) : μ.outerMeasure ((g * ·) ⁻¹' A) = μ.outerMeasure A := by
   convert μ.outerMeasure_preimage (Homeomorph.mulLeft g) (fun K => h g) A
 
@@ -306,7 +306,7 @@ theorem outerMeasure_caratheodory (A : Set G) :
 
 @[to_additive]
 theorem outerMeasure_pos_of_is_mul_left_invariant [Group G] [IsTopologicalGroup G]
-    (h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (K : Compacts G)
+    (h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_const_mul g) = μ K) (K : Compacts G)
     (hK : μ K ≠ 0) {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) : 0 < μ.outerMeasure U := by
   convert μ.innerContent_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U
   exact μ.outerMeasure_opens ⟨U, h1U⟩

Mathlib/MeasureTheory/Measure/Haar/Basic.lean

@@ -252,7 +252,7 @@ theorem mul_left_index_le {K : Set G} (hK : IsCompact K) {V : Set G} (hV : (inte
 theorem is_left_invariant_index {K : Set G} (hK : IsCompact K) (g : G) {V : Set G}
     (hV : (interior V).Nonempty) : index ((fun h => g * h) '' K) V = index K V := by
   refine le_antisymm (mul_left_index_le hK hV g) ?_
-  convert mul_left_index_le (hK.image <| continuous_mul_left g) hV g⁻¹
+  convert mul_left_index_le (hK.image <| continuous_const_mul g) hV g⁻¹
   rw [image_image]; symm; convert image_id' _ with h; apply inv_mul_cancel_left
 
 /-!
@@ -307,7 +307,7 @@ theorem prehaar_sup_eq {K₀ : PositiveCompacts G} {U : Set G} {K₁ K₂ : Comp
 @[to_additive]
 theorem is_left_invariant_prehaar {K₀ : PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty)
     (g : G) (K : Compacts G) :
-    prehaar (K₀ : Set G) U (K.map _ <| continuous_mul_left g) = prehaar (K₀ : Set G) U K := by
+    prehaar (K₀ : Set G) U (K.map _ <| continuous_const_mul g) = prehaar (K₀ : Set G) U K := by
   simp only [prehaar, Compacts.coe_map, is_left_invariant_index K.isCompact _ hU]
 
 /-!
@@ -447,8 +447,8 @@ theorem chaar_sup_eq {K₀ : PositiveCompacts G}
 
 @[to_additive is_left_invariant_addCHaar]
 theorem is_left_invariant_chaar {K₀ : PositiveCompacts G} (g : G) (K : Compacts G) :
-    chaar K₀ (K.map _ <| continuous_mul_left g) = chaar K₀ K := by
-  let eval : (Compacts G → ℝ) → ℝ := fun f => f (K.map _ <| continuous_mul_left g) - f K
+    chaar K₀ (K.map _ <| continuous_const_mul g) = chaar K₀ K := by
+  let eval : (Compacts G → ℝ) → ℝ := fun f => f (K.map _ <| continuous_const_mul g) - f K
   have : Continuous eval := (continuous_apply (K.map _ _)).sub (continuous_apply K)
   rw [← sub_eq_zero]; change chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)}
   apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)
@@ -484,7 +484,7 @@ theorem haarContent_self {K₀ : PositiveCompacts G} : haarContent K₀ K₀.toC
 /-- The variant of `is_left_invariant_chaar` for `haarContent` -/
 @[to_additive /-- The variant of `is_left_invariant_addCHaar` for `addHaarContent` -/]
 theorem is_left_invariant_haarContent {K₀ : PositiveCompacts G} (g : G) (K : Compacts G) :
-    haarContent K₀ (K.map _ <| continuous_mul_left g) = haarContent K₀ K := by
+    haarContent K₀ (K.map _ <| continuous_const_mul g) = haarContent K₀ K := by
   simpa only [ENNReal.coe_inj, ← NNReal.coe_inj, haarContent_apply] using
     is_left_invariant_chaar g K
 

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

@@ -835,7 +835,7 @@ theorem tendsto_addHaar_inter_smul_one_of_density_one (s : Set E) (x : E)
   congr 1
   apply measure_toMeasurable_inter_of_sFinite
   simp only [image_add_left, singleton_add]
-  apply (continuous_add_left (-x)).measurable (ht.const_smul₀ r)
+  apply (continuous_const_add (-x)).measurable (ht.const_smul₀ r)
 
 /-- Consider a point `x` at which a set `s` has density one, with respect to closed balls (i.e.,
 a Lebesgue density point of `s`). Then `s` intersects the rescaled copies `{x} + r • t` of a given

Mathlib/NumberTheory/Padics/Complex.lean

@@ -145,7 +145,7 @@ instance : Algebra ℚ_[p] ℂ_[p] where
   algebraMap := (UniformSpace.Completion.coeRingHom).comp (algebraMap ℚ_[p] (PadicAlgCl p))
   commutes' r x := by rw [mul_comm]
   smul_def' r x := by
-    apply UniformSpace.Completion.ext' (continuous_const_smul r) (continuous_mul_left _)
+    apply UniformSpace.Completion.ext' (continuous_const_smul r) (continuous_const_mul _)
     intro a
     rw [RingHom.coe_comp, Function.comp_apply, Algebra.smul_def]
     rfl

Mathlib/Probability/Distributions/Exponential.lean

@@ -164,8 +164,8 @@ lemma lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) :
       · simp only [intervalIntegrable_iff, uIoc_of_le h]
         exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
       · have : Continuous (fun a ↦ rexp (-(r * a))) := by
-          simp only [← neg_mul]; exact (continuous_mul_left (-r)).rexp
-        exact Continuous.continuousOn (Continuous.comp' (continuous_mul_left (-1)) this)
+          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
+        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
       · simp only [neg_mul, one_mul]
         exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
     · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

@@ -477,7 +477,7 @@ instance : Algebra S (v.adicCompletion K) where
   commutes' r x := by
     induction x using Completion.induction_on with
     | hp =>
-      exact isClosed_eq (continuous_mul_left _) (continuous_mul_right _)
+      exact isClosed_eq (continuous_const_mul _) (continuous_mul_const _)
     | ih x =>
       change (↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K) * x
         = x * (↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K)
@@ -486,7 +486,7 @@ instance : Algebra S (v.adicCompletion K) where
   smul_def' r x := by
     induction x using Completion.induction_on with
     | hp =>
-      exact isClosed_eq (continuous_const_smul _) (continuous_mul_left _)
+      exact isClosed_eq (continuous_const_smul _) (continuous_const_mul _)
     | ih x =>
       change _ = (↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K) * x
       norm_cast

Mathlib/Tactic/FunProp/Elab.lean

@@ -132,8 +132,8 @@ might print out
 ```
 Continuous
   continuous_add, args: [4,5], priority: 1000
-  continuous_add_left, args: [5], priority: 1000
-  continuous_add_right, args [4], priority: 1000
+  continuous_const_add, args: [5], priority: 1000
+  continuous_add_const, args [4], priority: 1000
   ...
 Differentiable
   Differentiable.add, args: [4,5], priority: 1000

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -47,7 +47,7 @@ variable {G : Type w} {H : Type x} {α : Type u} {β : Type v}
 
 /-- In a Hausdorff magma with continuous multiplication, the centralizer of any set is closed. -/
 lemma Set.isClosed_centralizer {M : Type*} (s : Set M) [Mul M] [TopologicalSpace M]
-    [ContinuousMul M] [T2Space M] : IsClosed (centralizer s) := by
+    [SeparatelyContinuousMul M] [T2Space M] : IsClosed (centralizer s) := by
   rw [centralizer, setOf_forall]
   refine isClosed_sInter ?_
   rintro - ⟨m, ht, rfl⟩
@@ -63,7 +63,7 @@ In this section we prove a few statements about groups with continuous `(*)`.
 -/
 
 
-variable [TopologicalSpace G] [Group G] [ContinuousMul G]
+variable [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G]
 
 /-- Multiplication from the left in a topological group as a homeomorphism. -/
 @[to_additive /-- Addition from the left in a topological additive group as a homeomorphism. -/]
@@ -411,29 +411,30 @@ instance ConjAct.units_continuousConstSMul {M} [Monoid M] [TopologicalSpace M]
     [ContinuousMul M] : ContinuousConstSMul (ConjAct Mˣ) M :=
   ⟨fun _ => (continuous_const.mul continuous_id).mul continuous_const⟩
 
-variable [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul G]
+variable [TopologicalSpace G] [Inv G] [Mul G]
 
 /-- Conjugation is jointly continuous on `G × G` when both `mul` and `inv` are continuous. -/
 @[to_additive continuous_addConj_prod
   /-- Conjugation is jointly continuous on `G × G` when both `add` and `neg` are continuous. -/]
-theorem IsTopologicalGroup.continuous_conj_prod [ContinuousInv G] :
+theorem IsTopologicalGroup.continuous_conj_prod [ContinuousMul G] [ContinuousInv G] :
     Continuous fun g : G × G => g.fst * g.snd * g.fst⁻¹ :=
   continuous_mul.mul (continuous_inv.comp continuous_fst)
 
 /-- Conjugation by a fixed element is continuous when `mul` is continuous. -/
-@[to_additive (attr := continuity)
+@[to_additive (attr := continuity, fun_prop)
   /-- Conjugation by a fixed element is continuous when `add` is continuous. -/]
-theorem IsTopologicalGroup.continuous_conj (g : G) : Continuous fun h : G => g * h * g⁻¹ :=
-  (continuous_mul_right g⁻¹).comp (continuous_mul_left g)
+theorem IsTopologicalGroup.continuous_conj [SeparatelyContinuousMul G] (g : G) :
+    Continuous fun h : G => g * h * g⁻¹ :=
+  (continuous_mul_const g⁻¹).comp (continuous_const_mul g)
 
 /-- Conjugation acting on fixed element of the group is continuous when both `mul` and
 `inv` are continuous. -/
-@[to_additive (attr := continuity)
+@[to_additive (attr := continuity, fun_prop)
   /-- Conjugation acting on fixed element of the additive group is continuous when both
     `add` and `neg` are continuous. -/]
-theorem IsTopologicalGroup.continuous_conj' [ContinuousInv G] (h : G) :
+theorem IsTopologicalGroup.continuous_conj' [ContinuousMul G] [ContinuousInv G] (h : G) :
     Continuous fun g : G => g * h * g⁻¹ :=
-  (continuous_mul_right h).mul continuous_inv
+  (continuous_mul_const h).mul continuous_inv
 
 end Conj
 
@@ -700,7 +701,7 @@ theorem mul_mem_connectedComponent_one {G : Type*} [TopologicalSpace G] [MulOneC
     (hh : h ∈ connectedComponent (1 : G)) : g * h ∈ connectedComponent (1 : G) := by
   rw [connectedComponent_eq hg]
   have hmul : g ∈ connectedComponent (g * h) := by
-    apply Continuous.image_connectedComponent_subset (continuous_mul_left g)
+    apply Continuous.image_connectedComponent_subset (continuous_const_mul g)
     rw [← connectedComponent_eq hh]
     exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
   simpa [← connectedComponent_eq hmul] using mem_connectedComponent