awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn :
  HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M) *
      List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) =
    0
neg :
  (HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M) +
        HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)) *
      List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) =
    0
neg₁ :
  HMul.hMul (α := ExteriorAlgebra R M) 0
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ))) =
    0
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M) *
        List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) +
      HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M) *
        List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) =
    0
have neg₂ : Eq (α := ExteriorAlgebra R M) 0 0
Tactic: rw [← add_mul, ι_add_mul_swap, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
f : Fin n → M
i : Fin n
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i)) :
        ExteriorAlgebra R M) =
    0
have zero : ∀ (f : Fin 0 → M) (i : Fin 0),
  HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i)) :
        ExteriorAlgebra R M) =
    0
Tactic: induction n with
  | zero => exact i.elim0
  | succ n hn =>
    rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]
    by_cases h : i = 0
    · rw [h, ι_sq_zero, zero_mul]
    · replace hn :=
        congr_arg (ι R (f 0) * ·) <| hn (fun i => f <| Fin.succ i) (i.pred h)
      simp only at hn
      rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn
      refine (eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn
      rw [← add_mul, ι_add_mul_swap, zero_mul]
Cleared hypotheses: n, f, i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
f : Fin n → M
i : Fin n
zero :
  ∀ (f : Fin 0 → M) (i : Fin 0),
    HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M)
        (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i)) :
          ExteriorAlgebra R M) =
      0
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i)) :
        ExteriorAlgebra R M) =
    0
have succ : ∀ (n : ℕ)
  (hn :
    ∀ (f : Fin n → M) (i : Fin n),
      HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M)
          (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i)) :
            ExteriorAlgebra R M) =
        0)
  (f : Fin (n + 1) → M) (i : Fin (n + 1)),
  HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f i) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i)) :
        ExteriorAlgebra R M) =
    0
Tactic: induction n with
  | zero => exact i.elim0
  | succ n hn =>
    rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]
    by_cases h : i = 0
    · rw [h, ι_sq_zero, zero_mul]
    · replace hn :=
        congr_arg (ι R (f 0) * ·) <| hn (fun i => f <| Fin.succ i) (i.pred h)
      simp only at hn
      rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn
      refine (eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn
      rw [← add_mul, ι_add_mul_swap, zero_mul]
Cleared hypotheses: n, f, i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
F : MultilinearMap R (fun (x : Fin n) ↦ M) (ExteriorAlgebra R M) :=
  MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ ExteriorAlgebra R M)
    (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)) fun (x : Fin n) ↦ ι R
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ Eq (α := ExteriorAlgebra R M) ((F : (a : (i : Fin n) → M) → ExteriorAlgebra R M) f : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
have dsimp : Eq (α := ExteriorAlgebra R M)
  (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
Tactic: dsimp [F]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
have inr : ∀
  (this :
    ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_3 : AddCommGroup M] [inst_4 : Module R M] (n : ℕ)
      (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (hxy : x ≠ y) (h : x < y),
      Eq (α := ExteriorAlgebra R M)
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0)
  (h : ¬x < y),
  Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
Tactic: wlog h : x < y
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
inr :
  ∀
    (this :
      ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_3 : AddCommGroup M] [inst_4 : Module R M] (n : ℕ)
        (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (hxy : x ≠ y) (h : x < y),
        Eq (α := ExteriorAlgebra R M)
          (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0)
    (h : ¬x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
have wlog : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_3 : AddCommGroup M] [inst_4 : Module R M] (n : ℕ)
  (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (hxy : x ≠ y) (h : x < y),
  Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
Tactic: wlog h : x < y
Cleared hypotheses: n, f, x, y, hfxy, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
hn :
  ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
have succ : HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
    ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
      ExteriorAlgebra R M) =
  0
Tactic: rw [List.ofFn_succ, List.prod_cons]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
hn :
  ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
        ExteriorAlgebra R M) =
    0
have pos : ∀ (hx : x = 0),
  HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
        ExteriorAlgebra R M) =
    0
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
hn :
  ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
pos :
  ∀ (hx : x = 0),
    HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
          ExteriorAlgebra R M) =
      0
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
        ExteriorAlgebra R M) =
    0
have neg : ∀ (hx : ¬x = 0),
  HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
        ExteriorAlgebra R M) =
    0
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
hn :
  ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : x = 0
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
        ExteriorAlgebra R M) =
    0
have hfxy₁ : f 0 = f y
Tactic: rw [hx] at hfxy h
Cleared hypotheses: hfxy, h, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
hn :
  ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : x = 0
hfxy₁ : f 0 = f y
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
        ExteriorAlgebra R M) =
    0
have h₁ : 0 < y
Tactic: rw [hx] at hfxy h
Cleared hypotheses: hfxy, h, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
hn :
  ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f 0 = f y
h : 0 < y
hx : x = 0
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
        ExteriorAlgebra R M) =
    0
have pos : HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
    ((ι R : (a : M) → ExteriorAlgebra R M) (f (y.pred sorry).succ) : ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
      ExteriorAlgebra R M) =
  0
Tactic: rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
hn :
  ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) :
        ExteriorAlgebra R M) =
    0
have h₁ : Eq (α := ExteriorAlgebra R M)
  (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ))) 0
Tactic: convert! mul_zero (ι R (f 0))
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
hn :
  ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ))) 0
have h₁ : Eq.{u2 + 1} (α := M) ((fun (i : Fin n) ↦ f i.succ) (x.pred hx)) ((fun (i : Fin n) ↦ f i.succ) (y.pred sorry))
Tactic: refine
            hn
              (fun i => f <| Fin.succ i) (x.pred hx)
              (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) ?_
              (Fin.pred_lt_pred_iff.mpr h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
h : x < y
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
have zero : ∀ (f : Fin 0 → M) (x y : Fin 0) (hfxy : f x = f y) (h : x < y),
  Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
Tactic: induction n with
      | zero => exact x.elim0
      | succ n hn =>
        rw [List.ofFn_succ, List.prod_cons]
        by_cases hx : x = 0
        -- one of the repeated terms is on the left
        · rw [hx] at hfxy h
          rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]
          exact ι_mul_prod_list (f ∘ Fin.succ) _
        -- ignore the left-most term and induct on the remaining ones, decrementing indices
        · convert! mul_zero (ι R (f 0))
          refine
            hn
              (fun i => f <| Fin.succ i) (x.pred hx)
              (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) ?_
              (Fin.pred_lt_pred_iff.mpr h)
          simp only [Fin.succ_pred]
          exact hfxy
Cleared hypotheses: n, f, x, y, hfxy, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R_1 : Type u1
inst : CommRing R_1
M_1 : Type u2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u1
inst_3 : CommRing R
M : Type u2
inst_4 : AddCommGroup M
inst_5 : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
h : x < y
zero :
  ∀ (f : Fin 0 → M) (x y : Fin 0) (hfxy : f x = f y) (h : x < y),
    Eq (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
have succ : ∀ (n : ℕ)
  (hn :
    ∀ (f : Fin n → M) (x y : Fin n) (hfxy : f x = f y) (h : x < y),
      Eq (α := ExteriorAlgebra R M)
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0)
  (f : Fin (n + 1) → M) (x y : Fin (n + 1)) (hfxy : f x = f y) (h : x < y),
  Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i))) 0
Tactic: induction n with
      | zero => exact x.elim0
      | succ n hn =>
        rw [List.ofFn_succ, List.prod_cons]
        by_cases hx : x = 0
        -- one of the repeated terms is on the left
        · rw [hx] at hfxy h
          rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]
          exact ι_mul_prod_list (f ∘ Fin.succ) _
        -- ignore the left-most term and induct on the remaining ones, decrementing indices
        · convert! mul_zero (ι R (f 0))
          refine
            hn
              (fun i => f <| Fin.succ i) (x.pred hx)
              (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) ?_
              (Fin.pred_lt_pred_iff.mpr h)
          simp only [Fin.succ_pred]
          exact hfxy
Cleared hypotheses: n, f, x, y, hfxy, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
m : M
⊢ Eq (α := M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M)
    ((AlternatingMap.curryLeft (ιMulti R n.succ) : (a : M) → M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M) m :
      M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M)
    (LinearMap.compAlternatingMap (LinearMap.mulLeft R ((ι R : (a : M) → ExteriorAlgebra R M) m)) (ιMulti R n) :
      M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M)
have H : ∀ (x : Fin n → M),
  Eq (α := ExteriorAlgebra R M)
    ((((AlternatingMap.curryLeft (ιMulti R n.succ) : (a : M) → M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M) m :
            M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M) :
          (a : Fin n → M) → ExteriorAlgebra R M)
        x :
      ExteriorAlgebra R M)
    (((LinearMap.compAlternatingMap (LinearMap.mulLeft R ((ι R : (a : M) → ExteriorAlgebra R M) m)) (ιMulti R n) :
            M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M) :
          (a : Fin n → M) → ExteriorAlgebra R M)
        x :
      ExteriorAlgebra R M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
a : Fin m → M
b : Fin n → M
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ιMulti R m : (a : Fin m → M) → ExteriorAlgebra R M) a : ExteriorAlgebra R M)
      ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) b : ExteriorAlgebra R M) =
    (ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M) (Fin.append a b)
have simp : HMul.hMul (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := m) fun (i : Fin m) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (a i)))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (b i))) =
  List.prod (List.ofFn (n := m + n) fun (i : Fin (m + n)) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (Fin.append a b i))
Tactic: simp only [ιMulti_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
a : Fin m → M
b : Fin n → M
⊢ HMul.hMul (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := m) fun (i : Fin m) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (a i)))
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (b i))) =
    List.prod (List.ofFn ((⇑(ι R) : (a : M) → ExteriorAlgebra R M) ∘ Fin.append a b))
have rw : HMul.hMul (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := m) fun (i : Fin m) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (a i)))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (b i))) =
  HMul.hMul (α := ExteriorAlgebra R M) (List.prod (List.map (⇑(ι R) : (a : M) → ExteriorAlgebra R M) (List.ofFn a)))
    (List.prod (List.map (⇑(ι R) : (a : M) → ExteriorAlgebra R M) (List.ofFn b)))
Tactic: rw [← List.map_ofFn, List.ofFn_fin_append, List.map_append, List.prod_append]