awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ Eq (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    (((AlgHom.toLinearMap (AlgHom.comp ofQuaternion toQuaternion) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R :
        (a : R) → CliffordAlgebra (Q c₁ c₂))
      1)
    (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))) ∘ₗ ι (Q c₁ c₂)) ∘ₗ
          LinearMap.inr R R R :
        (a : R) → CliffordAlgebra (Q c₁ c₂))
      1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)
⊢ (ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂))
      ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) c) =
    c

Tactic:
AlgHom.congr_fun ofQuaternion_comp_toQuaternion c

Premises used: QuaternionAlgebra.Basis.lift, AlgHom.congr_fun, CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
hi :
  Eq (α := ℍ[R,c₁,c₂])
    ((AlgHom.comp toQuaternion ofQuaternion : (a : ℍ[R,c₁,c₂]) → ℍ[R,c₁,c₂]) (Basis.i (Basis.self R)) : ℍ[R,c₁,c₂])
    ((AlgHom.id R ℍ[R,c₁,c₂] : (a : ℍ[R,c₁,c₂]) → ℍ[R,c₁,c₂]) (Basis.i (Basis.self R)) : ℍ[R,c₁,c₂])
hj :
  Eq (α := ℍ[R,c₁,c₂])
    ((AlgHom.comp toQuaternion ofQuaternion : (a : ℍ[R,c₁,c₂]) → ℍ[R,c₁,c₂]) (Basis.j (Basis.self R)) : ℍ[R,c₁,c₂])
    ((AlgHom.id R ℍ[R,c₁,c₂] : (a : ℍ[R,c₁,c₂]) → ℍ[R,c₁,c₂]) (Basis.j (Basis.self R)) : ℍ[R,c₁,c₂])
⊢ Eq (α := ℍ[R,c₁,c₂] →ₐ[R] ℍ[R,c₁,c₂]) (AlgHom.comp toQuaternion ofQuaternion) (AlgHom.id R ℍ[R,c₁,c₂])

Tactic:
ext : 1
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((AlgHom.comp toQuaternion ofQuaternion : (a : ℍ[R,c₁,c₂]) → ℍ[R,c₁,c₂]) (Basis.i (Basis.self R)) : ℍ[R,c₁,c₂])
    ((AlgHom.id R ℍ[R,c₁,c₂] : (a : ℍ[R,c₁,c₂]) → ℍ[R,c₁,c₂]) (Basis.i (Basis.self R)) : ℍ[R,c₁,c₂])

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((AlgHom.comp toQuaternion ofQuaternion : (a : ℍ[R,c₁,c₂]) → ℍ[R,c₁,c₂]) (Basis.j (Basis.self R)) : ℍ[R,c₁,c₂])
    ((AlgHom.id R ℍ[R,c₁,c₂] : (a : ℍ[R,c₁,c₂]) → ℍ[R,c₁,c₂]) (Basis.j (Basis.self R)) : ℍ[R,c₁,c₂])

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
q : ℍ[R,c₁,c₂]
⊢ (toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
      ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q) =
    q

Tactic:
AlgHom.congr_fun toQuaternion_comp_ofQuaternion q

Premises used: CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion, QuaternionAlgebra.Basis.lift, AlgHom.congr_fun
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
q : ℍ[R,c₁,c₂]
rw :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
rw₁ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
rw₂ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    (star
        ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
          ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])
rw₃ :
  star q =
    star
      ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q))
rw₄ rw₅ : star q = star q
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) (star q)) :
      ℍ[R,c₁,c₂])
    ((CliffordAlgebraQuaternion.equiv : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        (star ((ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) q)) :
      ℍ[R,c₁,c₂])

Tactic:
rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
      toQuaternion_ofQuaternion]

Premises used: CliffordAlgebraQuaternion.toQuaternion_star, CliffordAlgebraQuaternion.toQuaternion_ofQuaternion, CliffordAlgebraQuaternion.equiv_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
r₁ r₂ : R
rw :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₁ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₁ * 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₂ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (r₂ * 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₃ :
  HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₁ 1) : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₄ :
  HMul.hMul (β := CliffordAlgebra (R := R) (M := R) 0)
      (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1))
      ((ι 0 : (a : R) → CliffordAlgebra 0) (HSMul.hSMul (β := R) r₂ 1) : CliffordAlgebra (R := R) (M := R) 0) =
    0
rw₅ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₁ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) *
      HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) r₂ ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₆ :
  (r₁ * r₂) •
      HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) ((ι 0 : (a : R) → CliffordAlgebra 0) 1)
        ((ι 0 : (a : R) → CliffordAlgebra 0) 1) =
    0
rw₇ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
      ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) ((0 : (a : R) → R) 1)) =
    0
rw₈ :
  HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂)
      ((algebraMap R (CliffordAlgebra (R := R) (M := R) 0) : (a : R) → CliffordAlgebra 0) 0) =
    0
rw₉ : HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R) 0) (r₁ * r₂) 0 = 0
rw₁₀ rw₁₁ : Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := R) 0) 0 0
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R) 0) (β := CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₁ : CliffordAlgebra (R := R) (M := R) 0)
      ((ι 0 : (a : R) → CliffordAlgebra 0) r₂ : CliffordAlgebra (R := R) (M := R) 0) =
    0

Tactic:
rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero]

Premises used: CliffordAlgebra.ι_sq_scalar, QuadraticMap.zero_apply, smul_zero, map_zero, smul_mul_smul_comm, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[ε])
    ((AlgHom.comp (B := CliffordAlgebra (R := R) (M := R) 0)
            (((CliffordAlgebra.lift.{u_1, u_1, u_1} (R := R) (M := R) 0 (A := R[ε]) :
                  { f : R →ₗ[R] R[ε] //
                      ∀ (m : R),
                        HMul.hMul (α := R[ε]) (β := R[ε]) ((f : (a : R) → R[ε]) m : R[ε])
                            ((f : (a : R) → R[ε]) m : R[ε]) =
                          (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m : R) } ≃
                    (CliffordAlgebra (R := R) (M := R) 0 →ₐ[R] R[ε])) :
                (a :
                    { f : R →ₗ[R] R[ε] //
                      ∀ (m : R),
                        (f : (a : R) → R[ε]) m * (f : (a : R) → R[ε]) m =
                          (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m) }) →
                  CliffordAlgebra 0 →ₐ[R] R[ε])
              (Subtype.mk (p := fun (f : R →ₗ[R] R[ε]) ↦
                ∀ (m : R),
                  HMul.hMul (α := R[ε]) (β := R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) =
                    (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m : R))
                (inrHom R R) ⋯))
            ((DualNumber.lift :
                (a :
                    { fe : (R →ₐ[R] CliffordAlgebra 0) × CliffordAlgebra 0 //
                      fe.2 * fe.2 = 0 ∧ ∀ (a : R), Commute fe.2 ((fe.1 : (a : R) → CliffordAlgebra 0) a) }) →
                  R[ε] →ₐ[R] CliffordAlgebra 0)
              (Subtype.mk (p :=
                fun (fe : (R →ₐ[R] CliffordAlgebra (R := R) (M := R) 0) × CliffordAlgebra (R := R) (M := R) 0) ↦
                fe.2 * fe.2 = 0 ∧ ∀ (a : R), Commute fe.2 ((fe.1 : (a : R) → CliffordAlgebra 0) a))
                (Algebra.ofId R (CliffordAlgebra (R := R) (M := R) 0), (ι 0 : (a : R) → CliffordAlgebra 0) 1) ⋯)) :
          (a : R[ε]) → R[ε])
        ε :
      R[ε])
    ((AlgHom.id R R[ε] : (a : R[ε]) → R[ε]) ε : R[ε])

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := CliffordAlgebra (R := R) (M := R) 0)
    ((AlgHom.toLinearMap
            (AlgHom.comp (B := R[ε])
              ((DualNumber.lift :
                  (a :
                      { fe : (R →ₐ[R] CliffordAlgebra 0) × CliffordAlgebra 0 //
                        fe.2 * fe.2 = 0 ∧ ∀ (a : R), Commute fe.2 ((fe.1 : (a : R) → CliffordAlgebra 0) a) }) →
                    R[ε] →ₐ[R] CliffordAlgebra 0)
                (Subtype.mk (p :=
                  fun (fe : (R →ₐ[R] CliffordAlgebra (R := R) (M := R) 0) × CliffordAlgebra (R := R) (M := R) 0) ↦
                  fe.2 * fe.2 = 0 ∧ ∀ (a : R), Commute fe.2 ((fe.1 : (a : R) → CliffordAlgebra 0) a))
                  (Algebra.ofId R (CliffordAlgebra (R := R) (M := R) 0), (ι 0 : (a : R) → CliffordAlgebra 0) 1) ⋯))
              (((CliffordAlgebra.lift.{u_1, u_1, u_1} (R := R) (M := R) 0 (A := R[ε]) :
                    { f : R →ₗ[R] R[ε] //
                        ∀ (m : R),
                          HMul.hMul (α := R[ε]) (β := R[ε]) ((f : (a : R) → R[ε]) m : R[ε])
                              ((f : (a : R) → R[ε]) m : R[ε]) =
                            (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m : R) } ≃
                      (CliffordAlgebra (R := R) (M := R) 0 →ₐ[R] R[ε])) :
                  (a :
                      { f : R →ₗ[R] R[ε] //
                        ∀ (m : R),
                          (f : (a : R) → R[ε]) m * (f : (a : R) → R[ε]) m =
                            (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m) }) →
                    CliffordAlgebra 0 →ₐ[R] R[ε])
                (Subtype.mk (p := fun (f : R →ₗ[R] R[ε]) ↦
                  ∀ (m : R),
                    HMul.hMul (α := R[ε]) (β := R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) ((f : (a : R) → R[ε]) m : R[ε]) =
                      (algebraMap R R[ε] : (a : R) → R[ε]) ((0 : (a : R) → R) m : R))
                  (inrHom R R) ⋯))) ∘ₗ
          ι 0 :
        (a : R) → CliffordAlgebra 0)
      1)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := R) 0)) ∘ₗ ι 0 : (a : R) → CliffordAlgebra 0) 1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ (CliffordAlgebraDualNumber.equiv : (a : CliffordAlgebra 0) → R[ε])
      ((ι 0 : (a : R) → CliffordAlgebra 0) r : CliffordAlgebra (R := R) (M := R) 0) =
    HSMul.hSMul (β := R[ε]) r ε

Tactic:
(lift_ι_apply _ _ r).trans (inr_eq_smul_eps _)

Premises used: CliffordAlgebra.lift_ι_apply, DualNumber.inr_eq_smul_eps, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := CliffordAlgebra (R := R) (M := R) 0)
    ((AlgEquiv.symm CliffordAlgebraDualNumber.equiv : (a : R[ε]) → CliffordAlgebra 0) ε :
      CliffordAlgebra (R := R) (M := R) 0)
    ((ι 0 : (a : R) → CliffordAlgebra 0) 1 : CliffordAlgebra (R := R) (M := R) 0)

Tactic:
DualNumber.lift_apply_eps _

Premises used: DualNumber.lift_apply_eps
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R (CliffordAlgebra Q)) → Submodule R (CliffordAlgebra Q)) (even Q) =
    evenOdd Q 0

Tactic:
rfl

Premises used: iInf, iSup, Set.iInter, setOf, CliffordAlgebra.evenOdd, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
x x_1 x_2 : M
simp :
  Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q) +
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
      ⋯ =
    Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯ +
      Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯
⊢ (fun (m₁ m₂ : M) ↦
        Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
          (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_1) x_2 =
    HAdd.hAdd (α := ↥(even Q))
      ((fun (m₁ m₂ : M) ↦
          Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            (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_2)
      ((fun (m₁ m₂ : M) ↦
          Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            (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_1 x_2)

Tactic:
simp only [map_add, add_mul]

Premises used: add_mul, map_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
x x_1 x_2 : M
⊢ Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q) +
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
      ⋯ =
    Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯ +
      Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
x : R
x_1 x_2 : M
simp :
  Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
      (x •
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
      ⋯ =
    x •
      Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯
⊢ (fun (m₁ m₂ : M) ↦
        Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
          (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_1) x_2 =
    HSMul.hSMul (β := ↥(even Q)) x
      ((fun (m₁ m₂ : M) ↦
          Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            (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_1 x_2)

Tactic:
simp only [map_smul, smul_mul_assoc]

Premises used: smul_mul_assoc, map_smul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
x : R
x_1 x_2 : M
⊢ Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
      (x •
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
      ⋯ =
    x •
      Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
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
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
x x_1 x_2 : M
simp :
  Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q) +
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
      ⋯ =
    Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_1 : CliffordAlgebra Q))
        ⋯ +
      Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x_2 : CliffordAlgebra Q))
        ⋯
⊢ (fun (m₁ m₂ : M) ↦
        Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
          (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_1 + x_2) =
    HAdd.hAdd (α := ↥(even Q))
      ((fun (m₁ m₂ : M) ↦
          Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            (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_1)
      ((fun (m₁ m₂ : M) ↦
          Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            (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_2)

Tactic:
simp only [map_add, mul_add]

Premises used: map_add, mul_add