awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)
⊢ x = 0 ∧ r = 0
have this₁ : r = 0 ∧ 0 = x
Tactic: have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
-- 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
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) 0)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) 0)
have refine_2 : Eq (α := ExteriorAlgebra R M) 0 ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) 0)
Tactic: rw [map_zero, map_zero]
-- 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
refine_2 : Eq (α := ExteriorAlgebra R M) 0 ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) 0)
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) 0)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) 0)
have refine_2₁ : Eq (α := ExteriorAlgebra R M) 0 0
Tactic: rw [map_zero, map_zero]
-- 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
inst_3 : Nontrivial R
x : M
⊢ Ne (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    (1 : ExteriorAlgebra R M)
have rw : ¬(x = 0 ∧ Eq.{u1 + 1} (α := R) 1 0)
Tactic: rw [← (algebraMap R (ExteriorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]
-- 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
⊢ Disjoint (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) 1
have rw : ∀ (x : ExteriorAlgebra R M),
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) x →
    Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) 1 x → x = 0
Tactic: rw [Submodule.disjoint_def]
-- 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
x_1 : ExteriorAlgebra R M
x : M
hx : (ι R : (a : M) → ExteriorAlgebra R M) x = x_1
h : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) 1 x_1
⊢ x_1 = 0
have obtain : ∀ (r : R)
  (hx :
    Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M))
  (h :
    Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M)) 1
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)),
  Eq (α := ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
Tactic: obtain ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ := Submodule.mem_one.mp h
Cleared hypotheses: x_1, hx, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
hx :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
h :
  Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M)) 1
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
have hx₁ : x = 0 ∧ r = 0
Tactic: rw [ι_eq_algebraMap_iff x] at hx
Cleared hypotheses: hx, 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
x : M
r : R
hx : x = 0 ∧ r = 0
h :
  Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M)) 1
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
have rw : Eq (α := ExteriorAlgebra R M) ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) 0) 0
Tactic: rw [hx.2, map_zero]
-- 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
x : M
r : R
hx : x = 0 ∧ r = 0
h :
  Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M)) 1
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
rw : Eq (α := ExteriorAlgebra R M) ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) 0) 0
⊢ Eq (α := ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
have rw₁ : Eq (α := ExteriorAlgebra R M) 0 0
Tactic: rw [hx.2, map_zero]
-- 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 : ℕ
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
have 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
Tactic: rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]
-- 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 : ℕ
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)
        ((ι 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 pos : ∀ (h : i = 0),
  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
Tactic: by_cases h : i = 0
-- 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 : ℕ
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)
pos :
  ∀ (h : i = 0),
    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
⊢ 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 : ∀ (h : ¬i = 0),
  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
Tactic: by_cases h : i = 0
-- 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 : ℕ
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)
h : i = 0
⊢ 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 pos : 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 0) : ExteriorAlgebra R M) *
    List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) =
  0
Tactic: rw [h, ι_sq_zero, 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 : ℕ
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)
h : i = 0
pos :
  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 0) : 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 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 pos₁ : 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
Tactic: rw [h, ι_sq_zero, 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 : ℕ
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)
h : i = 0
pos :
  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 0) : ExteriorAlgebra R M) *
      List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (f i.succ)) =
    0
pos₁ :
  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 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 pos₂ : Eq (α := ExteriorAlgebra R M) 0 0
Tactic: rw [h, ι_sq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
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)
h : ¬i = 0
⊢ 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 hn₁ : Eq (α := ExteriorAlgebra R M)
  ((fun (x : ExteriorAlgebra R M) ↦
      HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M) x)
    (HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f (i.pred h).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)))
  ((fun (x : ExteriorAlgebra R M) ↦
      HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M) x)
    0)
Tactic: replace hn :=
        congr_arg (ι R (f 0) * ·) <| hn (fun i => f <| Fin.succ i) (i.pred h)
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
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) ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M)
      (HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) (f (i.pred h).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)) =
    HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) (f 0) : ExteriorAlgebra R M) (0 : 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
have 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
Tactic: rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn
Cleared hypotheses: hn
-- 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
⊢ 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 : 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
Tactic: refine (eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn
-- 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
⊢ 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 : (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
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 + 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
⊢ 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₁ : 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
Tactic: rw [← add_mul, ι_add_mul_swap, zero_mul]