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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
ι' : Type u_5
p : ι' → Prop
b : ι' → Set F
h : Filter.HasBasis (𝓝 0) p b
⊢ 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)}

Tactic:
(ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis h).comap _

Premises used: Set.Mem, setOf, Filter.HasBasis.comap, Set.preimage, Set.MapsTo, ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis
-- 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
⊢ 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)}

Tactic:
exact (ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis h).comap _

Premises used: Filter.HasBasis.comap, ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis
-- 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
⊢ Filter.HasBasis (α := E [⋀^ι]→L[𝕜] F) (𝓝 0)
    (fun (SV : Set (ι → E) × Set F) ↦ IsVonNBounded 𝕜 SV.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) SV.2)
    fun (SV : Set (ι → E) × Set F) ↦ {f : E [⋀^ι]→L[𝕜] F | MapsTo (⇑f : (a : ι → E) → F) SV.1 SV.2}

Tactic:
hasBasis_nhds_zero_of_basis (Filter.basis_sets _)

Premises used: setOf, Filter.basis_sets, ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis
-- 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 𝕜 E
inst_9 : T2Space F
⊢ IsClosedEmbedding (X := E [⋀^ι]→L[𝕜] F) toContinuousMultilinearMap

Tactic:
⟨isEmbedding_toContinuousMultilinearMap, isClosed_range_toContinuousMultilinearMap⟩

Premises used: ContinuousAlternatingMap.isClosed_range_toContinuousMultilinearMap, ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, Topology.IsClosedEmbedding.mk
-- 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 𝕜 E
⊢ ContinuousEvalConst (E [⋀^ι]→L[𝕜] F) (ι → E) F

Tactic:
.of_continuous_forget continuous_toContinuousMultilinearMap

Premises used: ContinuousEvalConst.of_continuous_forget, ContinuousAlternatingMap.continuous_toContinuousMultilinearMap
-- 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 𝕜 E
inst_9 : T2Space F
⊢ T2Space (E [⋀^ι]→L[𝕜] F)

Tactic:
.of_injective_continuous DFunLike.coe_injective continuous_coeFun

Premises used: T2Space.of_injective_continuous, DFunLike.coe_injective, continuous_coeFun
-- 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 𝕜 E
inst_9 : T2Space F
⊢ T3Space (E [⋀^ι]→L[𝕜] F)

Tactic:
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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ContinuousSMul 𝕜 E
𝕜' : Type u_5
inst_9 : NontriviallyNormedField 𝕜'
inst_10 : NormedAlgebra 𝕜' 𝕜
inst_11 : Module 𝕜' E
inst_12 : IsScalarTower 𝕜' 𝕜 E
inst_13 : Module 𝕜' F
inst_14 : IsScalarTower 𝕜' 𝕜 F
⊢ IsEmbedding (X := E [⋀^ι]→L[𝕜] F) (Y := E [⋀^ι]→L[𝕜'] F) (restrictScalars 𝕜')

Tactic:
letI : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  (isUniformEmbedding_restrictScalars _).isEmbedding

Premises used: ContinuousAlternatingMap.isUniformEmbedding_restrictScalars, 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
inst_8 : ContinuousSMul 𝕜 E
𝕜' : Type u_5
inst_9 : NontriviallyNormedField 𝕜'
inst_10 : NormedAlgebra 𝕜' 𝕜
inst_11 : Module 𝕜' E
inst_12 : IsScalarTower 𝕜' 𝕜 E
inst_13 : Module 𝕜' F
inst_14 : IsScalarTower 𝕜' 𝕜 F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (restrictScalars 𝕜')

Tactic:
isEmbedding_restrictScalars.continuous

Premises used: ContinuousAlternatingMap.isEmbedding_restrictScalars, 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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F
hf :
  ∀ (x : G) (v : (i : ι) → E) (i j : ι),
    v i = v j →
      i ≠ j →
        Eq.{u_3 + 1} (α := F)
          ((((f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x :
                  ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) :
                (a : (i : ι) → E) → F)
              v :
            F)
          (0 : F)
x x_1 : G
H :
  ∀ (x_2 : ι → E),
    Eq.{u_3 + 1} (α := F)
      (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x + x_1),
              map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } :
            (a : ι → E) → F)
          x_2 :
        F)
      (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x,
                map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } +
              { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
                map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } :
            (a : ι → E) → F)
          x_2 :
        F)
⊢ { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x + x_1),
      map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } =
    { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x,
        map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } +
      { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
        map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] 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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F
hf :
  ∀ (x : G) (v : (i : ι) → E) (i j : ι),
    v i = v j →
      i ≠ j →
        Eq.{u_3 + 1} (α := F)
          ((((f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x :
                  ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) :
                (a : (i : ι) → E) → F)
              v :
            F)
          (0 : F)
x x_1 : G
x_2 : ι → E
⊢ Eq.{u_3 + 1} (α := F)
    (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x + x_1),
            map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } :
          (a : ι → E) → F)
        x_2 :
      F)
    (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x,
              map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } +
            { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
              map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } :
          (a : ι → E) → F)
        x_2 :
      F)

Tactic:
simp
-- 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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F
hf :
  ∀ (x : G) (v : (i : ι) → E) (i j : ι),
    v i = v j →
      i ≠ j →
        Eq.{u_3 + 1} (α := F)
          ((((f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x :
                  ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) :
                (a : (i : ι) → E) → F)
              v :
            F)
          (0 : F)
x : 𝕜
x_1 : G
H :
  ∀ (x_2 : ι → E),
    Eq.{u_3 + 1} (α := F)
      (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x • x_1),
              map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } :
            (a : ι → E) → F)
          x_2 :
        F)
      ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
              { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
                map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } :
            (a : ι → E) → F)
          x_2 :
        F)
⊢ { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x • x_1),
      map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
        map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] 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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F
hf :
  ∀ (x : G) (v : (i : ι) → E) (i j : ι),
    v i = v j →
      i ≠ j →
        Eq.{u_3 + 1} (α := F)
          ((((f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x :
                  ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) :
                (a : (i : ι) → E) → F)
              v :
            F)
          (0 : F)
x : 𝕜
x_1 : G
x_2 : ι → E
⊢ Eq.{u_3 + 1} (α := F)
    (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x • x_1),
            map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } :
          (a : ι → E) → F)
        x_2 :
      F)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
            { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
              map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } :
          (a : ι → E) → F)
        x_2 :
      F)

Tactic:
simp
-- 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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F
hf :
  ∀ (x : G) (v : (i : ι) → E) (i j : ι),
    v i = v j →
      i ≠ j →
        Eq.{u_3 + 1} (α := F)
          ((((f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x :
                  ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) :
                (a : (i : ι) → E) → F)
              v :
            F)
          (0 : F)
x : G
v : ι → E
⊢ Eq.{u_3 + 1} (α := F) ((((liftCLM f hf : (a : G) → E [⋀^ι]→L[𝕜] F) x : E [⋀^ι]→L[𝕜] F) : (a : ι → E) → F) v : F)
    ((((f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x :
            ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) :
          (a : (i : ι) → E) → F)
        v :
      F)

Tactic:
rfl

Premises used: 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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst_12 : AddCommGroup E'
inst_13 : Module 𝕜 E'
inst_14 : TopologicalSpace E'
f : E →L[𝕜] E'
rw :
  Continuous[instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (toContinuousMultilinearMap ∘ AddHom.toFun (LinearMap.toAddHom (compContinuousLinearMapₗ f)))
⊢ Continuous[instTopologicalSpace, instTopologicalSpace]
    (AddHom.toFun (LinearMap.toAddHom (compContinuousLinearMapₗ f)))

Tactic:
rw [isEmbedding_toContinuousMultilinearMap.continuous_iff]

Premises used: ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, Topology.IsEmbedding.continuous_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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst_12 : AddCommGroup E'
inst_13 : Module 𝕜 E'
inst_14 : TopologicalSpace E'
f : E →L[𝕜] E'
⊢ Continuous[instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (toContinuousMultilinearMap ∘ AddHom.toFun (LinearMap.toAddHom (compContinuousLinearMapₗ f)))

Tactic:
(map_continuous <| ContinuousMultilinearMap.compContinuousLinearMapL fun _ ↦ f).comp
      continuous_toContinuousMultilinearMap

Premises used: Continuous.comp, ContinuousMapClass.map_continuous, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousMultilinearMap.compContinuousLinearMapL, ContinuousAlternatingMap.continuous_toContinuousMultilinearMap
-- 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
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst_12 : AddCommGroup E'
inst_13 : Module 𝕜 E'
inst_14 : TopologicalSpace E'
f : E →L[𝕜] E'
⊢ Continuous[instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (toContinuousMultilinearMap ∘ AddHom.toFun (LinearMap.toAddHom (compContinuousLinearMapₗ f)))

Tactic:
exact (map_continuous <| ContinuousMultilinearMap.compContinuousLinearMapL fun _ ↦ f).comp
      continuous_toContinuousMultilinearMap

Premises used: Continuous.comp, ContinuousMapClass.map_continuous, ContinuousMultilinearMap.compContinuousLinearMapL, ContinuousAlternatingMap.continuous_toContinuousMultilinearMap
-- 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 : ContinuousConstSMul 𝕜 F
inst_9 : ContinuousSMul 𝕜 E
m : ι → E
c : E [⋀^ι]→L[𝕜] F
⊢ Eq.{u_3 + 1} (α := F) ((apply 𝕜 E F m : (a : E [⋀^ι]→L[𝕜] F) → F) c : F) ((c : (a : ι → E) → F) m : F)

Tactic:
rfl

Premises used: 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 𝕜 E
α : Type u_5
p : α → E [⋀^ι]→L[𝕜] F
q : E [⋀^ι]→L[𝕜] F
h : HasSum p q
m : ι → E
⊢ HasSum.{u_3, u_5} (α := F) (fun (a : α) ↦ ((p a : (a : ι → E) → F) m : F)) ((q : (a : ι → E) → F) m : F)

Tactic:
h.map (applyAddHom m) (continuous_eval_const m)

Premises used: HasSum.map, ContinuousEvalConst.continuous_eval_const, ContinuousAlternatingMap.applyAddHom
-- 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 𝕜 E
α : Type u_5
p : α → E [⋀^ι]→L[𝕜] F
inst_9 : T2Space F
hp : Summable p
m : ι → E
⊢ Eq.{u_3 + 1} (α := F) ((∑' (a : α), p a : (a : ι → E) → F) m : F) (∑' (a : α), (p a : (a : ι → E) → F) m : F)

Tactic:
(hasSum_eval hp.hasSum m).tsum_eq.symm

Premises used: ContinuousAlternatingMap.hasSum_eval, HasSum.tsum_eq, Summable.hasSum, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
rw :
  Continuous[ContinuousAlternatingMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (ContinuousAlternatingMap.toContinuousMultilinearMap ∘
      AddHom.toFun
        (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
          ((compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g)))
⊢ Continuous[ContinuousAlternatingMap.instTopologicalSpace, ContinuousAlternatingMap.instTopologicalSpace]
    (AddHom.toFun
      (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
        ((compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g)))

Tactic:
rw [ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap.continuous_iff]

Premises used: ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
⊢ Continuous[ContinuousAlternatingMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (ContinuousAlternatingMap.toContinuousMultilinearMap ∘
      AddHom.toFun
        (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
          ((compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g)))

Tactic:
(map_continuous <| compContinuousMultilinearMapL 𝕜 (fun _ : ι ↦ E) F G g).comp
          ContinuousAlternatingMap.continuous_toContinuousMultilinearMap

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, Continuous.comp, ContinuousMapClass.map_continuous, DFunLike.coe, ContinuousAlternatingMap.continuous_toContinuousMultilinearMap, ContinuousLinearMap.compContinuousMultilinearMapL
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Topology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
⊢ Continuous[ContinuousAlternatingMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (ContinuousAlternatingMap.toContinuousMultilinearMap ∘
      AddHom.toFun
        (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
          ((compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g)))

Tactic:
exact (map_continuous <| compContinuousMultilinearMapL 𝕜 (fun _ : ι ↦ E) F G g).comp
          ContinuousAlternatingMap.continuous_toContinuousMultilinearMap

Premises used: Continuous.comp, ContinuousMapClass.map_continuous, DFunLike.coe, ContinuousAlternatingMap.continuous_toContinuousMultilinearMap, ContinuousLinearMap.compContinuousMultilinearMapL