awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
rw :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      (HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
        e0 Q)
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
rw₁ rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
⊢ HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
rw [← mul_assoc, e0_mul_v_mul_e0]

Premises used: mul_assoc, CliffordAlgebra.EquivEven.e0_mul_v_mul_e0
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))

Tactic:
have h1 : e0 Q * v Q m₁ * (e0 Q * v Q m₂) = v Q m₁ * v Q m₂ := by
                  rw [← mul_assoc, e0_mul_v_mul_e0]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
rw :
  -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    r₂ •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
rw₁ :
  -(r₂ •
        HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))) =
    r₂ •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
rw₂ :
  r₂ •
      -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    r₂ •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
rw₃ rw₄ :
  r₂ •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q) =
    r₂ •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
⊢ -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)

Tactic:
rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]

Premises used: CliffordAlgebra.EquivEven.neg_e0_mul_v, smul_neg, smul_mul_assoc, mul_smul_comm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
⊢ -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)

Tactic:
have h2 : -(r₂ • e0 Q * v Q m₁) = v Q m₁ * r₂ • e0 Q := by
                  rw [mul_smul_comm, smul_mul_assoc, ← smul_neg, neg_e0_mul_v]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
h2 :
  -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
rw : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = r₁ • e0 Q * r₂ • e0 Q
rw₁ : -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 = (r₁ * r₂) • (e0 Q * e0 Q)
rw₂ :
  -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 =
    HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) (-1)
rw₃ rw₄ :
  -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1 =
    -HSMul.hSMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₁ * r₂) 1
⊢ -(algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q)) (r₁ * r₂) =
    r₁ • e0 Q * r₂ • e0 Q

Tactic:
rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]

Premises used: smul_neg, smul_mul_smul_comm, Algebra.algebraMap_eq_smul_one, CliffordAlgebra.EquivEven.e0_mul_e0
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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₁_1 m₂_1 : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) *
      HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₂ : CliffordAlgebra (R := R) (M := M × R) (Q' Q))
h2 :
  -HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
        ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) =
    HMul.hMul (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
      ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m₁ : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (r₂ • e0 Q)
⊢ -(algebraMap R (CliffordAlgebra (R := R) (M := M × R) (Q' Q)) : (a : R) → CliffordAlgebra (Q' Q)) (r₁ * r₂) =
    r₁ • e0 Q * r₂ • e0 Q

Tactic:
have h3 : -algebraMap R _ (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q := by
                  rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
rw rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
        ((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    ((ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
        ((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
        ((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    ((ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
        (Subtype.mk (p := fun (x : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) ↦
          Membership.mem (γ := Subalgebra R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (even (Q' Q)) x)
          (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
            CliffordAlgebra (Q' Q))
          ⋯) :
      CliffordAlgebra Q)

Tactic:
rw [Subtype.coe_eta]

Premises used: Subtype.coe_eta
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
simp_rw :
  (ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
      (Subtype.mk (p := fun (x : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) ↦
        Membership.mem (γ := Subalgebra R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (even (Q' Q)) x)
        (HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)))
        ⋯) =
    HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q)
⊢ (ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
      (Subtype.mk (p := fun (x : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) ↦
        Membership.mem (γ := Subalgebra R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (even (Q' Q)) x)
        (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
          CliffordAlgebra (Q' Q))
        ⋯) =
    HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q)

Tactic:
simp_rw [toEven_ι]

Premises used: CliffordAlgebra.toEven_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
⊢ (ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
      (Subtype.mk (p := fun (x : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) ↦
        Membership.mem (γ := Subalgebra R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (even (Q' Q)) x)
        (HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)))
        ⋯) =
    HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q)

Tactic:
ofEven_ι Q _ _

Premises used: CliffordAlgebra.EquivEven.e0, CliffordAlgebra.ofEven_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
⊢ (ofEven Q : (a : ↥(even (Q' Q))) → CliffordAlgebra Q)
      (Subtype.mk (p := fun (x : CliffordAlgebra (R := R) (M := M × R) (Q' Q)) ↦
        Membership.mem (γ := Subalgebra R (CliffordAlgebra (R := R) (M := M × R) (Q' Q))) (even (Q' Q)) x)
        (HMul.hMul (β := CliffordAlgebra (R := R) (M := M × R) (Q' Q)) (e0 Q)
          ((v Q : (a : M) → CliffordAlgebra (Q' Q)) m : CliffordAlgebra (R := R) (M := M × R) (Q' Q)))
        ⋯) =
    HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q)

Tactic:
exact ofEven_ι Q _ _

Premises used: CliffordAlgebra.ofEven_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
rw :
  HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0) 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₁ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₂ :
  HAdd.hAdd (α := CliffordAlgebra Q) 0 1 *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) (0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₃ :
  HMul.hMul (β := CliffordAlgebra Q) (HAdd.hAdd (α := CliffordAlgebra Q) 0 1)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₄ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) (1 : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m
rw₅ rw₆ :
  Eq (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ HAdd.hAdd (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) 0)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) *
      HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q) m

Tactic:
rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]

Premises used: sub_zero, map_zero, zero_add, map_one, one_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
r : R
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra (Q' Q)))

Tactic:
simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]

Premises used: Subalgebra.coe_algebraMap, CliffordAlgebra.reverse.commutes, AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m)))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
        CliffordAlgebra (Q' Q)))

Tactic:
simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
      reverse_ι, neg_e0_mul_v, map_neg]

Premises used: CliffordAlgebra.EquivEven.reverse_e0, CliffordAlgebra.EquivEven.neg_e0_mul_v, map_neg, CliffordAlgebra.reverse.map_mul, Subalgebra.coe_neg, CliffordAlgebra.involute_ι, CliffordAlgebra.toEven_ι, CliffordAlgebra.EquivEven.reverse_v, CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
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
x y : CliffordAlgebra Q
hx :
  Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) x) : CliffordAlgebra (Q' Q)))
hy :
  Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) y) : CliffordAlgebra (Q' Q)))
⊢ Eq (α := CliffordAlgebra (R := R) (M := M × R) (Q' Q))
    (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q)))
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x * y)))) :
      CliffordAlgebra (Q' Q))
    ((reverse : (a : CliffordAlgebra (Q' Q)) → CliffordAlgebra (Q' Q))
      (↑((toEven Q : (a : CliffordAlgebra Q) → ↥(even (Q' Q))) (x * y)) : CliffordAlgebra (Q' Q)))

Tactic:
simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]

Premises used: Subalgebra.coe_mul, CliffordAlgebra.reverse.map_mul, map_mul