-- Mathlib/Topology/Algebra/Module/UniformConvergence.lean
/-- Let `E` be a topological vector space over a normed field `𝕜`, let `α` be any type.
Let `H` be a submodule of `α →ᵤ E` such that the range of each `f ∈ H` is von Neumann bounded.
Then `H` is a topological vector space over `𝕜`,
i.e., the pointwise scalar multiplication is continuous in both variables.

For convenience we require that `H` is a vector space over `𝕜`
with a topology induced by `UniformFun.ofFun ∘ φ`, where `φ : H →ₗ[𝕜] (α → E)`. -/
lemma UniformFun.continuousSMul_induced_of_range_bounded (φ : hom)
    (hφ : IsInducing (ofFun ∘ φ)) (h : ∀ u : H, Bornology.IsVonNBounded 𝕜 (Set.range (φ u))) :
    ContinuousSMul 𝕜 H

Proof state:
case hsmul.intro.mk.intro.intro
𝕜 : 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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x => x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun x => x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : (V, W).1 ∈ 𝓝 0
hW : (V, W).2 ∈ 𝓝 0
a : 𝕜
ha : a ∈ V
u : H
hu : u ∈ {u | ∀ (x : α), φ u x ∈ W}
x : α
⊢ (a • φ u) x ∈ U

Tactic:
exact hVW (Set.mk_mem_prod ha (hu x))

Result:
no goals

Proof state:
case hsmul_left
𝕜 : 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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}
c : 𝕜
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x => c • x) (𝓝 0) (𝓝 0)
⊢ ∃ j ∈ 𝓝 0, Set.MapsTo (fun x => c • x) {u | ∀ (x : α), φ u x ∈ j} {u | ∀ (x : α), φ u x ∈ U}

Tactic:
refine ⟨_, this hU, fun u hu x ↦ ?_⟩

Result:
case hsmul_left
𝕜 : 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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}
c : 𝕜
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x => c • x) (𝓝 0) (𝓝 0)
u : H
hu : u ∈ {u | ∀ (x : α), φ u x ∈ (fun x => c • x) ⁻¹' U}
x : α
⊢ φ ((fun x => c • x) u) x ∈ U

Proof state:
case hsmul.intro.mk.intro.intro
𝕜 : 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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x => x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun x => x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : (V, W).1 ∈ 𝓝 0
hW : (V, W).2 ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∃ j ∈ 𝓝 0, V • {u | ∀ (x : α), φ u x ∈ j} ⊆ {u | ∀ (x : α), φ u x ∈ U}

Tactic:
refine ⟨V, hV, W, hW, Set.smul_subset_iff.2 fun a ha u hu x ↦ ?_⟩

Result:
case hsmul.intro.mk.intro.intro
𝕜 : 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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x => x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun x => x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : (V, W).1 ∈ 𝓝 0
hW : (V, W).2 ∈ 𝓝 0
a : 𝕜
ha : a ∈ V
u : H
hu : u ∈ {u | ∀ (x : α), φ u x ∈ W}
x : α
⊢ φ (a • u) x ∈ U

Proof state:
case hsmul_right
𝕜 : 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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}
u : H
U : Set E
hU : U ∈ 𝓝 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, x • u ∈ {u | ∀ (x : α), φ u x ∈ U}

Tactic:
simp only [Set.mem_setOf_eq, map_smul, Pi.smul_apply]

Result:
case hsmul_right
𝕜 : 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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}
u : H
U : Set E
hU : U ∈ 𝓝 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ∀ (x_1 : α), x • φ u x_1 ∈ 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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
⊢ (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}

Tactic:
simp only [hφ.nhds_eq_comap, Function.comp_apply, map_zero]

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✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : UniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
⊢ (comap (⇑ofFun ∘ ⇑φ) (𝓝 (ofFun 0))).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}