-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
this : NeZero.{w} (R := K) (↑n : K)
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  HMul.hMul (β := CyclotomicField n K) y
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑a.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  HMul.hMul (β := CyclotomicField n K) z
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑b.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) b.1
⊢ HMul.hMul (β := CyclotomicField n K) (y + z)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑(a.1 * (↑b.2 : CyclotomicRing n A K) + b.1 * (↑a.2 : CyclotomicRing n A K),
                  Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
                    Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
                    ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) ⋯).2 :
            CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (a.1 * (↑b.2 : CyclotomicRing n A K) + b.1 * (↑a.2 : CyclotomicRing n A K),
          Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
            Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
            ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) ⋯).1
have refine_3 : HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          a.1 :
        CyclotomicField n K)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑b.2 : CyclotomicRing n A K) :
        CyclotomicField n K) +
    HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          b.1 :
        CyclotomicField n K)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑a.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
  (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
    (a.1 * (↑b.2 : CyclotomicRing n A K) + b.1 * (↑a.2 : CyclotomicRing n A K),
        Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
          Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
          ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) sorry).1
Tactic: rw [map_mul, add_mul, ← mul_assoc, ha,
        mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc, hb]