awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ Absorbs 𝕜 U
    (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) x) S s)
have 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
Tactic: filter_upwards [hS (eventually_nhds_zero_mapsTo hs hU)] with c hc
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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}
⊢ image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) x) S s ⊆ c • U
have h : ∀ x ∈ S, ∀ y ∈ s, Membership.mem (α := F) (c • U) ((x : (a : (i : ι) → E i) → F) y : F)
Tactic: rw [image2_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ Membership.mem (α := F) (c • U) ((f : (a : (i : ι) → E i) → F) x : F)
have 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)
Tactic: rcases hc hf with ⟨g, hg, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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 + x_1).compContinuousLinearMap (M₁ := E) (M₁' := E₁) f =
    x.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f + x_1.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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 • x_1).compContinuousLinearMap (M₁ := E) (M₁' := E₁) f =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (x_1.compContinuousLinearMap (M₁ := E) (M₁' := E₁) f)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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' := ⋯ }
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] aux.toFun
have apply : Filter.Tendsto (α := ContinuousMultilinearMap 𝕜 E₁ F) (β := ContinuousMultilinearMap 𝕜 E F)
  (⇑aux : (a : ContinuousMultilinearMap 𝕜 E₁ F) → ContinuousMultilinearMap 𝕜 E F) (𝓝 0) (𝓝 0)
Tactic: apply continuous_of_tendsto_nhds_zero aux
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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' := ⋯ }
⊢ Filter.Tendsto (α := ContinuousMultilinearMap 𝕜 E₁ F) (β := ContinuousMultilinearMap 𝕜 E F)
    (⇑aux : (a : ContinuousMultilinearMap 𝕜 E₁ F) → ContinuousMultilinearMap 𝕜 E F) (𝓝 0) (𝓝 0)
have 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)
Tactic: rw [hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ g.compContinuousMultilinearMap (M₁ := E) (x + x_1) =
    g.compContinuousMultilinearMap (M₁ := E) x + g.compContinuousMultilinearMap (M₁ := E) x_1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ g.compContinuousMultilinearMap (M₁ := E) (x • x_1) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (g.compContinuousMultilinearMap (M₁ := E) x_1)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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' := ⋯ }
⊢ Continuous[ContinuousMultilinearMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace] aux₁.toFun
have apply : Filter.Tendsto (α := ContinuousMultilinearMap 𝕜 E F) (β := ContinuousMultilinearMap 𝕜 E G)
  (⇑aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) (𝓝 0) (𝓝 0)
Tactic: apply continuous_of_tendsto_nhds_zero aux₁
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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' := ⋯ }
⊢ Filter.Tendsto (α := ContinuousMultilinearMap 𝕜 E F) (β := ContinuousMultilinearMap 𝕜 E G)
    (⇑aux₁ : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) (𝓝 0) (𝓝 0)
have 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)
Tactic: rw [ContinuousMultilinearMap.hasBasis_nhds_zero.tendsto_iff
              ContinuousMultilinearMap.hasBasis_nhds_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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)
have refine_1 : Membership.mem (γ := Filter F) (𝓝 0) (U, (⇑g : (a : F) → G) ⁻¹' V).2
Tactic: refine ⟨(U, g ⁻¹' V), ⟨hU, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ ∃ (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)
have 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)
Tactic: refine ⟨(U, g ⁻¹' V), ⟨hU, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ { 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 }
have 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' := sorry, map_smul' := sorry, cont := sorry } :
                (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' := sorry, map_smul' := sorry, cont := sorry :
                    ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G }
                  { toFun := x_1.compContinuousMultilinearMap (M₁ := E), map_add' := sorry, map_smul' := sorry, cont := sorry :
                    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: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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
⊢ { 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 }
have 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' := sorry, map_smul' := sorry, cont := sorry } :
                (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' := sorry, map_smul' := sorry, cont := sorry :
                    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: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
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' := ⋯ }
⊢ Continuous[topologicalSpace, topologicalSpace] aux.toFun
have 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)
Tactic: apply continuous_of_tendsto_nhds_zero aux