awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)

Tactic:
have : Tendsto (fun x : 𝕜 × E ↦ x.1 • x.2) (𝓝 0) (𝓝 0) :=
      continuous_smul.tendsto' _ _ (zero_smul _ _)
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
hsmul :
  ∀ (V : Set 𝕜) (W : Set E) (hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U)
    (hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1) (hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2),
    ∃ (V : Set 𝕜),
      Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
        ∃ (j : Set E),
          Membership.mem (γ := Filter E) (𝓝 0) j ∧
            HSMul.hSMul (β := Set H) V {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)} ⊆
              {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)}
⊢ ∃ (V : Set 𝕜),
    Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
      ∃ (j : Set E),
        Membership.mem (γ := Filter E) (𝓝 0) j ∧
          HSMul.hSMul (β := Set H) V {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)} ⊆
            {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)}

Tactic:
rcases ((Filter.basis_sets _).prod_nhds (Filter.basis_sets _)).tendsto_left_iff.1 this U hU
      with ⟨⟨V, W⟩, ⟨hV, hW⟩, hVW⟩

Premises used: Filter.basis_sets, Filter.HasBasis.prod_nhds, Iff.mp, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1
hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2
⊢ ∃ (V : Set 𝕜),
    Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
      ∃ (j : Set E),
        Membership.mem (γ := Filter E) (𝓝 0) j ∧
          HSMul.hSMul (β := Set H) V {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)} ⊆
            {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)}

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

Premises used: Iff.mpr, Set.smul_subset_iff, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1
hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2
hsmul :
  ∀ (a : 𝕜) (ha : a ∈ V) (u : H)
    (hu : Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) W ((φ : (a : H) → α → E) u x : E)} u)
    (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) (a • u) x : E)
⊢ ∃ (V : Set 𝕜),
    Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
      ∃ (j : Set E),
        Membership.mem (γ := Filter E) (𝓝 0) j ∧
          HSMul.hSMul (β := Set H) V {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)} ⊆
            {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)}

Tactic:
refine ⟨V, hV, W, hW, Set.smul_subset_iff.2 fun a ha u hu x ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1
hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2
a : 𝕜
ha : a ∈ V
u : H
hu : Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) W ((φ : (a : H) → α → E) u x : E)} u
x : α
hsmul : HSMul.hSMul (β := α → E) a ((φ : (a : H) → α → E) u : α → E) x ∈ U
⊢ Membership.mem (α := E) U ((φ : (a : H) → α → E) (a • u) x : E)

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1
hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2
a : 𝕜
ha : a ∈ V
u : H
hu : Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) W ((φ : (a : H) → α → E) u x : E)} u
x : α
⊢ HSMul.hSMul (β := α → E) a ((φ : (a : H) → α → E) u : α → E) x ∈ U

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

Premises used: Set.Mem, Set.mk_mem_prod
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun (x : 𝕜 × E) ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : Membership.mem (γ := Filter 𝕜) (𝓝 0) (V, W).1
hW : Membership.mem (γ := Filter E) (𝓝 0) (V, W).2
a : 𝕜
ha : a ∈ V
u : H
hu : Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) W ((φ : (a : H) → α → E) u x : E)} u
x : α
⊢ HSMul.hSMul (β := α → E) a ((φ : (a : H) → α → E) u : α → E) x ∈ U

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

Premises used: Set.mk_mem_prod
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
c : 𝕜
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Tendsto (β := E) (fun (x : E) ↦ c • x) (𝓝 0) (𝓝 0)

Tactic:
have : Tendsto (c • · : E → E) (𝓝 0) (𝓝 0) :=
      (continuous_const_smul c).tendsto' _ _ (smul_zero _)
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
c : 𝕜
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : E) ↦ c • x) (𝓝 0) (𝓝 0)
⊢ ∃ (j : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) j ∧
      Set.MapsTo (β := H) (fun (x : H) ↦ c • x)
        {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)}
        {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)}

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
c : 𝕜
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : E) ↦ c • x) (𝓝 0) (𝓝 0)
hsmul_left :
  ∀ (u : H)
    (hu :
      Membership.mem (γ := Set H)
        {u : H |
          ∀ (x : α), Membership.mem (α := E) (γ := Set E) ((fun (x : E) ↦ c • x) ⁻¹' U) ((φ : (a : H) → α → E) u x : E)}
        u)
    (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) ((fun (x : H) ↦ c • x) u) x : E)
⊢ ∃ (j : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) j ∧
      Set.MapsTo (β := H) (fun (x : H) ↦ c • x)
        {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)}
        {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)}

Tactic:
refine ⟨_, this hU, fun u hu x ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
c : 𝕜
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : E) ↦ c • x) (𝓝 0) (𝓝 0)
u : H
hu :
  Membership.mem (γ := Set H)
    {u : H |
      ∀ (x : α), Membership.mem (α := E) (γ := Set E) ((fun (x : E) ↦ c • x) ⁻¹' U) ((φ : (a : H) → α → E) u x : E)}
    u
x : α
⊢ Membership.mem (α := E) U ((φ : (a : H) → α → E) ((fun (x : H) ↦ c • x) u) x : E)

Tactic:
simpa only [map_smul] using hu x

Premises used: map_smul
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
u : H
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hsmul_right : ∀ᶠ (x : 𝕜) in 𝓝 0, ∀ (x_1 : α), HSMul.hSMul (β := E) x ((φ : (a : H) → α → E) u x_1 : E) ∈ U
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0,
    Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)} (x • u)

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

Premises used: Set.mem_setOf_eq, map_smul, Pi.smul_apply
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
u : H
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ∀ (x_1 : α), HSMul.hSMul (β := E) x ((φ : (a : H) → α → E) u x_1 : E) ∈ U

Tactic:
simpa only [Set.mapsTo_range_iff] using (h u hU).eventually_nhds_zero (mem_of_mem_nhds hU)

Premises used: Absorbs.eventually_nhds_zero, mem_of_mem_nhds, Set.mapsTo_range_iff
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ[𝔖] E)
    (Function.comp (β := α → E) (⇑(ofFun 𝔖) : (a : α → E) → α →ᵤ[𝔖] E) (⇑φ : (a : H) → α → E))
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
obtain :
  ∀
    (hφ :
      IsInducing (X := H) (Y := α →ᵤ[𝔖] E)
        (Function.comp (β := α → E) (⇑(ofFun 𝔖) : (a : α → E) → α →ᵤ[𝔖] E) (⇑φ : (a : H) → α → E))),
    ContinuousSMul 𝕜 H
⊢ ContinuousSMul 𝕜 H

Tactic:
obtain rfl := hφ.eq_induced

Premises used: Topology.IsInducing.eq_induced, rfl
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
simp : ContinuousSMul 𝕜 H
⊢ ContinuousSMul 𝕜 H

Tactic:
simp +instances only [induced_iInf, UniformOnFun.topologicalSpace_eq, induced_compose]

Premises used: induced_compose, UniformOnFun.topologicalSpace_eq, induced_iInf
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
⊢ ContinuousSMul 𝕜 H

Tactic:
continuousSMul_iInf fun s ↦ continuousSMul_iInf fun hs ↦ ?_

Premises used: continuousSMul_iInf
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
refine : ∀ (s : Set α) (hs : s ∈ 𝔖), ContinuousSMul 𝕜 H
⊢ ContinuousSMul 𝕜 H

Tactic:
refine continuousSMul_iInf fun s ↦ continuousSMul_iInf fun hs ↦ ?_

Premises used: continuousSMul_iInf
-- Module: Mathlib.Topology.Algebra.Module.UniformConvergence
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (Y := UniformFun.{u_2, u_3} (↑s : Type u_2) E)
    (Function.comp (β := (↑s : Type u_2) → E)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E) :
        (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) : H → (↑s : Type u_2) → E))
    (UniformFun.topologicalSpace (↑s : Type u_2) E)
x y : H
⊢ Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) (x + y) =
    HAdd.hAdd (α := (↑s : Type u_2) → E) (β := (↑s : Type u_2) → E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) x : (↑s : Type u_2) → E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) y : (↑s : Type u_2) → E)

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

Premises used: map_add, congr_arg, Set.restrict