awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (restrictScalars 𝕜' (M₁ := E))

Tactic:
isEmbedding_restrictScalars.continuous

Premises used: ContinuousMultilinearMap.isEmbedding_restrictScalars, Topology.IsEmbedding.continuous
-- 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 : ContinuousConstSMul 𝕜 F
m : (i : ι) → E i
c : ContinuousMultilinearMap 𝕜 E F
⊢ Eq.{u_4 + 1} (α := F) ((apply 𝕜 E F m : (a : ContinuousMultilinearMap 𝕜 E F) → F) c : F)
    ((c : (a : (i : ι) → E i) → F) m : F)

Tactic:
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 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
α : Type u_5
p : α → ContinuousMultilinearMap 𝕜 E F
q : ContinuousMultilinearMap 𝕜 E F
h : HasSum p q
m : (i : ι) → E i
⊢ HasSum.{u_4, u_5} (α := F) (fun (a : α) ↦ ((p a : (a : (i : ι) → E i) → F) m : F))
    ((q : (a : (i : ι) → E i) → F) m : F)

Tactic:
h.map (applyAddHom m) (continuous_eval_const m)

Premises used: HasSum.map, ContinuousEvalConst.continuous_eval_const, ContinuousMultilinearMap.applyAddHom
-- 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
α : Type u_5
p : α → ContinuousMultilinearMap 𝕜 E F
hp : Summable p
m : (i : ι) → E i
⊢ Eq.{u_4 + 1} (α := F) ((∑' (a : α), p a : (a : (i : ι) → E i) → F) m : F)
    (∑' (a : α), (p a : (a : (i : ι) → E i) → F) m : F)

Tactic:
(hasSum_eval hp.hasSum m).tsum_eq.symm

Premises used: ContinuousMultilinearMap.hasSum_eval, HasSum.tsum_eq, Summable.hasSum, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x x_1 : ContinuousMultilinearMap 𝕜 E F
H :
  ∀ (x_2 : (i : ι) → E i),
    Eq.{u_5 + 1} (α := G) ((g.compContinuousMultilinearMap (M₁ := E) (x + x_1) : (a : (i : ι) → E i) → G) x_2 : G)
      ((g.compContinuousMultilinearMap (M₁ := E) x + g.compContinuousMultilinearMap (M₁ := E) x_1 :
            (a : (i : ι) → E i) → G)
          x_2 :
        G)
⊢ g.compContinuousMultilinearMap (M₁ := E) (x + x_1) =
    g.compContinuousMultilinearMap (M₁ := E) x + g.compContinuousMultilinearMap (M₁ := E) x_1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x x_1 : ContinuousMultilinearMap 𝕜 E F
x_2 : (i : ι) → E i
⊢ Eq.{u_5 + 1} (α := G) ((g.compContinuousMultilinearMap (M₁ := E) (x + x_1) : (a : (i : ι) → E i) → G) x_2 : G)
    ((g.compContinuousMultilinearMap (M₁ := E) x + g.compContinuousMultilinearMap (M₁ := E) x_1 :
          (a : (i : ι) → E i) → G)
        x_2 :
      G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x : 𝕜
x_1 : ContinuousMultilinearMap 𝕜 E F
H :
  ∀ (x_2 : (i : ι) → E i),
    Eq.{u_5 + 1} (α := G) ((g.compContinuousMultilinearMap (M₁ := E) (x • x_1) : (a : (i : ι) → E i) → G) x_2 : G)
      ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (g.compContinuousMultilinearMap (M₁ := E) x_1) :
            (a : (i : ι) → E i) → G)
          x_2 :
        G)
⊢ g.compContinuousMultilinearMap (M₁ := E) (x • x_1) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (g.compContinuousMultilinearMap (M₁ := E) x_1)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x : 𝕜
x_1 : ContinuousMultilinearMap 𝕜 E F
x_2 : (i : ι) → E i
⊢ Eq.{u_5 + 1} (α := G) ((g.compContinuousMultilinearMap (M₁ := E) (x • x_1) : (a : (i : ι) → E i) → G) x_2 : G)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (g.compContinuousMultilinearMap (M₁ := E) x_1) :
          (a : (i : ι) → E i) → G)
        x_2 :
      G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯ }
apply :
  Filter.Tendsto (α := ContinuousMultilinearMap 𝕜 E F) (β := ContinuousMultilinearMap 𝕜 E G)
    (⇑aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) (𝓝 0) (𝓝 0)
⊢ Continuous[ContinuousMultilinearMap.instTopologicalSpace, ContinuousMultilinearMap.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
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯ }
rw :
  ∀ (ib : Set ((i : ι) → E i) × Set G),
    IsVonNBounded 𝕜 ib.1 ∧ Membership.mem (γ := Filter G) (𝓝 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 G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
                {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) ib.1 ib.2}
                ((aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
                  ContinuousMultilinearMap 𝕜 E G)
⊢ Filter.Tendsto (α := ContinuousMultilinearMap 𝕜 E F) (β := ContinuousMultilinearMap 𝕜 E G)
    (⇑aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) (𝓝 0) (𝓝 0)

Tactic:
rw [ContinuousMultilinearMap.hasBasis_nhds_zero.tendsto_iff
              ContinuousMultilinearMap.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
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : Membership.mem (γ := Filter G) (𝓝 0) (U, V).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 G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
            {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V).1 (U, V).2}
            ((aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
              ContinuousMultilinearMap 𝕜 E G)

Tactic:
⟨(U, g ⁻¹' V), ⟨hU, ?_⟩, ?_⟩

Premises used: Prod.mk, Set.preimage, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : Membership.mem (γ := Filter G) (𝓝 0) (U, V).2
refine_1 : Membership.mem (γ := Filter F) (𝓝 0) (U, (⇑g : (a : F) → G) ⁻¹' V).2
refine_2 :
  ∀ (x : ContinuousMultilinearMap 𝕜 E F),
    Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E F))
        {f : ContinuousMultilinearMap 𝕜 E F |
          MapsTo (β := F) (⇑f : (a : (i : ι) → E i) → F) (U, (⇑g : (a : F) → G) ⁻¹' V).1
            (U, (⇑g : (a : F) → G) ⁻¹' V).2}
        x →
      Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
        {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V).1 (U, V).2}
        ((aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
          ContinuousMultilinearMap 𝕜 E G)
⊢ ∃ (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 G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
            {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V).1 (U, V).2}
            ((aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
              ContinuousMultilinearMap 𝕜 E G)

Tactic:
refine ⟨(U, g ⁻¹' V), ⟨hU, ?_⟩, ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : Membership.mem (γ := Filter G) (𝓝 0) (U, V).2
⊢ Membership.mem (γ := Filter G) (𝓝 ((g : (a : F) → G) 0) : Filter G) V

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : Membership.mem (γ := Filter G) (𝓝 0) (U, V).2
⊢ Membership.mem (γ := Filter F) (𝓝 0) (U, (⇑g : (a : F) → G) ⁻¹' V).2

Tactic:
exact (map_continuous g).tendsto 0 <| by simpa

Premises used: Continuous.tendsto, ContinuousMapClass.map_continuous, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : Membership.mem (γ := Filter G) (𝓝 0) (U, V).2
⊢ ∀ (x : ContinuousMultilinearMap 𝕜 E F),
    Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E F))
        {f : ContinuousMultilinearMap 𝕜 E F |
          MapsTo (β := F) (⇑f : (a : (i : ι) → E i) → F) (U, (⇑g : (a : F) → G) ⁻¹' V).1
            (U, (⇑g : (a : F) → G) ⁻¹' V).2}
        x →
      Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
        {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V).1 (U, V).2}
        ((aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
          ContinuousMultilinearMap 𝕜 E G)

Tactic:
fun f hf ↦ hf

Premises used: Set.Mem, setOf, Set.preimage, Set.MapsTo
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : Membership.mem (γ := Filter G) (𝓝 0) (U, V).2
⊢ ∀ (x : ContinuousMultilinearMap 𝕜 E F),
    Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E F))
        {f : ContinuousMultilinearMap 𝕜 E F |
          MapsTo (β := F) (⇑f : (a : (i : ι) → E i) → F) (U, (⇑g : (a : F) → G) ⁻¹' V).1
            (U, (⇑g : (a : F) → G) ⁻¹' V).2}
        x →
      Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
        {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V).1 (U, V).2}
        ((aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
          ContinuousMultilinearMap 𝕜 E G)

Tactic:
exact fun f hf ↦ hf
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
x x_1 : F →L[𝕜] G
h :
  ∀ (x_2 : ContinuousMultilinearMap 𝕜 E F) (x_3 : (i : ι) → E i),
    Eq.{u_5 + 1} (α := G)
      (((({ toFun := (x + x_1).compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                  (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G)
                x_2 :
              ContinuousMultilinearMap 𝕜 E G) :
            (a : (i : ι) → E i) → G)
          x_3 :
        G)
      ((((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                    { toFun := x.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
                      ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G }
                    { toFun := x_1.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
                      ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                  (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G)
                x_2 :
              ContinuousMultilinearMap 𝕜 E G) :
            (a : (i : ι) → E i) → G)
          x_3 :
        G)
⊢ { toFun := (x + x_1).compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
      { toFun := x.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
        ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G }
      { toFun := x_1.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
        ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G }

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
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
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
x x_1 : F →L[𝕜] G
x_2 : ContinuousMultilinearMap 𝕜 E F
x_3 : (i : ι) → E i
⊢ Eq.{u_5 + 1} (α := G)
    (((({ toFun := (x + x_1).compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G)
              x_2 :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        x_3 :
      G)
    ((((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                  { toFun := x.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
                    ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G }
                  { toFun := x_1.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
                    ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G)
              x_2 :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        x_3 :
      G)

Tactic:
simp