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
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
x : ExteriorAlgebra R 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)
        (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) x) :
      N)
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) fun (i : ℕ) ↦
            (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m :
          (a : ExteriorAlgebra R M) → N)
        x :
      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)
            (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) x) 0 :
          M [⋀^Fin 0]→ₗ[R] N) :
        (a : Fin 0 → M) → N)
      0 :
    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)
                fun (i : ℕ) ↦ (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m :
              (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
            x 0 :
          M [⋀^Fin 0]→ₗ[R] N) :
        (a : Fin 0 → M) → N)
      0 :
    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
⊢ 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)
        1 :
      N)
    ((f 0 : (a : Fin 0 → M) → N) 0 : 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)
          1 0 :
        (a : Fin 0 → M) → N)
      0 :
    N)
  ((f 0 : (a : Fin 0 → M) → N) 0 : 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
⊢ 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)
            1 0 :
          (a : Fin 0 → M) → N)
        0 :
      N)
    ((f 0 : (a : Fin 0 → M) → N) 0 : N)
have rw : Eq.{u_3 + 1} (α := N) ((f 0 : (a : Fin 0 → M) → N) 0 : N) ((f 0 : (a : Fin 0 → M) → N) 0 : N)
Tactic: rw [foldl_one]
-- 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
r : R
⊢ (((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 (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
have rw : (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
        ExteriorAlgebra R M →ₗ[R] N) :
      (a : ExteriorAlgebra R M) → N)
    (HSMul.hSMul (β := ExteriorAlgebra R M) r 1) =
  HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
Tactic: rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]
-- 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
r : R
rw :
  (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
          ExteriorAlgebra R M →ₗ[R] N) :
        (a : ExteriorAlgebra R M) → N)
      (HSMul.hSMul (β := ExteriorAlgebra R M) r 1) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : 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 (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
have rw₁ : HSMul.hSMul (β := N) r
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        1 :
      N) =
  HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
Tactic: rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]
-- 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
r : R
rw :
  (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
          ExteriorAlgebra R M →ₗ[R] N) :
        (a : ExteriorAlgebra R M) → N)
      (HSMul.hSMul (β := ExteriorAlgebra R M) r 1) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
rw₁ :
  HSMul.hSMul (β := N) r
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          1 :
        N) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : 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 (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
have rw₂ : HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N) = HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
Tactic: rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]
-- 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
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → 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)
        ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M) :
      N)
    ((f n : (a : Fin n → M) → N) v : N)
have rw : 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)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
    N)
  ((f n : (a : Fin n → M) → N) v : N)
Tactic: rw [ιMulti_apply]
-- 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
v : Fin 0 → 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)
        (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
have zero : 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)
      (List.prod []) :
    N)
  ((f 0 : (a : Fin 0 → M) → N) v : N)
Tactic: rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
-- 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
v : Fin 0 → M
zero :
  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)
        (List.prod []) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
⊢ 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)
        (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
have zero₁ : 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)
      1 :
    N)
  ((f 0 : (a : Fin 0 → M) → N) v : N)
Tactic: rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
-- 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
v : Fin 0 → M
zero :
  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)
        (List.prod []) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
zero₁ :
  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)
        1 :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
⊢ 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)
        (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
have zero₂ : Eq.{u_3 + 1} (α := N) ((f 0 : (a : Fin 0 → M) → N) 0 : N) ((f 0 : (a : Fin 0 → M) → N) v : N)
Tactic: rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
-- 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
v : Fin 0 → M
zero :
  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)
        (List.prod []) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
zero₁ :
  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)
        1 :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
zero₂ : Eq.{u_3 + 1} (α := N) ((f 0 : (a : Fin 0 → M) → N) 0 : N) ((f 0 : (a : Fin 0 → M) → N) v : N)
⊢ 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)
        (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
have zero₃ : Eq.{u_3 + 1} (α := N) ((f 0 : (a : Fin 0 → M) → N) v : N) ((f 0 : (a : Fin 0 → M) → N) v : N)
Tactic: rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
-- 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
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → 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)
          (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f n : (a : Fin n → M) → N) v : N)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → 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)
        (List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f (n + 1) : (a : Fin (n + 1) → M) → N) v : N)
have succ : Eq.{u_3 + 1} (α := N) ((f n.succ : (a : Fin n.succ → M) → N) (Matrix.vecCons (v 0) fun (i : Fin n) ↦ v i.succ) : N)
  ((f (n + 1) : (a : Fin (n + 1) → M) → N) v : N)
Tactic: rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
      AlternatingMap.curryLeft_apply_apply]
-- 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
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → 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)
          (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f n : (a : Fin n → M) → N) v : N)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ Eq.{u_3 + 1} (α := N) ((f n.succ : (a : Fin n.succ → M) → N) (Matrix.vecCons (v 0) fun (i : Fin n) ↦ v i.succ) : N)
    ((f (n + 1) : (a : Fin (n + 1) → M) → N) v : N)
have succ : (Matrix.vecCons (v 0) fun (i : Fin n) ↦ v i.succ) = v
Tactic: congr
-- 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
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → 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)
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f n : (a : Fin n → M) → N) v : N)
have zero : ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin 0 → 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)
        (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
Tactic: induction n generalizing f with
  | zero => rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
  | succ n ih =>
    rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
      AlternatingMap.curryLeft_apply_apply]
    congr
    exact Matrix.cons_head_tail _
Cleared hypotheses: n, 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
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
zero :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin 0 → 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)
          (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f 0 : (a : Fin 0 → M) → N) v : N)
⊢ 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)
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f n : (a : Fin n → M) → N) v : N)
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → 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)
            (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
          N)
        ((f n : (a : Fin n → M) → N) v : N))
  (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin (n + 1) → 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)
        (List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f (n + 1) : (a : Fin (n + 1) → M) → N) v : N)
Tactic: induction n generalizing f with
  | zero => rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
  | succ n ih =>
    rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
      AlternatingMap.curryLeft_apply_apply]
    congr
    exact Matrix.cons_head_tail _
Cleared hypotheses: n, 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'
g : N →ₗ[R] N'
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ Eq (α := ExteriorAlgebra R M →ₗ[R] N')
    ((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
      g.compAlternatingMap (f i))
    (g ∘ₗ (liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f)
have h : ∀ (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 ∘ₗ (liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
          (a : ExteriorAlgebra R M) → N')
        v :
      N')
Tactic: ext 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'
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 ∘ₗ (liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
          (a : ExteriorAlgebra R M) → N')
        v :
      N')
have h : 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')
Tactic: rw [LinearMap.comp_apply]