awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι_1 : Type u_2
E : ι_1 → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι_1) → TopologicalSpace (E i)
inst_2 : (i : ι_1) → AddCommGroup (E i)
inst_3 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ DirectedOn (fun (x1 x2 : Set ((i : ι_1) → E i)) ↦ x1 ⊆ x2) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}

Tactic:
directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union

Premises used: directedOn_of_sup_mem, Bornology.IsVonNBounded.union
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι_1 : Type u_2
E : ι_1 → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι_1) → TopologicalSpace (E i)
inst_2 : (i : ι_1) → AddCommGroup (E i)
inst_3 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ DirectedOn (fun (x1 x2 : Set ((i : ι_1) → E i)) ↦ x1 ⊆ x2) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}

Tactic:
exact directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union

Premises used: directedOn_of_sup_mem
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
⊢ Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F) (𝓝 0)
    (fun (SV : Set ((i : ι) → E i) × Set F) ↦ IsVonNBounded 𝕜 SV.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) SV.2)
    fun (SV : Set ((i : ι) → E i) × Set F) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι) → E i) → F) SV.1 SV.2}

Tactic:
hasBasis_nhds_zero_of_basis (Filter.basis_sets _)

Premises used: setOf, Filter.basis_sets, ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hu : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ ∀ᶠ (f : ContinuousMultilinearMap 𝕜 E F) in 𝓝 0, MapsTo (⇑f : (a : (i : ι) → E i) → F) s U

Tactic:
hasBasis_nhds_zero.mem_of_mem (i := (s, U)) ⟨hs, hu⟩

Premises used: Set.Mem, Filter.Eventually, setOf, ContinuousMultilinearMap.hasBasis_nhds_zero, And.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
h :
  ∀ (c : 𝕜)
    (hc :
      S ⊆
        HSMul.hSMul (β := Set (ContinuousMultilinearMap 𝕜 E F)) c
          {x : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑x : (a : (i : ι) → E i) → F) s U}),
    image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) x) S s ⊆ c • U
⊢ Absorbs 𝕜 U
    (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) x) S s)

Tactic:
filter_upwards [hS (eventually_nhds_zero_mapsTo hs hU)] with c hc

Premises used: ContinuousMultilinearMap.eventually_nhds_zero_mapsTo
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : 𝕜
hc :
  S ⊆
    HSMul.hSMul (β := Set (ContinuousMultilinearMap 𝕜 E F)) c
      {x : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑x : (a : (i : ι) → E i) → F) s U}
h : ∀ x ∈ S, ∀ y ∈ s, Membership.mem (α := F) (c • U) ((x : (a : (i : ι) → E i) → F) y : F)
⊢ image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) x) S s ⊆ c • U

Tactic:
rw [image2_subset_iff]

Premises used: Set.image2_subset_iff
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : 𝕜
hc :
  S ⊆
    HSMul.hSMul (β := Set (ContinuousMultilinearMap 𝕜 E F)) c
      {x : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑x : (a : (i : ι) → E i) → F) s U}
f : ContinuousMultilinearMap 𝕜 E F
hf : f ∈ S
x : (i : ι) → E i
hx : x ∈ s
h :
  ∀ (g : ContinuousMultilinearMap 𝕜 E F)
    (hg :
      Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E F))
        {x : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑x : (a : (i : ι) → E i) → F) s U} g)
    (hf : (fun (x : ContinuousMultilinearMap 𝕜 E F) ↦ c • x) g ∈ S),
    Membership.mem (α := F) (c • U)
      (((fun (x : ContinuousMultilinearMap 𝕜 E F) ↦ c • x) g : (a : (i : ι) → E i) → F) x : F)
⊢ Membership.mem (α := F) (c • U) ((f : (a : (i : ι) → E i) → F) x : F)

Tactic:
rcases hc hf with ⟨g, hg, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : 𝕜
hc :
  S ⊆
    HSMul.hSMul (β := Set (ContinuousMultilinearMap 𝕜 E F)) c
      {x : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑x : (a : (i : ι) → E i) → F) s U}
x : (i : ι) → E i
hx : x ∈ s
g : ContinuousMultilinearMap 𝕜 E F
hg :
  Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E F))
    {x : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑x : (a : (i : ι) → E i) → F) s U} g
hf : (fun (x : ContinuousMultilinearMap 𝕜 E F) ↦ c • x) g ∈ S
⊢ Membership.mem (α := F) (c • U)
    (((fun (x : ContinuousMultilinearMap 𝕜 E F) ↦ c • x) g : (a : (i : ι) → E i) → F) x : F)

Tactic:
smul_mem_smul_set (hg hx)

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
c : 𝕜
hc :
  S ⊆
    HSMul.hSMul (β := Set (ContinuousMultilinearMap 𝕜 E F)) c
      {x : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑x : (a : (i : ι) → E i) → F) s U}
x : (i : ι) → E i
hx : x ∈ s
g : ContinuousMultilinearMap 𝕜 E F
hg :
  Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E F))
    {x : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑x : (a : (i : ι) → E i) → F) s U} g
hf : (fun (x : ContinuousMultilinearMap 𝕜 E F) ↦ c • x) g ∈ S
⊢ Membership.mem (α := F) (c • U)
    (((fun (x : ContinuousMultilinearMap 𝕜 E F) ↦ c • x) g : (a : (i : ι) → E i) → F) x : F)

Tactic:
exact smul_mem_smul_set (hg hx)

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
x x_1 : ContinuousMultilinearMap 𝕜 E₁ F
H :
  ∀ (x_2 : (i : ι) → E i),
    Eq.{u_4 + 1} (α := F)
      (((x + x_1).compContinuousLinearMap (M₁ := E) (M₁' := E₁) f : (a : (i : ι) → E i) → F) x_2 : F)
      ((x.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f + x_1.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f :
            (a : (i : ι) → E i) → F)
          x_2 :
        F)
⊢ (x + x_1).compContinuousLinearMap (M₁ := E) (M₁' := E₁) f =
    x.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f + x_1.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
x x_1 : ContinuousMultilinearMap 𝕜 E₁ F
x_2 : (i : ι) → E i
⊢ Eq.{u_4 + 1} (α := F) (((x + x_1).compContinuousLinearMap (M₁ := E) (M₁' := E₁) f : (a : (i : ι) → E i) → F) x_2 : F)
    ((x.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f + x_1.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f :
          (a : (i : ι) → E i) → F)
        x_2 :
      F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
x : 𝕜
x_1 : ContinuousMultilinearMap 𝕜 E₁ F
H :
  ∀ (x_2 : (i : ι) → E i),
    Eq.{u_4 + 1} (α := F)
      (((x • x_1).compContinuousLinearMap (M₁ := E) (M₁' := E₁) f : (a : (i : ι) → E i) → F) x_2 : F)
      ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
              (x_1.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f) :
            (a : (i : ι) → E i) → F)
          x_2 :
        F)
⊢ (x • x_1).compContinuousLinearMap (M₁ := E) (M₁' := E₁) f =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (x_1.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
x : 𝕜
x_1 : ContinuousMultilinearMap 𝕜 E₁ F
x_2 : (i : ι) → E i
⊢ Eq.{u_4 + 1} (α := F) (((x • x_1).compContinuousLinearMap (M₁ := E) (M₁' := E₁) f : (a : (i : ι) → E i) → F) x_2 : F)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (x_1.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f) :
          (a : (i : ι) → E i) → F)
        x_2 :
      F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun (g : ContinuousMultilinearMap 𝕜 E₁ F) ↦ g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f,
    map_add' := ⋯, map_smul' := ⋯ }
apply :
  Filter.Tendsto (α := ContinuousMultilinearMap 𝕜 E₁ F) (β := ContinuousMultilinearMap 𝕜 E F)
    (⇑aux : (a : ContinuousMultilinearMap 𝕜 E₁ F) → ContinuousMultilinearMap 𝕜 E F) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] aux.toFun

Tactic:
apply continuous_of_tendsto_nhds_zero aux

Premises used: continuous_of_tendsto_nhds_zero
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun (g : ContinuousMultilinearMap 𝕜 E₁ F) ↦ g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f,
    map_add' := ⋯, map_smul' := ⋯ }
rw :
  ∀ (ib : Set ((i : ι) → E i) × Set F),
    IsVonNBounded 𝕜 ib.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) ib.2 →
      ∃ (ia : Set ((i : ι) → E₁ i) × Set F),
        (IsVonNBounded 𝕜 ia.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) ia.2) ∧
          ∀ (x : ContinuousMultilinearMap 𝕜 E₁ F),
            Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E₁ F))
                {f : ContinuousMultilinearMap 𝕜 E₁ F | MapsTo (⇑f : (a : (i : ι) → E₁ i) → F) ia.1 ia.2} x →
              Membership.mem (α := ContinuousMultilinearMap 𝕜 E F) (γ := Set (ContinuousMultilinearMap 𝕜 E F))
                {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι) → E i) → F) ib.1 ib.2}
                ((aux : (a : ContinuousMultilinearMap 𝕜 E₁ F) → ContinuousMultilinearMap 𝕜 E F) x :
                  ContinuousMultilinearMap 𝕜 E F)
⊢ Filter.Tendsto (α := ContinuousMultilinearMap 𝕜 E₁ F) (β := ContinuousMultilinearMap 𝕜 E F)
    (⇑aux : (a : ContinuousMultilinearMap 𝕜 E₁ F) → ContinuousMultilinearMap 𝕜 E F) (𝓝 0) (𝓝 0)

Tactic:
rw [hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero]

Premises used: Filter.HasBasis.tendsto_iff, ContinuousMultilinearMap.hasBasis_nhds_zero
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun (g : ContinuousMultilinearMap 𝕜 E₁ F) ↦ g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f,
    map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set F
hU : IsVonNBounded 𝕜 (U, V).1
hV : Membership.mem (γ := Filter F) (𝓝 0) (U, V).2
φ : ((i : ι) → E i) →L[𝕜] (i : ι) → E₁ i := ContinuousLinearMap.piMap (φ := E) (ψ := E₁) f
⊢ ∃ (ia : Set ((i : ι) → E₁ i) × Set F),
    (IsVonNBounded 𝕜 ia.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) ia.2) ∧
      ∀ (x : ContinuousMultilinearMap 𝕜 E₁ F),
        Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E₁ F))
            {f : ContinuousMultilinearMap 𝕜 E₁ F | MapsTo (⇑f : (a : (i : ι) → E₁ i) → F) ia.1 ia.2} x →
          Membership.mem (α := ContinuousMultilinearMap 𝕜 E F) (γ := Set (ContinuousMultilinearMap 𝕜 E F))
            {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι) → E i) → F) (U, V).1 (U, V).2}
            ((aux : (a : ContinuousMultilinearMap 𝕜 E₁ F) → ContinuousMultilinearMap 𝕜 E F) x :
              ContinuousMultilinearMap 𝕜 E F)

Tactic:
⟨(φ '' U, V), ⟨hU.image φ, hV⟩, fun g hg ↦ hg.comp (mapsTo_image _ _)⟩

Premises used: Set.mapsTo_image, ContinuousLinearMap.toLinearMap, Prod.mk, Prod.fst, Set.MapsTo.comp, And.intro, Exists.intro, Set.image, Bornology.IsVonNBounded.image, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun (g : ContinuousMultilinearMap 𝕜 E₁ F) ↦ g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f,
    map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set F
hU : IsVonNBounded 𝕜 (U, V).1
hV : Membership.mem (γ := Filter F) (𝓝 0) (U, V).2
φ : ((i : ι) → E i) →L[𝕜] (i : ι) → E₁ i := ContinuousLinearMap.piMap (φ := E) (ψ := E₁) f
⊢ ∃ (ia : Set ((i : ι) → E₁ i) × Set F),
    (IsVonNBounded 𝕜 ia.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) ia.2) ∧
      ∀ (x : ContinuousMultilinearMap 𝕜 E₁ F),
        Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E₁ F))
            {f : ContinuousMultilinearMap 𝕜 E₁ F | MapsTo (⇑f : (a : (i : ι) → E₁ i) → F) ia.1 ia.2} x →
          Membership.mem (α := ContinuousMultilinearMap 𝕜 E F) (γ := Set (ContinuousMultilinearMap 𝕜 E F))
            {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι) → E i) → F) (U, V).1 (U, V).2}
            ((aux : (a : ContinuousMultilinearMap 𝕜 E₁ F) → ContinuousMultilinearMap 𝕜 E F) x :
              ContinuousMultilinearMap 𝕜 E F)

Tactic:
exact ⟨(φ '' U, V), ⟨hU.image φ, hV⟩, fun g hg ↦ hg.comp (mapsTo_image _ _)⟩
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst_8 : (i : ι) → TopologicalSpace (E₁ i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : (i : ι) → AddCommGroup (E₁ i)
inst_11 : (i : ι) → Module.{u_1, u_5} 𝕜 (E₁ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (g : ContinuousMultilinearMap 𝕜 E₁ F) ↦
    g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f

Tactic:
map_continuous (compContinuousLinearMapL f)

Premises used: ContinuousMapClass.map_continuous, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.compContinuousLinearMapL
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : T2Space F
⊢ T2Space (ContinuousMultilinearMap 𝕜 E F)

Tactic:
.of_injective_continuous DFunLike.coe_injective continuous_coeFun

Premises used: T2Space.of_injective_continuous, DFunLike.coe_injective, continuous_coeFun
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : T2Space F
⊢ T3Space (ContinuousMultilinearMap 𝕜 E F)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
𝕜' : Type u_5
inst_9 : NontriviallyNormedField 𝕜'
inst_10 : NormedAlgebra 𝕜' 𝕜
inst_11 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_12 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_13 : Module 𝕜' F
inst_14 : IsScalarTower 𝕜' 𝕜 F
⊢ IsEmbedding (X := ContinuousMultilinearMap 𝕜 E F) (Y := ContinuousMultilinearMap 𝕜' E F)
    (restrictScalars 𝕜' (M₁ := E))

Tactic:
letI : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  (isUniformEmbedding_restrictScalars _).isEmbedding

Premises used: IsUniformEmbedding.isEmbedding, ContinuousMultilinearMap.isUniformEmbedding_restrictScalars