awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx →
      P
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
refine : ∀ (ιv : CliffordAlgebra Q) (h : ιv ∈ (CliffordAlgebra.ι Q).range ^ ZMod.val (n := 2) 1), P ιv ⋯
⊢ P x hx

Tactic:
refine evenOdd_induction _ _ (motive := P) (fun ιv => ?_) add ι_mul_ι_mul x hx

Premises used: CliffordAlgebra.evenOdd_induction
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx →
      P
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
ιv : CliffordAlgebra Q
simp_rw : ∀ (h : ιv ∈ (CliffordAlgebra.ι Q).range), P ιv ⋯
⊢ ∀ (h : ιv ∈ (CliffordAlgebra.ι Q).range ^ ZMod.val (n := 2) 1), P ιv ⋯

Tactic:
simp_rw [ZMod.val_one, pow_one]

Premises used: pow_one, ZMod.val_one
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx →
      P
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
v : M
⊢ P ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) v) ⋯

Tactic:
ι v
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx →
      P
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
v : M
⊢ P ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) v) ⋯

Tactic:
exact ι v
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₄ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
          ((Q : (a : M) → R) m : R)) :
      CliffordAlgebra Q)
    (1 : CliffordAlgebra Q)
rw₅ : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) 1
rw₆ rw₇ : Eq (α := CliffordAlgebra Q) 1 1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    1

Tactic:
rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]

Premises used: CliffordAlgebra.ι_sq_scalar, invOf_mul_self, smul_mul_assoc, map_mul, map_one, Algebra.smul_def, map_smul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₄ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
          ((Q : (a : M) → R) m : R)) :
      CliffordAlgebra Q)
    (1 : CliffordAlgebra Q)
rw₅ : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) 1
rw₆ rw₇ : Eq (α := CliffordAlgebra Q) 1 1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q) =
    1

Tactic:
rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]

Premises used: CliffordAlgebra.ι_sq_scalar, invOf_mul_self, map_mul, map_one, mul_smul_comm, Algebra.smul_def, map_smul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
inst_4 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
this : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :=
  invertibleιOfInvertible Q m
⊢ Eq (α := CliffordAlgebra Q)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) m) _ :
      CliffordAlgebra Q)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) m) _ :
      CliffordAlgebra Q)

Tactic:
(rfl : ⅟(ι Q m) = _)

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
inst_4 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
this : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :=
  invertibleιOfInvertible Q m
⊢ Eq (α := CliffordAlgebra Q)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) m) _ :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
      CliffordAlgebra Q)

Tactic:
convert! (rfl : ⅟(ι Q m) = _)

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)
intro :
  ∀ (val : Invertible (α := R) ((Q : (a : M) → R) m : R)),
    IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
cases h.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)
val : Invertible (α := R) ((Q : (a : M) → R) m : R)
this : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :=
  invertibleιOfInvertible Q m
⊢ IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
isUnit_of_invertible (ι Q m)

Premises used: CliffordAlgebra.ι, isUnit_of_invertible, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)
val : Invertible (α := R) ((Q : (a : M) → R) m : R)
this : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) :=
  invertibleιOfInvertible Q m
⊢ IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
exact isUnit_of_invertible (ι Q m)

Premises used: CliffordAlgebra.ι, isUnit_of_invertible, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
m : M
inst_4 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ Eq (α := ExteriorAlgebra R M)
    (((↑(equivExterior Q) : CliffordAlgebra Q →ₗ[R] ExteriorAlgebra R M) :
        (a : CliffordAlgebra Q) → ExteriorAlgebra R M)
      1)
    1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
m : M
h : IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
intro :
  ∀ (val : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)),
    IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)
⊢ IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)

Tactic:
cases h.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
m : M
h : IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
val : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
this : Invertible (α := R) ((Q : (a : M) → R) m : R) := invertibleOfInvertibleι Q m
⊢ IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)

Tactic:
isUnit_of_invertible (Q m)

Premises used: isUnit_of_invertible, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
m : M
h : IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
val : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
this : Invertible (α := R) ((Q : (a : M) → R) m : R) := invertibleOfInvertibleι Q m
⊢ IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)

Tactic:
exact isUnit_of_invertible (Q m)

Premises used: isUnit_of_invertible, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
m : M
⊢ IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) ↔
    IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)

Tactic:
⟨isUnit_of_isUnit_ι Q, isUnit_ι_of_isUnit Q⟩

Premises used: CliffordAlgebra.isUnit_of_isUnit_ι, Iff.intro, CliffordAlgebra.isUnit_ι_of_isUnit
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ ((f₁ : (a : M₁) → N) x) ((f₂ : (a : M₂) → N) y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
zero :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
zero₁ :
  0 =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
zero₂ : 0 = HSMul.hSMul (β := CliffordAlgebra Qₙ) (HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁)) 0
zero₃ zero₄ : Eq (α := CliffordAlgebra Qₙ) 0 0
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)

Tactic:
rw [map_zero, zero_mul, mul_zero, smul_zero]

Premises used: MulZeroClass.zero_mul, smul_zero, map_zero, MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ ((f₁ : (a : M₁) → N) x) ((f₂ : (a : M₂) → N) y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
i₁' : { n : ℕ // (↑n : ZMod 2) = i₁ }
m₁' : CliffordAlgebra Q₁
hm₁ : m₁' ∈ (ι Q₁).range ^ (↑i₁' : ℕ)
mem :
  ∀ (i₁n : ℕ)
    (hm₁ :
      m₁' ∈
        (ι Q₁).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑i₁n : ZMod 2)) i₁n ⋯) : ℕ)),
    HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) m₁' : CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
      HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑i₁n : ZMod 2)) •
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) m₁' : CliffordAlgebra Qₙ)
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) m₁' : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) m₁' : CliffordAlgebra Qₙ)

Tactic:
obtain ⟨i₁n, rfl⟩ := i₁'

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ ((f₁ : (a : M₁) → N) x) ((f₂ : (a : M₂) → N) y)
m₁_1 : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n : ℕ
m₁ : CliffordAlgebra Q₁
hm₁ : m₁ ∈ (ι Q₁).range
i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
ih₁ :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x₁ : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑i : ZMod 2)) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) x₁ : CliffordAlgebra Qₙ)
mem :
  ∀ (v₁ : M₁),
    HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ)
            (HMul.hMul (α := CliffordAlgebra Q₁) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) v₁ : CliffordAlgebra Q₁) x₁) :
          CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
      HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑i.succ : ZMod 2)) •
        HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
          ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
          ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ)
              (HMul.hMul (α := CliffordAlgebra Q₁) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) v₁ : CliffordAlgebra Q₁)
                x₁) :
            CliffordAlgebra Qₙ)
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) (m₁ * x₁) : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * (↑i.succ : ZMod 2)) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) (m₁ * x₁) : CliffordAlgebra Qₙ)

Tactic:
obtain ⟨v₁, rfl⟩ := hm₁

Premises used: rfl