-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommRing R
x y : R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b }
        (star { re := x, im := y : QuadraticAlgebra R a b })).re =
    (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b) +
          HMul.hMul (β := QuadraticAlgebra R a b)
            (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
              ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) b)
              ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b))
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b) -
        HMul.hMul (β := QuadraticAlgebra R a b)
          (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) a : QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b))
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b)).re
⊢ HMul.hMul (α := QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b }
      (star { re := x, im := y : QuadraticAlgebra R a b }) =
    HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b) +
        HMul.hMul (β := QuadraticAlgebra R a b)
          (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b))
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b) -
      HMul.hMul (β := QuadraticAlgebra R a b)
        (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) a : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b))
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b)
have im : (HMul.hMul (α := QuadraticAlgebra R a b) { re := x, im := y : QuadraticAlgebra R a b }
      (star { re := x, im := y : QuadraticAlgebra R a b })).im =
  (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b) +
        HMul.hMul (β := QuadraticAlgebra R a b)
          (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) b)
            ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b))
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b) -
      HMul.hMul (β := QuadraticAlgebra R a b)
        (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) a : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b))
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) y : QuadraticAlgebra R a b)).im
Tactic: ext