-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x_1 y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃])
        (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
              (a : S) → ℍ[R,c₁,c₂,c₃])
            s :
          ℍ[R,c₁,c₂,c₃])
        x).re =
    (HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
        (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
              (a : S) → ℍ[R,c₁,c₂,c₃])
            s :
          ℍ[R,c₁,c₂,c₃])).re
imI :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃])
        (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
              (a : S) → ℍ[R,c₁,c₂,c₃])
            s :
          ℍ[R,c₁,c₂,c₃])
        x).imI =
    (HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
        (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
              (a : S) → ℍ[R,c₁,c₂,c₃])
            s :
          ℍ[R,c₁,c₂,c₃])).imI
imJ :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃])
        (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
              (a : S) → ℍ[R,c₁,c₂,c₃])
            s :
          ℍ[R,c₁,c₂,c₃])
        x).imJ =
    (HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
        (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
              (a : S) → ℍ[R,c₁,c₂,c₃])
            s :
          ℍ[R,c₁,c₂,c₃])).imJ
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃])
      (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
      x =
    HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
      (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
              map_zero' := ⋯, map_add' := ⋯ } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
have imK : (HMul.hMul (α := ℍ[R,c₁,c₂,c₃])
      (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
      x).imK =
  (HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
      (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])).imK
Tactic: ext