-- 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₂])
ι :
  ∀ (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₂))
              ((CliffordAlgebra.ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q c₁ c₂)) x))) :
        ℍ[R,c₁,c₂])
      (star
          ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂])
            ((CliffordAlgebra.ι (Q c₁ c₂) : (a : R × R) → CliffordAlgebra (Q 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₂)) c)) :
      ℍ[R,c₁,c₂])
    (star ((toQuaternion : (a : CliffordAlgebra (Q c₁ c₂)) → ℍ[R,c₁,c₂]) c) : ℍ[R,c₁,c₂])
have mul : ∀ (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: 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