-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem ofQuaternion_comp_toQuaternion :
    ofQuaternion.comp toQuaternion = AlgHom.id R (CliffordAlgebra (Q c₁ c₂))

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂) = ι (Q c₁ c₂)

Tactic:
ext

Result:
case a.hl.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R) 1 =
    (ι (Q c₁ c₂) ∘ₗ LinearMap.inl R R R) 1

case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1 =
    (ι (Q c₁ c₂) ∘ₗ LinearMap.inr R R R) 1

Proof state:
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) 0 + 0 • (ι (Q c₁ c₂)) (1, 0) + 1 • (ι (Q c₁ c₂)) (0, 1) +
      0 • ((ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (0, 1)) =
    (ι (Q c₁ c₂)) (0, 1)

Tactic:
simp only [toQuaternion_ι, zero_smul, one_smul, zero_add, add_zero, RingHom.map_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ofQuaternion.comp toQuaternion = AlgHom.id R (CliffordAlgebra (Q c₁ c₂))

Tactic:
ext : 1

Result:
case a
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ofQuaternion.comp toQuaternion).toLinearMap ∘ₗ ι (Q c₁ c₂) =
    (AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)

Proof state:
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1 =
    (ι (Q c₁ c₂) ∘ₗ LinearMap.inr R R R) 1

Tactic:
dsimp

Result:
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ofQuaternion (toQuaternion ((ι (Q c₁ c₂)) (0, 1))) = (ι (Q c₁ c₂)) (0, 1)

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ofQuaternion.comp toQuaternion).toLinearMap ∘ₗ ι (Q c₁ c₂) =
    (AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)

Tactic:
dsimp

Result:
case a
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂) = ι (Q c₁ c₂)

Proof state:
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ofQuaternion (toQuaternion ((ι (Q c₁ c₂)) (0, 1))) = (ι (Q c₁ c₂)) (0, 1)

Tactic:
rw [toQuaternion_ι]

Result:
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ofQuaternion { re := 0, imI := (0, 1).1, imJ := (0, 1).2, imK := 0 } = (ι (Q c₁ c₂)) (0, 1)

Proof state:
case a.hl.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R) 1 =
    (ι (Q c₁ c₂) ∘ₗ LinearMap.inl R R R) 1

case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.toLinearMap ∘ₗ toQuaternion.toLinearMap) ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1 =
    (ι (Q c₁ c₂) ∘ₗ LinearMap.inr R R R) 1

Tactic:
all_goals
  dsimp
  rw [toQuaternion_ι]
  dsimp
  simp only [toQuaternion_ι, zero_smul, one_smul, zero_add, add_zero, RingHom.map_zero]

Result:
no goals

Proof state:
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ofQuaternion { re := 0, imI := (0, 1).1, imJ := (0, 1).2, imK := 0 } = (ι (Q c₁ c₂)) (0, 1)

Tactic:
dsimp

Result:
case a.hr.h
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) 0 + 0 • (ι (Q c₁ c₂)) (1, 0) + 1 • (ι (Q c₁ c₂)) (0, 1) +
      0 • ((ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (0, 1)) =
    (ι (Q c₁ c₂)) (0, 1)