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'
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N
have M₁ : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
Tactic: suffices
    (∀ i, M [⋀^Fin i]→ₗ[R] N) →ₗ[R]
      ExteriorAlgebra R M →ₗ[R] ∀ i, M [⋀^Fin i]→ₗ[R] N by
    refine LinearMap.compr₂ this ?_
    refine (LinearEquiv.toLinearMap ?_).comp (LinearMap.proj 0)
    exact AlternatingMap.constLinearEquivOfIsEmpty.symm
-- 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'
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
have refine_1 : M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
Tactic: refine CliffordAlgebra.foldl _ ?_ ?_
-- 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'
refine_1 : M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
have refine_2 : ∀ (m : M) (x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  (((LinearMap.mk₂ R
                (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                  (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                sorry sorry sorry sorry :
              (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
            m :
          ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
        (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((((LinearMap.mk₂ R
                    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                      (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                    sorry sorry sorry sorry :
                  (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                m :
              ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
            (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
          x :
        (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) =
    HSMul.hSMul (α := R) ((0 : (a : M) → R) m : R) x
Tactic: refine CliffordAlgebra.foldl _ ?_ ?_
-- 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'
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
have refine_1 : ∀ (m₁ m₂ : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (m₁ + m₂) f =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₁ f)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₂ f)
Tactic: refine
      LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_)
        (fun m f₁ f₂ => ?_) fun c m f => ?_
-- 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'
refine_1 :
  ∀ (m₁ m₂ : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (m₁ + m₂) f =
      HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₁ f)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₂ f)
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
have refine_1₁ : ∀ (c : R) (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (c • m) f =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)
Tactic: refine
      LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_)
        (fun m f₁ f₂ => ?_) fun c m f => ?_
-- 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'
refine_1 :
  ∀ (m₁ m₂ : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (m₁ + m₂) f =
      HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₁ f)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₂ f)
refine_1₁ :
  ∀ (c : R) (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (c • m) f =
      HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f)
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
have refine_1₂ : ∀ (m : M) (f₁ f₂ : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (f₁ + f₂) =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₁)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₂)
Tactic: refine
      LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_)
        (fun m f₁ f₂ => ?_) fun c m f => ?_
-- 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'
refine_1 :
  ∀ (m₁ m₂ : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (m₁ + m₂) f =
      HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₁ f)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₂ f)
refine_1₁ :
  ∀ (c : R) (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (c • m) f =
      HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f)
refine_1₂ :
  ∀ (m : M) (f₁ f₂ : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m (f₁ + f₂) =
      HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f₁)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f₂)
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
have refine_1₃ : ∀ (c : R) (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (c • f) =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)
Tactic: refine
      LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_)
        (fun m f₁ f₂ => ?_) fun c m f => ?_
-- 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'
m₁ m₂ : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (m₁ + m₂) f =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₁ f)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₂ f)
have refine_1 : ∀ (i : ℕ),
  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (m₁ + m₂) f i =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₁ f)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₂ f)
      i
Tactic: ext i : 1
-- 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'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (c • m) f =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)
have refine_1 : ∀ (i : ℕ),
  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (c • m) f i =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)
      i
Tactic: ext i : 1
-- 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'
m : M
f₁ f₂ : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (f₁ + f₂) =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₁)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₂)
have refine_1 : ∀ (i : ℕ),
  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (f₁ + f₂) i =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₁)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f₂)
      i
Tactic: ext i : 1
-- 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'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (c • f) =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)
have refine_1 : ∀ (i : ℕ),
  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      m (c • f) i =
    HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m f)
      i
Tactic: ext i : 1
-- 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'
m : M
x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (((LinearMap.mk₂ R
                (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                  (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                ⋯ ⋯ ⋯ ⋯ :
              (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
            m :
          ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
        (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((((LinearMap.mk₂ R
                    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                      (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                    ⋯ ⋯ ⋯ ⋯ :
                  (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                m :
              ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
            (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
          x :
        (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) =
    HSMul.hSMul (α := R) ((0 : (a : M) → R) m : R) x
have refine_2 : ∀ (x_1 : ℕ) (x_2 : Fin x_1 → M),
  Eq.{u_3 + 1} (α := N)
    ((((((LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        sorry sorry sorry sorry :
                      (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    m :
                  ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              ((((LinearMap.mk₂ R
                            (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                              (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                            sorry sorry sorry sorry :
                          (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                        m :
                      ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  x :
                (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              x_1 :
            M [⋀^Fin x_1]→ₗ[R] N) :
          (a : Fin x_1 → M) → N)
        x_2 :
      N)
    ((HSMul.hSMul (α := R) ((0 : (a : M) → R) m : R) x x_1 : (a : Fin x_1 → M) → N) x_2 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ Eq.{u_3 + 1} (α := 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)
        ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) :
      N)
    ((f 1 : (a : Fin 1 → M) → N) ![m] : N)
have dsimp : Eq.{u_3 + 1} (α := N)
  ((((((foldl 0
                      (LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        sorry sorry sorry sorry)
                      sorry :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  f :
                ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
              (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
            ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) 0 :
          M [⋀^Fin 0]→ₗ[R] N) :
        (a : Fin 0 → M) → N)
      0 :
    N)
  ((f 1 : (a : Fin 1 → M) → N) ![m] : N)
Tactic: dsimp [liftAlternating]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ Eq.{u_3 + 1} (α := N)
    ((((((foldl 0
                        (LinearMap.mk₂ R
                          (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                            (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                          ⋯ ⋯ ⋯ ⋯)
                        ⋯ :
                      (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    f :
                  ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
    ((f 1 : (a : Fin 1 → M) → N) ![m] : N)
have rw : Eq.{u_3 + 1} (α := N) ((f (HAdd.hAdd (α := ℕ) 0 1) : (a : Fin (Nat.succ 0) → M) → N) (Matrix.vecCons m 0) : N)
  ((f 1 : (a : Fin 1 → M) → N) ![m] : N)
Tactic: rw [foldl_ι, LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply]