awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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 (E [⋀^ι]→L[𝕜] F)

Tactic:
isUniformEmbedding_toContinuousMultilinearMap.uniformContinuousConstSMul fun _ _ ↦ rfl

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.uniformContinuousConstSMul, rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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_3, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
rw : IsUniformInducing (α := E [⋀^ι]→L[𝕜] F) (toContinuousMultilinearMap ∘ g.compContinuousAlternatingMap)
⊢ IsUniformInducing (α := E [⋀^ι]→L[𝕜] F) g.compContinuousAlternatingMap

Tactic:
rw [← isUniformEmbedding_toContinuousMultilinearMap.1.of_comp_iff]

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformInducing.of_comp_iff, IsUniformEmbedding.toIsUniformInducing
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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_3, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
⊢ IsUniformInducing (α := E [⋀^ι]→L[𝕜] F) (toContinuousMultilinearMap ∘ g.compContinuousAlternatingMap)

Tactic:
(ContinuousMultilinearMap.isUniformInducing_postcomp g hg).comp
    isUniformEmbedding_toContinuousMultilinearMap.1

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, ContinuousLinearMap.compContinuousMultilinearMap, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.comp, ContinuousMultilinearMap.isUniformInducing_postcomp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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_3, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
⊢ IsUniformInducing (α := E [⋀^ι]→L[𝕜] F) (toContinuousMultilinearMap ∘ g.compContinuousAlternatingMap)

Tactic:
exact (ContinuousMultilinearMap.isUniformInducing_postcomp g hg).comp
    isUniformEmbedding_toContinuousMultilinearMap.1

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.comp, ContinuousMultilinearMap.isUniformInducing_postcomp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
inr :
  ∀
    (this :
      ∀ {F : Type u_3} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
        [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
        CompleteSpace (E [⋀^ι]→L[𝕜] F))
    (hF : ¬T2Space F), CompleteSpace (E [⋀^ι]→L[𝕜] F)
wlog :
  ∀ {F : Type u_3} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (E [⋀^ι]→L[𝕜] F)
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)

Tactic:
wlog hF : T2Space F generalizing F

Premises used: T2Space
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
inr : CompleteSpace (ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι)
inr₁ :
  Surjective (α := E [⋀^ι]→L[𝕜] F) (β := ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι)
    (ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.mkCLM 𝕜 F))
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)

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

Premises used: ContinuousAlternatingMap.isUniformInducing_postcomp, IsUniformInducing.completeSpace_congr
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ CompleteSpace (ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι)

Tactic:
this inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ CompleteSpace (ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι)

Tactic:
exact this inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
f : ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι
h₁ :
  ContinuousLinearMap.compContinuousAlternatingMap (N := F) (SeparationQuotient.mkCLM 𝕜 F)
      (ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.outCLM 𝕜 F) f) =
    f
⊢ ∃ (a : E [⋀^ι]→L[𝕜] F), ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.mkCLM 𝕜 F) a = f

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

Premises used: ContinuousLinearMap.compContinuousAlternatingMap, SeparationQuotient.outCLM
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
f : ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι
h₁ :
  ∀ (x : ι → E),
    Eq.{u_3 + 1} (α := SeparationQuotient F)
      (((ContinuousLinearMap.compContinuousAlternatingMap (N := F) (SeparationQuotient.mkCLM 𝕜 F)
                (ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.outCLM 𝕜 F) f) :
              ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι) :
            (a : ι → E) → SeparationQuotient F)
          x :
        SeparationQuotient F)
      ((f : (a : ι → E) → SeparationQuotient F) x : SeparationQuotient F)
⊢ ContinuousLinearMap.compContinuousAlternatingMap (N := F) (SeparationQuotient.mkCLM 𝕜 F)
      (ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.outCLM 𝕜 F) f) =
    f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
f : ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι
x : ι → E
⊢ Eq.{u_3 + 1} (α := SeparationQuotient F)
    (((ContinuousLinearMap.compContinuousAlternatingMap (N := F) (SeparationQuotient.mkCLM 𝕜 F)
              (ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.outCLM 𝕜 F) f) :
            ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι) :
          (a : ι → E) → SeparationQuotient F)
        x :
      SeparationQuotient F)
    ((f : (a : ι → E) → SeparationQuotient F) x : SeparationQuotient F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ContinuousSMul 𝕜 E
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
F : Type u_3
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
⊢ CompleteSpace (ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (i : ι) ↦ E) F)

Tactic:
have := ContinuousMultilinearMap.completeSpace (F := F) h
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ContinuousSMul 𝕜 E
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
F : Type u_3
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
this : CompleteSpace (ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (i : ι) ↦ E) F)
rw :
  IsComplete (α := ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F)
    (range toContinuousMultilinearMap)
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)

Tactic:
rw [completeSpace_iff_isComplete_range
    isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing]

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformEmbedding.isUniformInducing, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ContinuousSMul 𝕜 E
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
F : Type u_3
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
this : CompleteSpace (ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (i : ι) ↦ E) F)
⊢ IsComplete (α := ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F)
    (range toContinuousMultilinearMap)

Tactic:
apply isClosed_range_toContinuousMultilinearMap.isComplete

Premises used: IsClosed.isComplete
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
inst_11 : IsTopologicalAddGroup E
inst_12 : SequentialSpace (ι → E)
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)

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

Premises used: ContinuousAlternatingMap.completeSpace, Filter.Tendsto.isVonNBounded_range, Bornology.IsVonNBounded.insert, Topology.IsCoherentWith.of_seq
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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 : Module 𝕜' E
inst_11 : IsScalarTower 𝕜' 𝕜 E
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ContinuousSMul 𝕜 E
rw :
  IsUniformEmbedding (α := E [⋀^ι]→L[𝕜] F) (β := ContinuousMultilinearMap.{u_5, u_4, u_2, u_3} 𝕜' (fun (x : ι) ↦ E) F)
    (toContinuousMultilinearMap ∘ restrictScalars 𝕜')
⊢ IsUniformEmbedding (α := E [⋀^ι]→L[𝕜] F) (β := E [⋀^ι]→L[𝕜'] F) (restrictScalars 𝕜')

Tactic:
rw [← isUniformEmbedding_toContinuousMultilinearMap.of_comp_iff]

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformEmbedding.of_comp_iff
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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 : Module 𝕜' E
inst_11 : IsScalarTower 𝕜' 𝕜 E
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ContinuousSMul 𝕜 E
⊢ IsUniformEmbedding (α := E [⋀^ι]→L[𝕜] F) (β := ContinuousMultilinearMap.{u_5, u_4, u_2, u_3} 𝕜' (fun (x : ι) ↦ E) F)
    (toContinuousMultilinearMap ∘ restrictScalars 𝕜')

Tactic:
(ContinuousMultilinearMap.isUniformEmbedding_restrictScalars 𝕜').comp
    isUniformEmbedding_toContinuousMultilinearMap

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformEmbedding.comp, ContinuousMultilinearMap.restrictScalars, ContinuousMultilinearMap.isUniformEmbedding_restrictScalars
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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 : Module 𝕜' E
inst_11 : IsScalarTower 𝕜' 𝕜 E
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ContinuousSMul 𝕜 E
⊢ IsUniformEmbedding (α := E [⋀^ι]→L[𝕜] F) (β := ContinuousMultilinearMap.{u_5, u_4, u_2, u_3} 𝕜' (fun (x : ι) ↦ E) F)
    (toContinuousMultilinearMap ∘ restrictScalars 𝕜')

Tactic:
exact (ContinuousMultilinearMap.isUniformEmbedding_restrictScalars 𝕜').comp
    isUniformEmbedding_toContinuousMultilinearMap

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformEmbedding.comp, ContinuousMultilinearMap.isUniformEmbedding_restrictScalars
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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 : Module 𝕜' E
inst_11 : IsScalarTower 𝕜' 𝕜 E
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ContinuousSMul 𝕜 E
⊢ UniformContinuous (α := E [⋀^ι]→L[𝕜] F) (β := E [⋀^ι]→L[𝕜'] F) (restrictScalars 𝕜')

Tactic:
(isUniformEmbedding_restrictScalars 𝕜').uniformContinuous

Premises used: ContinuousAlternatingMap.isUniformEmbedding_restrictScalars, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
⊢ IsEmbedding (X := E [⋀^ι]→L[𝕜] F) toContinuousMultilinearMap

Tactic:
letI := IsTopologicalAddGroup.rightUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  isUniformEmbedding_toContinuousMultilinearMap.isEmbedding

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
⊢ IsTopologicalAddGroup (E [⋀^ι]→L[𝕜] F)

Tactic:
isEmbedding_toContinuousMultilinearMap.topologicalAddGroup
    (toContinuousMultilinearMapLinear (R := ℕ))

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMapLinear, ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, Topology.IsInducing.topologicalAddGroup, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
⊢ Continuous[instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace] toContinuousMultilinearMap

Tactic:
isEmbedding_toContinuousMultilinearMap.continuous

Premises used: ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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
⊢ ContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)

Tactic:
isEmbedding_toContinuousMultilinearMap.continuousConstSMul id rfl

Premises used: Topology.IsInducing.continuousConstSMul, ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, id, Topology.IsEmbedding.toIsInducing, rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ContinuousSMul 𝕜 F
⊢ ContinuousSMul 𝕜 (E [⋀^ι]→L[𝕜] F)

Tactic:
isEmbedding_toContinuousMultilinearMap.continuousSMul continuous_id rfl

Premises used: Topology.IsInducing.continuousSMul, ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, continuous_id, Topology.IsEmbedding.toIsInducing, rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
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
rw :
  Filter.HasBasis (α := E [⋀^ι]→L[𝕜] F) (Filter.comap toContinuousMultilinearMap (𝓝 (toContinuousMultilinearMap 0)))
    (fun (Si : Set (ι → E) × ι') ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set (ι → E) × ι') ↦
    {f : E [⋀^ι]→L[𝕜] F | MapsTo (⇑f : (a : ι → E) → F) Si.1 (b Si.2)}
⊢ Filter.HasBasis (α := E [⋀^ι]→L[𝕜] F) (𝓝 0) (fun (Si : Set (ι → E) × ι') ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2)
    fun (Si : Set (ι → E) × ι') ↦ {f : E [⋀^ι]→L[𝕜] F | MapsTo (⇑f : (a : ι → E) → F) Si.1 (b Si.2)}

Tactic:
rw [nhds_induced]

Premises used: nhds_induced