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
refine_2 : Eq (α := ExteriorAlgebra R M) 0 ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) 0)
refine_2₁ refine_2₂ : Eq (α := ExteriorAlgebra R M) 0 0
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) 0)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) 0)

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
rw : ¬(x = 0 ∧ Eq.{u1 + 1} (α := R) 1 0)
⊢ Ne (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    (1 : ExteriorAlgebra R M)

Tactic:
rw [← (algebraMap R (ExteriorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]

Premises used: ExteriorAlgebra.ι_eq_algebraMap_iff, Algebra.algebraMap, ExteriorAlgebra, RingHom.map_one, Ne
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
⊢ ¬(x = 0 ∧ Eq.{u1 + 1} (α := R) 1 0)

Tactic:
one_ne_zero ∘ And.right

Premises used: Function.comp, And.right, one_ne_zero, Not
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
⊢ ¬(x = 0 ∧ Eq.{u1 + 1} (α := R) 1 0)

Tactic:
exact one_ne_zero ∘ And.right

Premises used: And.right, one_ne_zero
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
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
⊢ Disjoint (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) 1

Tactic:
rw [Submodule.disjoint_def]

Premises used: Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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)
⊢ x_1 = 0

Tactic:
obtain ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ := Submodule.mem_one.mp h

Premises used: Submodule.mem_one, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)
⊢ x = 0 ∧ r = 0

Tactic:
rw [ι_eq_algebraMap_iff x] at hx

Premises used: ExteriorAlgebra.ι_eq_algebraMap_iff
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)
hx₁ : x = 0 ∧ r = 0
⊢ 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)

Tactic:
rw [ι_eq_algebraMap_iff x] at hx

Premises used: ExteriorAlgebra.ι_eq_algebraMap_iff
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
rw₁ rw₂ : Eq (α := 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)

Tactic:
rw [hx.2, map_zero]

Premises used: map_zero, And.right
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M) +
      HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M) =
    0

Tactic:
CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho <| .all _ _

Premises used: QuadraticMap.IsOrtho.all, CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
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:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
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:
exact i.elim0

Premises used: Fin.elim0
-- 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 : ℕ
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)
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
⊢ 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:
rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]

Premises used: mul_assoc, List.prod_cons, 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 : ℕ
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
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
⊢ 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
-- 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 : ℕ
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
pos₂ pos₃ : Eq (α := ExteriorAlgebra R M) 0 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:
rw [h, ι_sq_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, ExteriorAlgebra.ι_sq_zero
-- 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 : ℕ
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
⊢ 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)
-- 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 + 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 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

Premises used: mul_assoc, MulZeroClass.mul_zero, Fin.succ_pred
-- 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 + 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

Tactic:
(eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn

Premises used: eq_zero_iff_eq_zero_of_add_eq_zero, Iff.mp
-- 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 + 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) *
        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
⊢ 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

Premises used: eq_zero_iff_eq_zero_of_add_eq_zero, Iff.mp
-- 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 + 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
neg₂ neg₃ : Eq (α := ExteriorAlgebra R M) 0 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

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

Premises used: add_mul, MulZeroClass.zero_mul, ExteriorAlgebra.ι_add_mul_swap
-- 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
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
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
⊢ 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

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]

Premises used: add_mul, MulZeroClass.zero_mul, mul_assoc, ExteriorAlgebra.ι_sq_zero, ExteriorAlgebra.ι_add_mul_swap, MulZeroClass.mul_zero, 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 : ℕ
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
dsimp :
  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) ((F : (a : (i : Fin n) → M) → ExteriorAlgebra R M) f : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)

Tactic:
dsimp [F]
-- 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
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
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
⊢ 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
-- 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:
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