awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
      (c₁ * HMul.hMul (α := R) (1, 0).1 (1, 0).1 + c₂ * HMul.hMul (α := R) (1, 0).2 (1, 0).2) =
    HAdd.hAdd (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂)) c₁ :
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      (HSMul.hSMul (α := R) (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) 0
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
rw :
  Eq (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
        (c₁ * HMul.hMul (α := R) (0, 1).1 (0, 1).1 + c₂ * HMul.hMul (α := R) (0, 1).2 (0, 1).2) :
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂)) c₂ :
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) (β :=
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) :
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) =
    HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) c₂ 1

Tactic:
rw [ι_sq_scalar, Q_apply, ← Algebra.algebraMap_eq_smul_one]

Premises used: CliffordAlgebra.ι_sq_scalar, Algebra.algebraMap_eq_smul_one, CliffordAlgebraQuaternion.Q_apply
-- 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₂))
    ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
        (c₁ * HMul.hMul (α := R) (0, 1).1 (0, 1).1 + c₂ * HMul.hMul (α := R) (0, 1).2 (0, 1).2) :
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂)) c₂ :
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
rw :
  Eq (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
        (HSub.hSub (β := R)
          (HSub.hSub (α := R) (β := R) ((Q c₁ c₂ : (a : R × R) → R) (HAdd.hAdd (α := R × R) (0, 1) (1, 0)) : R)
            ((Q c₁ c₂ : (a : R × R) → R) (0, 1) : R))
          ((Q c₁ c₂ : (a : R × R) → R) (1, 0) : R)) :
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    (0 : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
⊢ HMul.hMul (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) (β :=
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
      ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) =
    HSMul.hSMul (α := R) (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) 0
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) :
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) -
      HMul.hMul (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) (β :=
        CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) :
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))

Tactic:
rw [zero_smul, zero_sub, eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar]

Premises used: CliffordAlgebra.ι_mul_ι_add_swap, QuadraticMap.polar, zero_smul, eq_neg_iff_add_eq_zero, zero_sub
-- 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₂))
    ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
        (HSub.hSub (β := R)
          (HSub.hSub (α := R) (β := R) ((Q c₁ c₂ : (a : R × R) → R) (HAdd.hAdd (α := R × R) (0, 1) (1, 0)) : R)
            ((Q c₁ c₂ : (a : R × R) → R) (0, 1) : R))
          ((Q c₁ c₂ : (a : R × R) → R) (1, 0) : R)) :
      CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    (0 : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v₁ v₂ : R × R
⊢ { re := 0, imI := (v₁ + v₂).1, imJ := (v₁ + v₂).2, imK := 0 } =
    HAdd.hAdd (α := ℍ[R,c₁,c₂]) { re := 0, imI := v₁.1, imJ := v₁.2, imK := 0 : ℍ[R,c₁,c₂] }
      { re := 0, imI := v₂.1, imJ := v₂.2, imK := 0 : ℍ[R,c₁,c₂] }

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ r : R
v : R × R
dsimp :
  Eq (α := ℍ[R,c₁,c₂]) { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 }
    { re := r * 0, imI := r * v.1, imJ := r * v.2, imK := r * 0 }
⊢ { re := 0, imI := (r • v).1, imJ := (r • v).2, imK := 0 } =
    HSMul.hSMul (α := R) (β := ℍ[R,c₁,c₂]) ((RingHom.id R : (a : R) → R) r : R)
      { re := 0, imI := v.1, imJ := v.2, imK := 0 : ℍ[R,c₁,c₂] }

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ r : R
v : R × R
rw rw₁ :
  Eq (α := ℍ[R,c₁,c₂]) { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 }
    { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 }
⊢ Eq (α := ℍ[R,c₁,c₂]) { re := 0, imI := r * v.1, imJ := r * v.2, imK := 0 }
    { re := r * 0, imI := r * v.1, imJ := r * v.2, imK := r * 0 }

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
dsimp :
  Eq (α := ℍ[R,c₁,c₂])
    { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
      imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
      imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
      imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 }
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
⊢ HMul.hMul (α := ℍ[R,c₁,c₂]) (β := ℍ[R,c₁,c₂])
      (({ toFun := fun (v : R × R) ↦ { re := 0, imI := v.1, imJ := v.2, imK := 0 : ℍ[R,c₁,c₂] }, map_add' := ⋯,
              map_smul' := ⋯ : R × R →ₗ[R] ℍ[R,c₁,c₂] } :
            (a : R × R) → ℍ[R,c₁,c₂])
          v :
        ℍ[R,c₁,c₂])
      (({ toFun := fun (v : R × R) ↦ { re := 0, imI := v.1, imJ := v.2, imK := 0 : ℍ[R,c₁,c₂] }, map_add' := ⋯,
              map_smul' := ⋯ : R × R →ₗ[R] ℍ[R,c₁,c₂] } :
            (a : R × R) → ℍ[R,c₁,c₂])
          v :
        ℍ[R,c₁,c₂]) =
    (algebraMap R ℍ[R,c₁,c₂] : (a : R) → ℍ[R,c₁,c₂]) ((Q c₁ c₂ : (a : R × R) → R) v)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
re :
  QuaternionAlgebra.re (a := c₁) (b := 0) (c := c₂)
      { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
    QuaternionAlgebra.re (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
imI :
  QuaternionAlgebra.imI (a := c₁) (b := 0) (c := c₂)
      { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
    QuaternionAlgebra.imI (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
imJ :
  QuaternionAlgebra.imJ (a := c₁) (b := 0) (c := c₂)
      { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
    QuaternionAlgebra.imJ (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
imK :
  QuaternionAlgebra.imK (a := c₁) (b := 0) (c := c₂)
      { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
    QuaternionAlgebra.imK (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
⊢ Eq (α := ℍ[R,c₁,c₂])
    { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
      imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
      imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
      imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 }
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
re :
  HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0 =
    c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)
⊢ QuaternionAlgebra.re (a := c₁) (b := 0) (c := c₂)
      { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
    QuaternionAlgebra.re (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0 =
    c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
imI : 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2 = 0
⊢ QuaternionAlgebra.imI (a := c₁) (b := 0) (c := c₂)
      { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
    QuaternionAlgebra.imI (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2 = 0

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
imJ : 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1 = 0
⊢ QuaternionAlgebra.imJ (a := c₁) (b := 0) (c := c₂)
      { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
    QuaternionAlgebra.imJ (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1 = 0

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
imK : HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 = 0
⊢ QuaternionAlgebra.imK (a := c₁) (b := 0) (c := c₂)
      { re := HMul.hMul (α := R) 0 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 : ℍ[R,c₁,c₂] } =
    QuaternionAlgebra.imK (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 = 0

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) v) :
      ℍ[R,c₁,c₂])
    ({ re := 0, imI := v.1, imJ := v.2, imK := 0 } : ℍ[R,c₁,c₂])

Tactic:
CliffordAlgebra.lift_ι_apply _ _ v

Premises used: CliffordAlgebra.lift_ι_apply
-- 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₂)
simp :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂)) c)) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) c) : ℍ[R,c₁,c₂])
⊢ Eq (α := ℍ[R,c₁,c₂]) ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) (star c) : ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) c) : ℍ[R,c₁,c₂])

Tactic:
simp only [CliffordAlgebra.star_def']

Premises used: CliffordAlgebra.star_def'
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ r : R
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
            ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂))
              r))) :
      ℍ[R,c₁,c₂])
    (star
        ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
          ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂)) r)) :
      ℍ[R,c₁,c₂])

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
x : R × R
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
            ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) x))) :
      ℍ[R,c₁,c₂])
    (star
        ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
          ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) x)) :
      ℍ[R,c₁,c₂])

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
x₁ x₂ : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)
hx₁ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂)) x₁)) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) x₁) : ℍ[R,c₁,c₂])
hx₂ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂)) x₂)) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) x₂) : ℍ[R,c₁,c₂])
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂)) (x₁ * x₂))) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) (x₁ * x₂)) : ℍ[R,c₁,c₂])

Tactic:
simp [hx₁, hx₂]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
x₁ x₂ : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)
hx₁ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂)) x₁)) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) x₁) : ℍ[R,c₁,c₂])
hx₂ :
  Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂)) x₂)) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) x₂) : ℍ[R,c₁,c₂])
⊢ Eq (α := ℍ[R,c₁,c₂])
    ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
        ((involute : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂))
          ((reverse : (a : CliffordAlgebra (Q c₁ c₂)) → CliffordAlgebra (Q c₁ c₂)) (x₁ + x₂))) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) (x₁ + x₂)) : ℍ[R,c₁,c₂])

Tactic:
simp [hx₁, hx₂]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ a₁ a₂ a₃ a₄ : R
⊢ (ofQuaternion : (a : ℍ[R,c₁,c₂]) → CliffordAlgebra (Q c₁ c₂)) { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } =
    HAdd.hAdd (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
          ((algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) : (a : R) → CliffordAlgebra (Q c₁ c₂)) a₁ :
            CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
          (HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) a₂
            ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
              CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))) +
        HSMul.hSMul (β := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) a₃
          ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) :
            CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) +
      a₄ •
        HMul.hMul (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) (β :=
          CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
          ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (1, 0) :
            CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
          ((ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) (0, 1) :
            CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))

Tactic:
rfl

Premises used: QuaternionAlgebra.Basis.lift, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
a :
  Eq (α := R →ₗ[R] CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((AlgHom.toLinearMap (AlgHom.comp ofQuaternion toQuaternion) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))) ∘ₗ ι (Q c₁ c₂)) ∘ₗ
      LinearMap.inl R R R)
a₁ :
  Eq (α := R →ₗ[R] CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((AlgHom.toLinearMap (AlgHom.comp ofQuaternion toQuaternion) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))) ∘ₗ ι (Q c₁ c₂)) ∘ₗ
      LinearMap.inr R R R)
⊢ Eq (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂) →ₐ[R] CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    (AlgHom.comp ofQuaternion toQuaternion) (AlgHom.id R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)))

Tactic:
ext : 2
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
a :
  Eq (α := CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    (((AlgHom.toLinearMap (AlgHom.comp ofQuaternion toQuaternion) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl 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.inl R R R :
        (a : R) → CliffordAlgebra (Q c₁ c₂))
      1)
⊢ Eq (α := R →ₗ[R] CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((AlgHom.toLinearMap (AlgHom.comp ofQuaternion toQuaternion) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))) ∘ₗ ι (Q c₁ c₂)) ∘ₗ
      LinearMap.inl R R R)

Tactic:
ext
-- 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.inl 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.inl 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
a :
  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)
⊢ Eq (α := R →ₗ[R] CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))
    ((AlgHom.toLinearMap (AlgHom.comp ofQuaternion toQuaternion) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂))) ∘ₗ ι (Q c₁ c₂)) ∘ₗ
      LinearMap.inr R R R)

Tactic:
ext