-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
rw :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
            {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
rw₁ :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
          prod {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])})) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
rw₂ :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
          HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X]))) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
⊢ HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) ::ₘ
          HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
            {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
have rw₃ : HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
    (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X]))) =
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
    (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X]))
Tactic: rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]