awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
r : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
              CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
          N) :
      N')
have h : HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
  (g : (a : N) → N')
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
      N)
Tactic: rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul,
      LinearMap.compAlternatingMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
r : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
h :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    (g : (a : N) → N')
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
            CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
        N)
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
              CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
          N) :
      N')
have h₁ : HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
  (g : (a : N) → N') (HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N))
Tactic: rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul,
      LinearMap.compAlternatingMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
r : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
h :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    (g : (a : N) → N')
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
            CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
        N)
h₁ :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    (g : (a : N) → N') (HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N))
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
              CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
          N) :
      N')
have h₂ : HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
  HSMul.hSMul (β := N') r ((g : (a : N) → N') ((f 0 : (a : Fin 0 → M) → N) 0 : N) : N')
Tactic: rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul,
      LinearMap.compAlternatingMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
r : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
h :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    (g : (a : N) → N')
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
            CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
        N)
h₁ :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    (g : (a : N) → N') (HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N))
h₂ :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    HSMul.hSMul (β := N') r ((g : (a : N) → N') ((f 0 : (a : Fin 0 → M) → N) 0 : N) : N')
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
              CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
          N) :
      N')
have h₃ : HSMul.hSMul (β := N') r ((g : (a : N) → N') ((f 0 : (a : Fin 0 → M) → N) 0 : N) : N') =
  HSMul.hSMul (β := N') r ((g : (a : N) → N') ((f 0 : (a : Fin 0 → M) → N) 0 : N) : N')
Tactic: rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul,
      LinearMap.compAlternatingMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
x y : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    Eq.{u_4 + 1} (α := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          x :
        N')
      ((g : (a : N) → N')
          ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                  ExteriorAlgebra R M →ₗ[R] N) :
                (a : ExteriorAlgebra R M) → N)
              x :
            N) :
        N')
hy :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    Eq.{u_4 + 1} (α := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          y :
        N')
      ((g : (a : N) → N')
          ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                  ExteriorAlgebra R M →ₗ[R] N) :
                (a : ExteriorAlgebra R M) → N)
              y :
            N) :
        N')
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        (x + y) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            (x + y) :
          N) :
      N')
have h : HAdd.hAdd (α := N') (β := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        x :
      N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        y :
      N') =
  (g : (a : N) → N')
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        (x + y) :
      N)
Tactic: rw [map_add, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
x : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0
m : M
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    Eq.{u_4 + 1} (α := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          x :
        N')
      ((g : (a : N) → N')
          ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                  ExteriorAlgebra R M →ₗ[R] N) :
                (a : ExteriorAlgebra R M) → N)
              x :
            N) :
        N')
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        (HMul.hMul (α := CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
          ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) x) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            (HMul.hMul (α := CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
              ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
              x) :
          N) :
      N')
have h : Eq.{u_4 + 1} (α := N')
  (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
          (AlternatingMap.curryLeft (g.compAlternatingMap (f i.succ)) : (a : M) → M [⋀^Fin i]→ₗ[R] N') m :
        (a : ExteriorAlgebra R M) → N')
      x :
    N')
  (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
          g.compAlternatingMap ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m) :
        (a : ExteriorAlgebra R M) → N')
      x :
    N')
Tactic: rw [liftAlternating_ι_mul, liftAlternating_ι_mul, ← hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : ExteriorAlgebra R M
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        v :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            v :
          N) :
      N')
have h : ∀ (r : R) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
              CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
          N) :
      N')
Tactic: induction v using CliffordAlgebra.left_induction generalizing f with
  | algebraMap =>
    rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul,
      LinearMap.compAlternatingMap_apply]
  | add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx =>
    rw [liftAlternating_ι_mul, liftAlternating_ι_mul, ← hx]
    simp_rw [AlternatingMap.curryLeft_compAlternatingMap]
Cleared hypotheses: f, v
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
F : ExteriorAlgebra R M →ₗ[R] N
⊢ F ∘ₗ
      (liftAlternating :
          (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] ExteriorAlgebra R M) → ExteriorAlgebra R M →ₗ[R] ExteriorAlgebra R M)
        (ιMulti R) =
    F
have rw : F ∘ₗ LinearMap.id = F
Tactic: rw [liftAlternating_ιMulti, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
F : ExteriorAlgebra R M →ₗ[R] N
rw : F ∘ₗ LinearMap.id = F
⊢ F ∘ₗ
      (liftAlternating :
          (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] ExteriorAlgebra R M) → ExteriorAlgebra R M →ₗ[R] ExteriorAlgebra R M)
        (ιMulti R) =
    F
have rw₁ : F = F
Tactic: rw [liftAlternating_ιMulti, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))
    (⋀[R]^n M)
have a : LE.le (α := Submodule R (ExteriorAlgebra R M))
  (span R
    (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
      {a : Fin n → M | range a ⊆ s}))
  (⋀[R]^n M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
a :
  LE.le (α := Submodule R (ExteriorAlgebra R M))
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))
    (⋀[R]^n M)
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))
    (⋀[R]^n M)
have a₁ : LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
  (span R
    (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
      {a : Fin n → M | range a ⊆ s}))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
⊢ LE.le (α := Submodule R (ExteriorAlgebra R M))
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))
    (⋀[R]^n M)
have a : image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
    {a : Fin n → M | range a ⊆ s} ⊆
  (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
Tactic: rw [span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
y : Fin n → M
y_mem : Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | range a ⊆ s} y
⊢ Membership.mem (α := ExteriorAlgebra R M) (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)
have a : Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
  (range (ι := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M))
  ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)
Tactic: apply ExteriorAlgebra.ιMulti_range R n
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
⊢ LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))
have a : HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n ⊆
  (↑(span R
        (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
          {a : Fin n → M | range a ⊆ s})) :
    Set (ExteriorAlgebra R M))
Tactic: rw [ExteriorAlgebra.exteriorPower, LinearMap.range_eq_map, ← hs, map_span, span_pow, span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
x : ExteriorAlgebra R M
hx : x ∈ HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ x ∈
    (↑(span R
          (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
            {a : Fin n → M | range a ⊆ s})) :
      Set (ExteriorAlgebra R M))
have a : ∀ (f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1)))
  (hx :
    List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
      HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n),
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(span R
          (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
            {a : Fin n → M | range a ⊆ s})) :
      Set (ExteriorAlgebra R M))
Tactic: obtain ⟨f, rfl⟩ := Set.mem_pow.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(span R
          (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
            {a : Fin n → M | range a ⊆ s})) :
      Set (ExteriorAlgebra R M))
have a : Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | range a ⊆ s}
  ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
    Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
        Membership.mem (γ := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s)
          x) ∘
      f)
Tactic: refine mem_span_of_mem ⟨ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f, ?_, ?_⟩