awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : M →L[R] M'
c : R
g : M' [⋀^ι]→L[R] N
⊢ (c • g).compContinuousLinearMap f =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (g.compContinuousLinearMap f)
have H : ∀ (x : ι → M),
  Eq.{u_4 + 1} (α := N) (((c • g).compContinuousLinearMap f : (a : ι → M) → N) x : N)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (g.compContinuousLinearMap f) : (a : ι → M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M [⋀^ι]→L[R] N
⊢ f.compContinuousAlternatingMap (g₁ + g₂) = f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂
have H : ∀ (x : ι → M),
  Eq.{u_5 + 1} (α := N') ((f.compContinuousAlternatingMap (g₁ + g₂) : (a : ι → M) → N') x : N')
    ((f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂ : (a : ι → M) → N') x : N')
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
c : R
f : N →L[R] N'
g : M [⋀^ι]→L[R] N
⊢ f.compContinuousAlternatingMap (c • g) = c • f.compContinuousAlternatingMap g
have H : ∀ (x : ι → M),
  Eq.{u_5 + 1} (α := N') ((f.compContinuousAlternatingMap (c • g) : (a : ι → M) → N') x : N')
    ((c • f.compContinuousAlternatingMap g : (a : ι → M) → N') x : N')
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
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
⊢ 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 (α := ℤˣ) (β := ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N)
          (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0);
    { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ })
    0
have H : ∀ (x : ι → 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 (α := ℤˣ) (β := ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N)
                (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0);
          { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := sorry } :
          (a : ι → M) → N)
        x :
      N)
    ((0 : (a : ι → M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
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
⊢ (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 })
have 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' := sorry } :
          (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' := sorry : 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' := sorry : M [⋀^ι]→L[R] N }) :
          (a : ι → M) → N)
        x_2 :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
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
⊢ 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)))
have 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)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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] (range toContinuousMultilinearMap)
have 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)})
Tactic: simp only [range_toContinuousMultilinearMap, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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)})
have 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)})
Tactic: refine isClosed_iInter fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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)})
have 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)})
Tactic: refine isClosed_iInter fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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)})
have 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)})
Tactic: refine isClosed_iInter fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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)})
have 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)})
Tactic: refine isClosed_iInter fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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)})
have 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)}
Tactic: refine isClosed_iInter fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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)})
have 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)}
Tactic: repeat refine isClosed_iInter fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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) g.compContinuousAlternatingMap
have rw : IsUniformInducing (α := E [⋀^ι]→L[𝕜] F) (toContinuousMultilinearMap ∘ g.compContinuousAlternatingMap)
Tactic: rw [← isUniformEmbedding_toContinuousMultilinearMap.1.of_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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}
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)
have 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)
Tactic: wlog hF : T2Space F generalizing F
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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)
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)
have 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)
Tactic: wlog hF : T2Space F generalizing F
Cleared hypotheses: inst_9, inst_10
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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 (E [⋀^ι]→L[𝕜] F)
have inr : CompleteSpace (ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι)
Tactic: rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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) ι)
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)
have inr₁ : Surjective (α := E [⋀^ι]→L[𝕜] F) (β := ContinuousAlternatingMap.{u_1, u_2, u_3, u_4} 𝕜 E (SeparationQuotient F) ι)
  (ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.mkCLM 𝕜 F))
Tactic: rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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) ι
⊢ ∃ (a : E [⋀^ι]→L[𝕜] F), ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.mkCLM 𝕜 F) a = f
have h₁ : ContinuousLinearMap.compContinuousAlternatingMap (N := F) (SeparationQuotient.mkCLM 𝕜 F)
    (ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.outCLM 𝕜 F) f) =
  f
Tactic: use (SeparationQuotient.outCLM _ _).compContinuousAlternatingMap f
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
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) ι
⊢ ContinuousLinearMap.compContinuousAlternatingMap (N := F) (SeparationQuotient.mkCLM 𝕜 F)
      (ContinuousLinearMap.compContinuousAlternatingMap (SeparationQuotient.outCLM 𝕜 F) f) =
    f
have 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)
Tactic: ext