-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem continuousSMul [RingHomSurjective σ] [RingHomIsometric σ]
    [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] (𝔖 : Set (Set E))
    (h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S) :
    ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹¹ : NormedField 𝕜₁
inst✝¹⁰ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Tactic:
let φ : (UniformConvergenceCLM σ F 𝔖) →ₗ[𝕜₂] E → F :=
  ⟨⟨DFunLike.coe, fun _ _ => rfl⟩, fun _ _ => rfl⟩

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹¹ : NormedField 𝕜₁
inst✝¹⁰ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
φ : UniformConvergenceCLM σ F 𝔖 →ₗ[𝕜₂] E → F := { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹¹ : NormedField 𝕜₁
inst✝¹⁰ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Tactic:
haveI : UniformAddGroup F := uniformAddGroup_of_addCommGroup

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹¹ : NormedField 𝕜₁
inst✝¹⁰ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹¹ : NormedField 𝕜₁
inst✝¹⁰ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Tactic:
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹¹ : NormedField 𝕜₁
inst✝¹⁰ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹¹ : NormedField 𝕜₁
inst✝¹⁰ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
φ : UniformConvergenceCLM σ F 𝔖 →ₗ[𝕜₂] E → F := { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Tactic:
exact UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜₂ E F (UniformConvergenceCLM σ F 𝔖) φ
  ⟨rfl⟩ fun u s hs => (h𝔖₃ s hs).image u

Result:
no goals