-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
refine_4 :
  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.1 :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (a.1 * b.1,
          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
⊢ 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.1,
                  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.1,
          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

Tactic:
rw [map_mul, mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), mul_assoc, ←
        mul_assoc z, hb, ← mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc, ha]

Premises used: Algebra.algebraMap, mul_assoc, map_mul, mul_comm, Subtype.val, CyclotomicRing, Prod.snd, DFunLike.coe