awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
inst_7 : IsTopologicalAddGroup N
inst_8 : Fintype ι
inst_9 : DecidableEq ι
f x x_1 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N
H :
  ∀ (x_2 : ι → M),
    Eq.{u_3 + 1} (α := N)
      ((let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
              ∑ σ : Equiv.Perm ι,
                HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
                  (domDomCongr σ (x + x_1));
            { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ } :
            (a : ι → M) → N)
          x_2 :
        N)
      ((HAdd.hAdd (α := M [⋀^ι]→L[R] N)
              (let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
                ∑ σ : Equiv.Perm ι,
                  HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
                    (domDomCongr σ x);
              { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→L[R] N })
              (let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
                ∑ σ : Equiv.Perm ι,
                  HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
                    (domDomCongr σ x_1);
              { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→L[R] N }) :
            (a : ι → M) → N)
          x_2 :
        N)
⊢ (let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
      ∑ σ : Equiv.Perm ι,
        HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
          (domDomCongr σ (x + x_1));
    { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }) =
    HAdd.hAdd (α := M [⋀^ι]→L[R] N)
      (let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
        ∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (domDomCongr σ x);
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→L[R] N })
      (let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
        ∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (domDomCongr σ x_1);
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→L[R] N })

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
inst_7 : IsTopologicalAddGroup N
inst_8 : Fintype ι
inst_9 : DecidableEq ι
f x x_1 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N
x_2 : ι → M
⊢ Eq.{u_3 + 1} (α := N)
    ((let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
            ∑ σ : Equiv.Perm ι,
              HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
                (domDomCongr σ (x + x_1));
          { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ } :
          (a : ι → M) → N)
        x_2 :
      N)
    ((HAdd.hAdd (α := M [⋀^ι]→L[R] N)
            (let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
              ∑ σ : Equiv.Perm ι,
                HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
                  (domDomCongr σ x);
            { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→L[R] N })
            (let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
              ∑ σ : Equiv.Perm ι,
                HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
                  (domDomCongr σ x_1);
            { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→L[R] N }) :
          (a : ι → M) → N)
        x_2 :
      N)

Tactic:
simp [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
inst_7 : IsTopologicalAddGroup N
inst_8 : Fintype ι
inst_9 : DecidableEq ι
f : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N
v : ι → M
⊢ Eq.{u_3 + 1} (α := N)
    (((((alternatization : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N →+ M [⋀^ι]→L[R] N) :
                (a : ContinuousMultilinearMap R (fun (x : ι) ↦ M) N) → M [⋀^ι]→L[R] N)
              f :
            M [⋀^ι]→L[R] N) :
          (a : ι → M) → N)
        v :
      N)
    (∑ σ : Equiv.Perm ι,
        HSMul.hSMul (α := ℤˣ) (β := N) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
          ((f : (a : (i : ι) → M) → N) (v ∘ (⇑σ : (a : ι) → ι)) : N) :
      N)

Tactic:
simp [alternatization, Function.comp_def]

Premises used: ContinuousMultilinearMap.alternatization, Function.comp_def
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
inst_7 : IsTopologicalAddGroup N
inst_8 : Fintype ι
inst_9 : DecidableEq ι
f : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N
H :
  ∀ (v : ι → M),
    Eq.{u_3 + 1} (α := N)
      ((ContinuousAlternatingMap.toAlternatingMap
              (((alternatization :
                    ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N →+ M [⋀^ι]→L[R] N) :
                  (a : ContinuousMultilinearMap R (fun (x : ι) ↦ M) N) → M [⋀^ι]→L[R] N)
                f) :
            (a : ι → M) → N)
          v :
        N)
      ((((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N) → M [⋀^ι]→ₗ[R] N)
                (f.toMultilinearMap (M₁ := fun (x : ι) ↦ M)) :
              M [⋀^ι]→ₗ[R] N) :
            (a : ι → M) → N)
          v :
        N)
⊢ Eq (α := M [⋀^ι]→ₗ[R] N)
    (ContinuousAlternatingMap.toAlternatingMap
      (((alternatization : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N →+ M [⋀^ι]→L[R] N) :
          (a : ContinuousMultilinearMap R (fun (x : ι) ↦ M) N) → M [⋀^ι]→L[R] N)
        f))
    ((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N) → M [⋀^ι]→ₗ[R] N)
      (f.toMultilinearMap (M₁ := fun (x : ι) ↦ M)))

Tactic:
ext v
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
inst_7 : IsTopologicalAddGroup N
inst_8 : Fintype ι
inst_9 : DecidableEq ι
f : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N
v : ι → M
⊢ Eq.{u_3 + 1} (α := N)
    ((ContinuousAlternatingMap.toAlternatingMap
            (((alternatization :
                  ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N →+ M [⋀^ι]→L[R] N) :
                (a : ContinuousMultilinearMap R (fun (x : ι) ↦ M) N) → M [⋀^ι]→L[R] N)
              f) :
          (a : ι → M) → N)
        v :
      N)
    ((((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N) → M [⋀^ι]→ₗ[R] N)
              (f.toMultilinearMap (M₁ := fun (x : ι) ↦ M)) :
            M [⋀^ι]→ₗ[R] N) :
          (a : ι → M) → N)
        v :
      N)

Tactic:
simp [alternatization_apply_apply, MultilinearMap.alternatization_apply, Function.comp_def]

Premises used: ContinuousMultilinearMap.alternatization_apply_apply, MultilinearMap.alternatization_apply, Function.comp_def
-- 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
simp :
  IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (i : ι → E),
      ⋂ (i_1 : ι),
        ⋂ (i_2 : ι),
          ⋂ (_ : i i_1 = i i_2),
            ⋂ (_ : i_1 ≠ i_2),
              {x : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
                Eq.{u_3 + 1} (α := F) ((x : (a : (i : ι) → E) → F) i : F) (0 : F)})
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace] (range toContinuousMultilinearMap)

Tactic:
simp only [range_toContinuousMultilinearMap, setOf_forall]

Premises used: ContinuousAlternatingMap.range_toContinuousMultilinearMap, Set.setOf_forall
-- 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
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (i : ι → E),
      ⋂ (i_1 : ι),
        ⋂ (i_2 : ι),
          ⋂ (_ : i i_1 = i i_2),
            ⋂ (_ : i_1 ≠ i_2),
              {x : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
                Eq.{u_3 + 1} (α := F) ((x : (a : (i : ι) → E) → F) i : F) (0 : F)})

Tactic:
isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
refine :
  ∀ (x : ι → E),
    IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
      (⋂ (i : ι),
        ⋂ (i_1 : ι),
          ⋂ (_ : x i = x i_1),
            ⋂ (_ : i ≠ i_1),
              {x_2 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
                Eq.{u_3 + 1} (α := F) ((x_2 : (a : (i : ι) → E) → F) x : F) (0 : F)})
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (i : ι → E),
      ⋂ (i_1 : ι),
        ⋂ (i_2 : ι),
          ⋂ (_ : i i_1 = i i_2),
            ⋂ (_ : i_1 ≠ i_2),
              {x : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
                Eq.{u_3 + 1} (α := F) ((x : (a : (i : ι) → E) → F) i : F) (0 : F)})

Tactic:
refine isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (i : ι),
      ⋂ (i_1 : ι),
        ⋂ (_ : x i = x i_1),
          ⋂ (_ : i ≠ i_1),
            {x_2 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
              Eq.{u_3 + 1} (α := F) ((x_2 : (a : (i : ι) → E) → F) x : F) (0 : F)})

Tactic:
isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
refine :
  ∀ (x_1 : ι),
    IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
      (⋂ (i : ι),
        ⋂ (_ : x x_1 = x i),
          ⋂ (_ : x_1 ≠ i),
            {x_3 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
              Eq.{u_3 + 1} (α := F) ((x_3 : (a : (i : ι) → E) → F) x : F) (0 : F)})
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (i : ι),
      ⋂ (i_1 : ι),
        ⋂ (_ : x i = x i_1),
          ⋂ (_ : i ≠ i_1),
            {x_2 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
              Eq.{u_3 + 1} (α := F) ((x_2 : (a : (i : ι) → E) → F) x : F) (0 : F)})

Tactic:
refine isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
x_1 : ι
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (i : ι),
      ⋂ (_ : x x_1 = x i),
        ⋂ (_ : x_1 ≠ i),
          {x_3 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
            Eq.{u_3 + 1} (α := F) ((x_3 : (a : (i : ι) → E) → F) x : F) (0 : F)})

Tactic:
isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
x_1 : ι
refine :
  ∀ (x_2 : ι),
    IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
      (⋂ (_ : x x_1 = x x_2),
        ⋂ (_ : x_1 ≠ x_2),
          {x_4 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
            Eq.{u_3 + 1} (α := F) ((x_4 : (a : (i : ι) → E) → F) x : F) (0 : F)})
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (i : ι),
      ⋂ (_ : x x_1 = x i),
        ⋂ (_ : x_1 ≠ i),
          {x_3 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
            Eq.{u_3 + 1} (α := F) ((x_3 : (a : (i : ι) → E) → F) x : F) (0 : F)})

Tactic:
refine isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
x_1 x_2 : ι
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (_ : x x_1 = x x_2),
      ⋂ (_ : x_1 ≠ x_2),
        {x_4 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
          Eq.{u_3 + 1} (α := F) ((x_4 : (a : (i : ι) → E) → F) x : F) (0 : F)})

Tactic:
isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
x_1 x_2 : ι
refine :
  x x_1 = x x_2 →
    IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
      (⋂ (_ : x_1 ≠ x_2),
        {x_4 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
          Eq.{u_3 + 1} (α := F) ((x_4 : (a : (i : ι) → E) → F) x : F) (0 : F)})
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (_ : x x_1 = x x_2),
      ⋂ (_ : x_1 ≠ x_2),
        {x_4 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
          Eq.{u_3 + 1} (α := F) ((x_4 : (a : (i : ι) → E) → F) x : F) (0 : F)})

Tactic:
refine isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
x_1 x_2 : ι
h : x x_1 = x x_2
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (_ : x_1 ≠ x_2),
      {x_3 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
        Eq.{u_3 + 1} (α := F) ((x_3 : (a : (i : ι) → E) → F) x : F) (0 : F)})

Tactic:
isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
x_1 x_2 : ι
h : x x_1 = x x_2
refine :
  x_1 ≠ x_2 →
    IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
      {x_4 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
        Eq.{u_3 + 1} (α := F) ((x_4 : (a : (i : ι) → E) → F) x : F) (0 : F)}
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (_ : x_1 ≠ x_2),
      {x_3 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
        Eq.{u_3 + 1} (α := F) ((x_3 : (a : (i : ι) → E) → F) x : F) (0 : F)})

Tactic:
refine isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
repeat :
  ∀ (x : ι → E) (x_1 x_2 : ι),
    x x_1 = x x_2 →
      x_1 ≠ x_2 →
        IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
          {x_5 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
            Eq.{u_3 + 1} (α := F) ((x_5 : (a : (i : ι) → E) → F) x : F) (0 : F)}
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    (⋂ (i : ι → E),
      ⋂ (i_1 : ι),
        ⋂ (i_2 : ι),
          ⋂ (_ : i i_1 = i i_2),
            ⋂ (_ : i_1 ≠ i_2),
              {x : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
                Eq.{u_3 + 1} (α := F) ((x : (a : (i : ι) → E) → F) i : F) (0 : F)})

Tactic:
repeat refine isClosed_iInter fun _ ↦ ?_

Premises used: isClosed_iInter
-- 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
x : ι → E
x_1 x_2 : ι
h : x x_1 = x x_2
h_1 : x_1 ≠ x_2
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    {x_3 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
      Eq.{u_3 + 1} (α := F) ((x_3 : (a : (i : ι) → E) → F) x : F) (0 : F)}

Tactic:
isClosed_singleton.preimage (continuous_eval_const _)

Premises used: Set.Mem, setOf, Set.preimage, ContinuousEvalConst.continuous_eval_const, Set.singleton, IsClosed.preimage, isClosed_singleton
-- 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
x : ι → E
x_1 x_2 : ι
h : x x_1 = x x_2
h_1 : x_1 ≠ x_2
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace]
    {x_3 : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F |
      Eq.{u_3 + 1} (α := F) ((x_3 : (a : (i : ι) → E) → F) x : F) (0 : F)}

Tactic:
exact isClosed_singleton.preimage (continuous_eval_const _)

Premises used: ContinuousEvalConst.continuous_eval_const, IsClosed.preimage, isClosed_singleton
-- 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
⊢ UniformContinuous (α := E [⋀^ι]→L[𝕜] F) toContinuousMultilinearMap

Tactic:
isUniformEmbedding_toContinuousMultilinearMap.uniformContinuous

Premises used: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ContinuousSMul 𝕜 E
⊢ UniformContinuous (α := E [⋀^ι]→L[𝕜] F) (β := (a : ι → E) → F) (DFunLike.coe (β := fun (a : ι → E) ↦ F))

Tactic:
ContinuousMultilinearMap.uniformContinuous_coe_fun.comp
    uniformContinuous_toContinuousMultilinearMap

Premises used: UniformContinuous.comp, ContinuousAlternatingMap.uniformContinuous_toContinuousMultilinearMap, ContinuousMultilinearMap.uniformContinuous_coe_fun
-- 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
x : ι → E
⊢ UniformContinuous (β := F) fun (f : E [⋀^ι]→L[𝕜] F) ↦ (f : (a : ι → E) → F) x

Tactic:
uniformContinuous_pi.1 uniformContinuous_coe_fun x

Premises used: ContinuousAlternatingMap.uniformContinuous_coe_fun, uniformContinuous_pi, Iff.mp
-- 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
⊢ IsUniformAddGroup (E [⋀^ι]→L[𝕜] F)

Tactic:
isUniformEmbedding_toContinuousMultilinearMap.isUniformAddGroup
    (toContinuousMultilinearMapLinear (R := ℕ))

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMapLinear, ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, IsUniformInducing.isUniformAddGroup, IsUniformEmbedding.toIsUniformInducing