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_1 : 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_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
F : Type u_4
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s},
        inst_11.toTopologicalSpace]
      fun (f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) ↦
      (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f m
⊢ IsClosed[(uniformSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}).toTopologicalSpace]
    (⋂ (i : (i : ι) → E i),
      ⋂ (i_1 : ι),
        ⋂ (i_2 : E i_1),
          ⋂ (i_3 : E i_1),
            {x : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
              (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                    (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                  x (update (β := E) i i_1 (i_2 + i_3)) =
                HAdd.hAdd (α := F) (β := F)
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      x (update (β := E) i i_1 i_2) :
                    F)
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      x (update (β := E) i i_1 i_3) :
                    F)})

Tactic:
exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq H (H.add H)

Premises used: isClosed_eq, Continuous.add, isClosed_iInter
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F_1 : 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_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
F : Type u_4
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s},
        inst_11.toTopologicalSpace]
      fun (f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) ↦
      (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f m
⊢ IsClosed[(uniformSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}).toTopologicalSpace]
    (⋂ (i : (i : ι) → E i),
      ⋂ (i_1 : ι),
        ⋂ (i_2 : 𝕜),
          ⋂ (i_3 : E i_1),
            {x : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
              (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                    (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                  x (update (β := E) i i_1 (i_2 • i_3)) =
                HSMul.hSMul (β := F) i_2
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      x (update (β := E) i i_1 i_3) :
                    F)})

Tactic:
isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)

Premises used: isClosed_eq, Continuous.const_smul, isClosed_iInter
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F_1 : 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_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
F : Type u_4
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s},
        inst_11.toTopologicalSpace]
      fun (f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) ↦
      (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f m
⊢ IsClosed[(uniformSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}).toTopologicalSpace]
    (⋂ (i : (i : ι) → E i),
      ⋂ (i_1 : ι),
        ⋂ (i_2 : 𝕜),
          ⋂ (i_3 : E i_1),
            {x : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
              (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                    (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                  x (update (β := E) i i_1 (i_2 • i_3)) =
                HSMul.hSMul (β := F) i_2
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      x (update (β := E) i i_1 i_3) :
                    F)})

Tactic:
exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)

Premises used: isClosed_eq, Continuous.const_smul, isClosed_iInter
-- 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
inst_11 : ∀ (i : ι), IsTopologicalAddGroup.{u_3} (E i)
inst_12 : SequentialSpace ((i : ι) → E i)
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
completeSpace <| .of_seq fun _u x hux ↦ (hux.isVonNBounded_range 𝕜).insert x

Premises used: ContinuousMultilinearMap.completeSpace, Filter.Tendsto.isVonNBounded_range, Bornology.IsVonNBounded.insert, Topology.IsCoherentWith.of_seq
-- 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
x : 𝕜'
hx : 1 < ‖x‖
⊢ 1 < norm.{u_1} (E := 𝕜) ((algebraMap 𝕜' 𝕜 : (a : 𝕜') → 𝕜) x : 𝕜)

Tactic:
simpa
-- 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
rw :
  IsUniformEmbedding (α := ContinuousMultilinearMap 𝕜 E F) (β :=
    ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜' s}] F)
    (comp (β := ContinuousMultilinearMap 𝕜' E F) (toUniformOnFun (E := E)) (restrictScalars 𝕜' (M₁ := E)))
⊢ IsUniformEmbedding (α := ContinuousMultilinearMap 𝕜 E F) (β := ContinuousMultilinearMap 𝕜' E F)
    (restrictScalars 𝕜' (M₁ := E))

Tactic:
rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]

Premises used: ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, IsUniformEmbedding.of_comp_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 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
⊢ IsUniformEmbedding (α := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E))

Tactic:
isUniformEmbedding_toUniformOnFun

Premises used: ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun
-- 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
h : ∀ (s : Set ((i : ι) → E i)), IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s
⊢ IsUniformEmbedding (α := ContinuousMultilinearMap 𝕜 E F) (β :=
    ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜' s}] F)
    (comp (β := ContinuousMultilinearMap 𝕜' E F) (toUniformOnFun (E := E)) (restrictScalars 𝕜' (M₁ := E)))

Tactic:
convert! isUniformEmbedding_toUniformOnFun using 4 with s

Premises used: ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun
-- 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
s : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s

Tactic:
⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩

Premises used: Bornology.IsVonNBounded.restrict_scalars, Bornology.IsVonNBounded.extend_scalars, Iff.intro
-- 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
s : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s

Tactic:
exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩
-- 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : (i : ι) → Module.{u_5, u_3} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_5, u_1, u_3} 𝕜' 𝕜 (E i)
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
⊢ UniformContinuous (α := ContinuousMultilinearMap 𝕜 E F) (β := ContinuousMultilinearMap 𝕜' E F)
    (restrictScalars 𝕜' (M₁ := E))

Tactic:
(isUniformEmbedding_restrictScalars 𝕜').uniformContinuous

Premises used: IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.uniformContinuous, ContinuousMultilinearMap.isUniformEmbedding_restrictScalars
-- 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
⊢ IsTopologicalAddGroup (ContinuousMultilinearMap 𝕜 E F)

Tactic:
letI := IsTopologicalAddGroup.rightUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  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
M : Type u_5
inst_8 : Monoid M
inst_9 : DistribMulAction M F
inst_10 : SMulCommClass 𝕜 M F
inst_11 : ContinuousConstSMul M F
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI := isUniformAddGroup_of_addCommGroup (G := F)
-- 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
M : Type u_5
inst_8 : Monoid M
inst_9 : DistribMulAction M F
inst_10 : SMulCommClass 𝕜 M F
inst_11 : ContinuousConstSMul M F
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Tactic:
infer_instance
-- 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 : ContinuousSMul 𝕜 F
⊢ ContinuousSMul 𝕜 (ContinuousMultilinearMap 𝕜 E F)

Tactic:
letI := IsTopologicalAddGroup.rightUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  let φ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] (Π i, E i) → F :=
    { toFun := (↑), map_add' := fun _ _ ↦ rfl, map_smul' := fun _ _ ↦ rfl }
  UniformOnFun.continuousSMul_induced_of_image_bounded _ _ _ _ φ
    isEmbedding_toUniformOnFun.isInducing fun _ _ hu ↦ hu.image_multilinear _

Premises used: UniformOnFun.continuousSMul_induced_of_image_bounded, ContinuousMultilinearMap, Bornology.IsVonNBounded.image_multilinear, Topology.IsEmbedding.isInducing, ContinuousMultilinearMap.isEmbedding_toUniformOnFun, LinearMap.mk, AddHom.mk, DFunLike.coe, rfl
-- 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 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- 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
rw :
  Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F)
    (Filter.comap (toUniformOnFun (E := E)) (𝓝 (toUniformOnFun (E := E) 0)))
    (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}
⊢ Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F) (𝓝 0)
    (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}

Tactic:
rw [nhds_induced]

Premises used: nhds_induced
-- 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
⊢ Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F)
    (Filter.comap (toUniformOnFun (E := E)) (𝓝 (toUniformOnFun (E := E) 0)))
    (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}

Tactic:
(UniformOnFun.hasBasis_nhds_zero_of_basis _ ?_ ?_ h).comap DFunLike.coe

Premises used: Bornology.IsVonNBounded, Set.Mem, setOf, ContinuousMultilinearMap.toUniformOnFun, instZeroUniformOnFun._aux_1, Filter.HasBasis.comap, Set.preimage, Set.MapsTo, UniformOnFun.hasBasis_nhds_zero_of_basis, UniformOnFun, DFunLike.coe
-- 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
refine_1 : Set.Nonempty (α := Set ((i : ι_1) → E i)) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}
refine_2 : DirectedOn (fun (x1 x2 : Set ((i : ι_1) → E i)) ↦ x1 ⊆ x2) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}
⊢ Filter.HasBasis (α := ContinuousMultilinearMap 𝕜 E F)
    (Filter.comap (toUniformOnFun (E := E)) (𝓝 (toUniformOnFun (E := E) 0)))
    (fun (Si : Set ((i : ι_1) → E i) × ι) ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι_1) → E i) × ι) ↦
    {f : ContinuousMultilinearMap 𝕜 E F | MapsTo (⇑f : (a : (i : ι_1) → E i) → F) Si.1 (b Si.2)}

Tactic:
refine (UniformOnFun.hasBasis_nhds_zero_of_basis _ ?_ ?_ h).comap DFunLike.coe

Premises used: Filter.HasBasis.comap, UniformOnFun.hasBasis_nhds_zero_of_basis, DFunLike.coe
-- 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
⊢ Set.Nonempty (α := Set ((i : ι_1) → E i)) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}

Tactic:
⟨∅, isVonNBounded_empty _ _⟩

Premises used: Bornology.isVonNBounded_empty, Set.Nonempty, Exists.intro, EmptyCollection.emptyCollection
-- 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
⊢ Set.Nonempty (α := Set ((i : ι_1) → E i)) {s : Set ((i : ι_1) → E i) | IsVonNBounded 𝕜 s}

Tactic:
exact ⟨∅, isVonNBounded_empty _ _⟩