-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem ι_mul_prod_list {n : ℕ} (f : Fin n → M) (i : Fin n) :
    (ι R <| f i) * (List.ofFn fun i => ι R <| f i).prod = 0

Proof state:
case succ
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i => (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
⊢ (ι R) (f i) * (List.ofFn fun i => (ι R) (f i)).prod = 0

Tactic:
rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]

Result:
case succ
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i => (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Proof state:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn :
  (fun x => (ι R) (f 0) * x) ((ι R) (f (i.pred h).succ) * (List.ofFn fun i => (ι R) (f i.succ)).prod) =
    (fun x => (ι R) (f 0) * x) 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Tactic:
simp only at hn

Result:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * ((ι R) (f (i.pred h).succ) * (List.ofFn fun i => (ι R) (f i.succ)).prod) = (ι R) (f 0) * 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Proof state:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Tactic:
refine (eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn

Result:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0
⊢ (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i => (ι R) (f i.succ)).prod +
      (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod =
    0

Proof state:
case zero
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 0 → M
i : Fin 0
⊢ (ι R) (f i) * (List.ofFn fun i => (ι R) (f i)).prod = 0

Tactic:
exact i.elim0

Result:
no goals

Proof state:
case pos
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i => (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : i = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Tactic:
rw [h, ι_sq_zero, zero_mul]

Result:
no goals

Proof state:
case succ
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i => (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Tactic:
by_cases h : i = 0

Result:
case pos
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i => (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : i = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i => (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Proof state:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * ((ι R) (f (i.pred h).succ) * (List.ofFn fun i => (ι R) (f i.succ)).prod) = (ι R) (f 0) * 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Tactic:
rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn

Result:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0

Proof state:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i => (ι R) (f i.succ)).prod = 0
⊢ (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i => (ι R) (f i.succ)).prod +
      (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i => (ι R) (f i.succ)).prod =
    0

Tactic:
rw [← add_mul, ι_add_mul_swap, zero_mul]

Result:
no goals