awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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:
exact this R n f y x hfxy.symm hxy.symm (hxy.lt_or_gt.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Eq.symm, Ne.lt_or_gt
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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:
x.elim0

Premises used: Fin.elim0
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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:
exact x.elim0

Premises used: Fin.elim0
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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
⊢ 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:
rw [List.ofFn_succ, List.prod_cons]

Premises used: List.prod_cons, List.ofFn_succ
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
⊢ f 0 = f y

Tactic:
rw [hx] at hfxy h
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
⊢ 0 < y

Tactic:
rw [hx] at hfxy h
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
h₁ : 0 < y
⊢ x = 0

Tactic:
rw [hx] at hfxy h
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
pos :
  HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f (y.pred ⋯).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
⊢ 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 [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]

Premises used: Ne.symm, ne_of_lt, Fin.succ_pred
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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 (y.pred ⋯).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:
ι_mul_prod_list (f ∘ Fin.succ) _

Premises used: Fin.succ, Function.comp, ExteriorAlgebra.ι_mul_prod_list
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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 (y.pred ⋯).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:
exact ι_mul_prod_list (f ∘ Fin.succ) _

Premises used: Fin.succ, Function.comp, ExteriorAlgebra.ι_mul_prod_list
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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) (0 : ExteriorAlgebra R M) =
    0

Tactic:
mul_zero (ι R (f 0))

Premises used: MulZeroClass.mul_zero, ExteriorAlgebra.ι, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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
⊢ 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:
convert! mul_zero (ι R (f 0))

Premises used: MulZeroClass.mul_zero, ExteriorAlgebra.ι, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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

Tactic:
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)

Premises used: Iff.mpr, lt_of_le_of_lt, Fin.succ, Fin.pred, Fin.zero_le, Ne.symm, Fin.pred_lt_pred_iff, ne_of_lt
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
h₁ : Eq.{u2 + 1} (α := M) ((fun (i : Fin n) ↦ f i.succ) (x.pred hx)) ((fun (i : Fin n) ↦ f i.succ) (y.pred ⋯))
⊢ 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:
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)

Premises used: Iff.mpr, lt_of_le_of_lt, Fin.succ, Fin.pred, Fin.zero_le, Ne.symm, Fin.pred_lt_pred_iff, ne_of_lt
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
h₁ : f x = f y
⊢ Eq.{u2 + 1} (α := M) ((fun (i : Fin n) ↦ f i.succ) (x.pred hx)) ((fun (i : Fin n) ↦ f i.succ) (y.pred ⋯))

Tactic:
simp only [Fin.succ_pred]

Premises used: Fin.succ_pred
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
⊢ f x = f y

Tactic:
hfxy
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
⊢ f x = f y

Tactic:
exact hfxy
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι 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

Premises used: Function.comp, ExteriorAlgebra.ι_mul_prod_list, List.prod_cons, Fin.succ_pred, List.ofFn_succ
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n → M
⊢ Eq (α := ExteriorAlgebra R M) ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i)) : ExteriorAlgebra R M)

Tactic:
rfl

Premises used: rfl, List.prod
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
v : Fin 0 → M
⊢ Eq (α := ExteriorAlgebra R M) ((ιMulti R 0 : (a : Fin 0 → M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)
    (1 : ExteriorAlgebra R M)

Tactic:
simp [ιMulti]

Premises used: ExteriorAlgebra.ιMulti
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n.succ → M
⊢ (ιMulti R n.succ : (a : Fin n.succ → M) → ExteriorAlgebra R M) v =
    HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (v 0) : ExteriorAlgebra R M)
      ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (Matrix.vecTail v) : ExteriorAlgebra R M)

Tactic:
simp [ιMulti, Matrix.vecTail]

Premises used: ExteriorAlgebra.ιMulti, Matrix.vecTail
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
m : M
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
m : M
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:
simp
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n → M
hv : ¬Function.Injective v
⊢ Eq (α := ExteriorAlgebra R M) ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)

Tactic:
(ιMulti R n).map_eq_zero_of_not_injective v hv

Premises used: ExteriorAlgebra.ιMulti, AlternatingMap.map_eq_zero_of_not_injective
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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))
⊢ 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)

Tactic:
simp only [ιMulti_apply]

Premises used: ExteriorAlgebra.ιMulti_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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)))
⊢ 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))

Tactic:
rw [← List.map_ofFn, List.ofFn_fin_append, List.map_append, List.prod_append]

Premises used: List.prod_append, List.ofFn_fin_append, List.map_ofFn, List.map_append
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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))) =
    HMul.hMul (α := ExteriorAlgebra R M) (List.prod (List.ofFn ((⇑(ι R) : (a : M) → ExteriorAlgebra R M) ∘ a)))
      (List.prod (List.ofFn ((⇑(ι R) : (a : M) → ExteriorAlgebra R M) ∘ b)))
⊢ 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:
simp only [List.map_ofFn]

Premises used: List.map_ofFn