awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
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₂])
⊢ 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₂])
have imI : 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₂] } =
  imI (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
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₂])
⊢ 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₂])
have imJ : 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₂] } =
  imJ (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
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₂])
⊢ 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₂])
have imK : 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₂] } =
  imK (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ 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₂] } =
    re (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ 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₂] } =
    imI (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
have imI : 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2 = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ 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₂] } =
    imJ (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
have imJ : 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1 = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
v : R × R
⊢ 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₂] } =
    imK (a := c₁) (b := 0) (c := c₂) (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)) : ℍ[R,c₁,c₂])
have imK : HMul.hMul (α := R) 0 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + HMul.hMul (α := R) 0 0 = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (R := R) (M := R × R) (Q 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₂])
have 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₂])
Tactic: simp only [CliffordAlgebra.star_def']
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (R := R) (M := R × R) (Q 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₂)) c)) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) c) : ℍ[R,c₁,c₂])
have algebraMap : ∀ (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: induction c using CliffordAlgebra.induction with
  | algebraMap r => simp
  | ι x => simp
  | mul x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)
algebraMap :
  ∀ (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₂))
              ((Algebra.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₂])
            ((Algebra.algebraMap R (CliffordAlgebra (R := R) (M := R × R) (Q c₁ c₂)) :
                (a : R) → CliffordAlgebra (Q c₁ c₂))
              r)) :
        ℍ[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₂)) c)) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) c) : ℍ[R,c₁,c₂])
have ι : ∀ (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: induction c using CliffordAlgebra.induction with
  | algebraMap r => simp
  | ι x => simp
  | mul x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : 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₂)))
have 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)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
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)
⊢ 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₂)))
have 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)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
⊢ Eq (α := ℍ[R,c₁,c₂] →ₐ[R] ℍ[R,c₁,c₂]) (AlgHom.comp toQuaternion ofQuaternion) (AlgHom.id R ℍ[R,c₁,c₂])
have 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₂])
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
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₂])
⊢ Eq (α := ℍ[R,c₁,c₂] →ₐ[R] ℍ[R,c₁,c₂]) (AlgHom.comp toQuaternion ofQuaternion) (AlgHom.id R ℍ[R,c₁,c₂])
have 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₂])
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
c₁ c₂ : R
q : ℍ[R,c₁,c₂]
⊢ 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₂])
have 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₂])
Tactic: rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
      toQuaternion_ofQuaternion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
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₂])
⊢ 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₂])
have 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₂])
Tactic: rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
      toQuaternion_ofQuaternion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
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₂])
⊢ 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₂])
have 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₂])
Tactic: rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
      toQuaternion_ofQuaternion]