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
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)
      ((((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                    ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
                    { 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 := ⋯ } =
    HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
      ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      { 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)
    ((((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
                  ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
                  { 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
-- 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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
apply :
  Filter.Tendsto (α := F →L[𝕜] G) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
    (⇑aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (𝓝 0) (𝓝 0)
⊢ Continuous[topologicalSpace, topologicalSpace] 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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
rw :
  ∀ (ib : Set (ContinuousMultilinearMap 𝕜 E F) × Set ((i : ι) → E i) × Set G),
    IsVonNBounded 𝕜 ib.1 ∧ IsVonNBounded 𝕜 ib.2.1 ∧ Membership.mem (γ := Filter G) (𝓝 0) ib.2.2 →
      ∃ (ia : Prod.{u_4, u_5} (Set F) (Set G)),
        (IsVonNBounded 𝕜 ia.1 ∧ Membership.mem (γ := Filter G) (𝓝 0) ia.2) ∧
          ∀ (x : F →L[𝕜] G),
            Membership.mem (γ := Set (F →L[𝕜] G))
                {f : F →L[𝕜] G | ∀ x ∈ ia.1, Membership.mem (α := G) ia.2 ((f : (a : F) → G) x : G)} x →
              Membership.mem (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (γ :=
                Set (ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G))
                {f : ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G |
                  ∀ x ∈ ib.1,
                    Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
                      {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) ib.2.1 ib.2.2}
                      ((f : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
                        ContinuousMultilinearMap 𝕜 E G)}
                ((aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) x :
                  ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
⊢ Filter.Tendsto (α := F →L[𝕜] G) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
    (⇑aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (𝓝 0) (𝓝 0)

Tactic:
rw [ContinuousLinearMap.hasBasis_nhds_zero.tendsto_iff <|
        ContinuousLinearMap.hasBasis_nhds_zero_of_basis <|
        ContinuousMultilinearMap.hasBasis_nhds_zero]

Premises used: ContinuousLinearMap.hasBasis_nhds_zero, Filter.HasBasis.tendsto_iff, ContinuousMultilinearMap.hasBasis_nhds_zero, ContinuousLinearMap.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
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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
U : Set (ContinuousMultilinearMap 𝕜 E F)
V : Set ((i : ι) → E i)
W : Set G
hU : IsVonNBounded 𝕜 (U, V, W).1
hV : IsVonNBounded 𝕜 (U, V, W).2.1
hW : Membership.mem (γ := Filter G) (𝓝 0) (U, V, W).2.2
⊢ ∃ (ia : Prod.{u_4, u_5} (Set F) (Set G)),
    (IsVonNBounded 𝕜 ia.1 ∧ Membership.mem (γ := Filter G) (𝓝 0) ia.2) ∧
      ∀ (x : F →L[𝕜] G),
        Membership.mem (γ := Set (F →L[𝕜] G))
            {f : F →L[𝕜] G | ∀ x ∈ ia.1, Membership.mem (α := G) ia.2 ((f : (a : F) → G) x : G)} x →
          Membership.mem (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (γ :=
            Set (ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G))
            {f : ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G |
              ∀ x ∈ (U, V, W).1,
                Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
                  {f : ContinuousMultilinearMap 𝕜 E G |
                    MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V, W).2.1 (U, V, W).2.2}
                  ((f : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
                    ContinuousMultilinearMap 𝕜 E G)}
            ((aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) x :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)

Tactic:
⟨(.image2 (fun f v ↦ f v) U V, W), ⟨?_, hW⟩, ?_⟩

Premises used: Prod.mk, Set.image2, And.intro, Exists.intro
-- 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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
U : Set (ContinuousMultilinearMap 𝕜 E F)
V : Set ((i : ι) → E i)
W : Set G
hU : IsVonNBounded 𝕜 (U, V, W).1
hV : IsVonNBounded 𝕜 (U, V, W).2.1
hW : Membership.mem (γ := Filter G) (𝓝 0) (U, V, W).2.2
⊢ IsVonNBounded.{u_1, u_4} 𝕜 (E := F)
    (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v) U V, W).1

Tactic:
ContinuousMultilinearMap.isVonNBounded_image2_apply hU hV

Premises used: Set.Mem, setOf, ContinuousMultilinearMap.isVonNBounded_image2_apply, Set.image2
-- 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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
U : Set (ContinuousMultilinearMap 𝕜 E F)
V : Set ((i : ι) → E i)
W : Set G
hU : IsVonNBounded 𝕜 (U, V, W).1
hV : IsVonNBounded 𝕜 (U, V, W).2.1
hW : Membership.mem (γ := Filter G) (𝓝 0) (U, V, W).2.2
⊢ IsVonNBounded.{u_1, u_4} 𝕜 (E := F)
    (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v) U V, W).1

Tactic:
exact ContinuousMultilinearMap.isVonNBounded_image2_apply hU hV

Premises used: ContinuousMultilinearMap.isVonNBounded_image2_apply
-- 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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
U : Set (ContinuousMultilinearMap 𝕜 E F)
V : Set ((i : ι) → E i)
W : Set G
hU : IsVonNBounded 𝕜 (U, V, W).1
hV : IsVonNBounded 𝕜 (U, V, W).2.1
hW : Membership.mem (γ := Filter G) (𝓝 0) (U, V, W).2.2
⊢ ∀ (x : F →L[𝕜] G),
    Membership.mem (γ := Set (F →L[𝕜] G))
        {f : F →L[𝕜] G |
          ∀ (x : F),
            Membership.mem (γ := Set F)
                (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v)
                      U V,
                    W).1
                x →
              Membership.mem (α := G)
                (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v)
                      U V,
                    W).2
                ((f : (a : F) → G) x : G)}
        x →
      Membership.mem (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (γ :=
        Set (ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G))
        {f : ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G |
          ∀ x ∈ (U, V, W).1,
            Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
              {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V, W).2.1 (U, V, W).2.2}
              ((f : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
                ContinuousMultilinearMap 𝕜 E G)}
        ((aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) x :
          ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)

Tactic:
fun g hg f hf m hm ↦ hg _ <| mem_image2_of_mem hf hm

Premises used: Set.Mem, setOf, ContinuousMultilinearMap.toMultilinearMap, Set.MapsTo, Set.mem_image2_of_mem, 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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
U : Set (ContinuousMultilinearMap 𝕜 E F)
V : Set ((i : ι) → E i)
W : Set G
hU : IsVonNBounded 𝕜 (U, V, W).1
hV : IsVonNBounded 𝕜 (U, V, W).2.1
hW : Membership.mem (γ := Filter G) (𝓝 0) (U, V, W).2.2
⊢ ∀ (x : F →L[𝕜] G),
    Membership.mem (γ := Set (F →L[𝕜] G))
        {f : F →L[𝕜] G |
          ∀ (x : F),
            Membership.mem (γ := Set F)
                (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v)
                      U V,
                    W).1
                x →
              Membership.mem (α := G)
                (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v)
                      U V,
                    W).2
                ((f : (a : F) → G) x : G)}
        x →
      Membership.mem (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (γ :=
        Set (ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G))
        {f : ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G |
          ∀ x ∈ (U, V, W).1,
            Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
              {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V, W).2.1 (U, V, W).2.2}
              ((f : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
                ContinuousMultilinearMap 𝕜 E G)}
        ((aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) x :
          ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)

Tactic:
exact fun g hg f hf m hm ↦ hg _ <| mem_image2_of_mem hf hm
-- 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
f : ContinuousMultilinearMap 𝕜 E F
⊢ (((compContinuousMultilinearMapL 𝕜 E F G :
              (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
            g :
          ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) :
        (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G)
      f =
    g.compContinuousMultilinearMap (M₁ := E) f

Tactic:
rfl

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, rfl
-- 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
⊢ Continuous[ContinuousMultilinearMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (g.compContinuousMultilinearMap (M₁ := E))

Tactic:
map_continuous (compContinuousMultilinearMapL 𝕜 E F G g)

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, ContinuousMapClass.map_continuous, DFunLike.coe, ContinuousLinearMap.compContinuousMultilinearMapL
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
f : (i : ι) → ContinuousLinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ F
H :
  ∀ (x : (i : ι) → E₁ i),
    Eq.{u_5 + 1} (α := F)
      ((((ContinuousMultilinearMap.compContinuousLinearMapL (E := E₁) (E₁ := E) fun (i : ι) ↦
                    (↑(f i).symm : E₁ i →L[𝕜] E i) :
                  (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E₁ F)
                (AddHom.toFun
                  (LinearMap.toAddHom
                      ((↑(ContinuousMultilinearMap.compContinuousLinearMapL (E := E) (E₁ := E₁) fun (i : ι) ↦
                              (↑(f i) : E i →L[𝕜] E₁ i)) :
                          ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                        ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                    ContinuousMultilinearMap 𝕜 E₁ F →ₙ+ ContinuousMultilinearMap 𝕜 E F)
                  g) :
              ContinuousMultilinearMap 𝕜 E₁ F) :
            (a : (i : ι) → E₁ i) → F)
          x :
        F)
      ((g : (a : (i : ι) → E₁ i) → F) x : F)
⊢ (ContinuousMultilinearMap.compContinuousLinearMapL (E := E₁) (E₁ := E) fun (i : ι) ↦ (↑(f i).symm : E₁ i →L[𝕜] E i) :
        (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E₁ F)
      (AddHom.toFun
        (LinearMap.toAddHom
            ((↑(ContinuousMultilinearMap.compContinuousLinearMapL (E := E) (E₁ := E₁) fun (i : ι) ↦
                    (↑(f i) : E i →L[𝕜] E₁ i)) :
                ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
              ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
          ContinuousMultilinearMap 𝕜 E₁ F →ₙ+ ContinuousMultilinearMap 𝕜 E F)
        g) =
    g

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
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 : (i : ι) → TopologicalSpace (E₁ i)
inst_5 : (i : ι) → AddCommGroup (E₁ i)
inst_6 : (i : ι) → Module.{u_1, u_4} 𝕜 (E₁ i)
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
f : (i : ι) → ContinuousLinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ F
x : (i : ι) → E₁ i
⊢ Eq.{u_5 + 1} (α := F)
    ((((ContinuousMultilinearMap.compContinuousLinearMapL (E := E₁) (E₁ := E) fun (i : ι) ↦
                  (↑(f i).symm : E₁ i →L[𝕜] E i) :
                (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E₁ F)
              (AddHom.toFun
                (LinearMap.toAddHom
                    ((↑(ContinuousMultilinearMap.compContinuousLinearMapL (E := E) (E₁ := E₁) fun (i : ι) ↦
                            (↑(f i) : E i →L[𝕜] E₁ i)) :
                        ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                      ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F) :
                  ContinuousMultilinearMap 𝕜 E₁ F →ₙ+ ContinuousMultilinearMap 𝕜 E F)
                g) :
            ContinuousMultilinearMap 𝕜 E₁ F) :
          (a : (i : ι) → E₁ i) → F)
        x :
      F)
    ((g : (a : (i : ι) → E₁ i) → F) x : F)

Tactic:
simp