-- Mathlib/Topology/Algebra/Module/UniformConvergence.lean
/-- Let `E` be a TVS, `𝔖 : Set (Set α)` and `H` a submodule of `α →ᵤ[𝔖] E`. If the image of any
`S ∈ 𝔖` by any `u ∈ H` is bounded (in the sense of `Bornology.IsVonNBounded`), then `H`,
equipped with the topology of `𝔖`-convergence, is a TVS.

For convenience, we don't literally ask for `H : Submodule (α →ᵤ[𝔖] E)`. Instead, we prove the
result for any vector space `H` equipped with a linear inducing to `α →ᵤ[𝔖] E`, which is often
easier to use. We also state the `Submodule` version as
`UniformOnFun.continuousSMul_submodule_of_image_bounded`. -/
lemma UniformOnFun.continuousSMul_induced_of_image_bounded (φ : hom) (hφ : IsInducing (ofFun 𝔖 ∘ φ))
    (h : ∀ u : H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 ((φ u : α → E) '' s)) :
    ContinuousSMul 𝕜 H

Proof state:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)
φ' : H →ₗ[𝕜] ↑s → E := { toFun := s.restrict ∘ ⇑φ, map_add' := ⋯, map_smul' := ⋯ }
⊢ ContinuousSMul 𝕜 H

Tactic:
refine UniformFun.continuousSMul_induced_of_range_bounded 𝕜 s E H φ' ⟨rfl⟩ fun u ↦ ?_

Result:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)
φ' : H →ₗ[𝕜] ↑s → E := { toFun := s.restrict ∘ ⇑φ, map_add' := ⋯, map_smul' := ⋯ }
u : H
⊢ Bornology.IsVonNBounded 𝕜 (Set.range (φ' u))

Proof state:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousSMul 𝕜 H

Tactic:
letI : TopologicalSpace H :=
  .induced (UniformFun.ofFun ∘ s.restrict ∘ φ) (UniformFun.topologicalSpace s E)

Result:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)
⊢ ContinuousSMul 𝕜 H

Proof state:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)
x y : H
⊢ (s.restrict ∘ ⇑φ) (x + y) = (s.restrict ∘ ⇑φ) x + (s.restrict ∘ ⇑φ) y

Tactic:
exact congr_arg s.restrict (map_add φ x y)

Result:
no goals