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 : UniformSpace F
inst_7 : IsUniformAddGroup F
rw :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F))
    (TopologicalSpace.induced (toUniformOnFun (E := E))
      (UniformOnFun.topologicalSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}))
    UniformSpace.toTopologicalSpace
⊢ Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F)) (instTopologicalSpace (E := E))
    UniformSpace.toTopologicalSpace

Tactic:
rw [instTopologicalSpace, IsUniformAddGroup.rightUniformSpace_eq]

Premises used: IsUniformAddGroup.rightUniformSpace_eq, ContinuousMultilinearMap.instTopologicalSpace
-- 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
⊢ Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F))
    (TopologicalSpace.induced (toUniformOnFun (E := E))
      (UniformOnFun.topologicalSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}))
    UniformSpace.toTopologicalSpace

Tactic:
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 : UniformSpace F
inst_7 : IsUniformAddGroup F
⊢ IsUniformInducing (α := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E))

Tactic:
⟨rfl⟩

Premises used: IsUniformInducing.mk, 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
⊢ IsUniformEmbedding (α := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E))

Tactic:
⟨isUniformInducing_toUniformOnFun, DFunLike.coe_injective⟩

Premises used: IsUniformEmbedding.mk, DFunLike.coe_injective, ContinuousMultilinearMap.isUniformInducing_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
⊢ IsEmbedding (X := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E))

Tactic:
isUniformEmbedding_toUniformOnFun.isEmbedding

Premises used: ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, IsUniformEmbedding.isEmbedding
-- 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)
⊢ UniformContinuous (α := ContinuousMultilinearMap 𝕜 E F) (β := (a : (i : ι) → E i) → F)
    (DFunLike.coe (β := fun (a : (i : ι) → E i) ↦ F))

Tactic:
(UniformOnFun.uniformContinuous_toFun sUnion_isVonNBounded_eq_univ).comp
    isUniformEmbedding_toUniformOnFun.uniformContinuous

Premises used: IsUniformEmbedding.toIsUniformInducing, ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, UniformOnFun.uniformContinuous_toFun, UniformContinuous.comp, Bornology.sUnion_isVonNBounded_eq_univ, IsUniformInducing.uniformContinuous
-- 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)
x : (i : ι) → E i
⊢ UniformContinuous (β := F) fun (f : ContinuousMultilinearMap 𝕜 E F) ↦ (f : (a : (i : ι) → E i) → F) x

Tactic:
uniformContinuous_pi.1 uniformContinuous_coe_fun x

Premises used: ContinuousMultilinearMap.uniformContinuous_coe_fun, uniformContinuous_pi, Iff.mp
-- 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
⊢ IsUniformAddGroup (ContinuousMultilinearMap 𝕜 E F)

Tactic:
let φ : ContinuousMultilinearMap 𝕜 E F →+ (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F :=
    { toFun := toUniformOnFun, map_add' := fun _ _ ↦ rfl, map_zero' := rfl }
  isUniformEmbedding_toUniformOnFun.isUniformAddGroup φ

Premises used: IsUniformInducing.isUniformAddGroup, ContinuousMultilinearMap.toUniformOnFun, IsUniformEmbedding.toIsUniformInducing, AddMonoidHom.mk, ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, ZeroHom.mk, 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
M : Type u_5
inst_8 : Monoid M
inst_9 : DistribMulAction M F
inst_10 : SMulCommClass 𝕜 M F
inst_11 : ContinuousConstSMul M F
⊢ UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Tactic:
haveI := uniformContinuousConstSMul_of_continuousConstSMul M F
  isUniformEmbedding_toUniformOnFun.uniformContinuousConstSMul fun _ _ ↦ rfl

Premises used: IsUniformEmbedding.toIsUniformInducing, ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, IsUniformInducing.uniformContinuousConstSMul, 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : UniformSpace G
inst_10 : IsUniformAddGroup G
inst_11 : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
rw :
  IsUniformInducing (α := ContinuousMultilinearMap 𝕜 E F)
    (toUniformOnFun (E := E) ∘ g.compContinuousMultilinearMap (M₁ := E))
⊢ IsUniformInducing (α := ContinuousMultilinearMap 𝕜 E F) (g.compContinuousMultilinearMap (M₁ := E))

Tactic:
rw [← isUniformInducing_toUniformOnFun.of_comp_iff]

Premises used: IsUniformInducing.of_comp_iff, ContinuousMultilinearMap.isUniformInducing_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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : UniformSpace G
inst_10 : IsUniformAddGroup G
inst_11 : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
⊢ IsUniformInducing (α := ContinuousMultilinearMap 𝕜 E F)
    (toUniformOnFun (E := E) ∘ g.compContinuousMultilinearMap (M₁ := E))

Tactic:
(UniformOnFun.postcomp_isUniformInducing hg).comp isUniformInducing_toUniformOnFun

Premises used: ContinuousMultilinearMap.toUniformOnFun, UniformOnFun.postcomp_isUniformInducing, IsUniformInducing.comp, ContinuousMultilinearMap.isUniformInducing_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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : UniformSpace G
inst_10 : IsUniformAddGroup G
inst_11 : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
⊢ IsUniformInducing (α := ContinuousMultilinearMap 𝕜 E F)
    (toUniformOnFun (E := E) ∘ g.compContinuousMultilinearMap (M₁ := E))

Tactic:
exact (UniformOnFun.postcomp_isUniformInducing hg).comp isUniformInducing_toUniformOnFun

Premises used: UniformOnFun.postcomp_isUniformInducing, IsUniformInducing.comp, ContinuousMultilinearMap.isUniformInducing_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
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
inr :
  ∀
    (this :
      ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
        [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
        CompleteSpace (ContinuousMultilinearMap 𝕜 E F))
    (hF : ¬T2Space F), CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
wlog :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
wlog hF : T2Space F generalizing F

Premises used: T2Space
-- 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
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
inr : CompleteSpace (ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F))
inr₁ :
  Surjective (α := ContinuousMultilinearMap 𝕜 E F) (β :=
    ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F))
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (SeparationQuotient.mkCLM 𝕜 F))
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]

Premises used: ContinuousMultilinearMap.isUniformInducing_postcomp, IsUniformInducing.completeSpace_congr
-- 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
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
⊢ CompleteSpace (ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F))

Tactic:
this 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
⊢ CompleteSpace (ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F))

Tactic:
exact this 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F)
h₁ :
  ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (M₂ := F) (SeparationQuotient.mkCLM 𝕜 F)
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (SeparationQuotient.outCLM 𝕜 F) f) =
    f
⊢ ∃ (a : ContinuousMultilinearMap 𝕜 E F),
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (SeparationQuotient.mkCLM 𝕜 F) a = f

Tactic:
use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, SeparationQuotient.outCLM
-- 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
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F)
⊢ ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (M₂ := F) (SeparationQuotient.mkCLM 𝕜 F)
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) (SeparationQuotient.outCLM 𝕜 F) f) =
    f

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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
⊢ ∀ {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

Tactic:
have H : ∀ {m : Π i, E i},
      Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
    (uniformContinuous_eval (sUnion_isVonNBounded_eq_univ) _).continuous
-- 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]
    {a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
      Continuous[Pi.topologicalSpace, inst_11.toTopologicalSpace]
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
            (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
          a)}

Tactic:
UniformOnFun.isClosed_setOf_continuous h

Premises used: setOf, UniformOnFun.isClosed_setOf_continuous
-- 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]
    {a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
      Continuous[Pi.topologicalSpace, inst_11.toTopologicalSpace]
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
            (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
          a)}

Tactic:
exact UniformOnFun.isClosed_setOf_continuous h

Premises used: UniformOnFun.isClosed_setOf_continuous
-- 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:
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