-- 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_1 : NeZero.{w} (R := K) (↑n : K)
k : K
this_2 :
  ∀ (z : K),
    ∃ (x : A × ↥(nonZeroDivisors A : Submonoid A)),
      HMul.hMul (β := K) z ((algebraMap A K : (a : A) → K) (↑x.2 : A) : K) = (algebraMap A K : (a : A) → K) x.1
z : A
w : ↥(nonZeroDivisors A : Submonoid A)
hw : HMul.hMul (β := K) k ((algebraMap A K : (a : A) → K) (↑(z, w).2 : A) : K) = (algebraMap A K : (a : A) → K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := ⋯
refine_2 :
  HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
      ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
      ((algebraMap A (CyclotomicField n K) : (a : A) → CyclotomicField n K) (↑w : A) : CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      ((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) z,
          Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
            Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
            ((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) (↑w : A)) ⋯).1
refine_2₁ :
  HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
      ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
      ((algebraMap A (CyclotomicField n K) : (a : A) → CyclotomicField n K) (↑w : A) : CyclotomicField n K) =
    (algebraMap A (CyclotomicField n K) : (a : A) → CyclotomicField n K) z
refine_2₂ :
  HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
      ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
      ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) ((algebraMap A K : (a : A) → K) (↑w : A)) :
        CyclotomicField n K) =
    (algebraMap A (CyclotomicField n K) : (a : A) → CyclotomicField n K) z
refine_2₃ :
  Eq (α := CyclotomicField n K)
    ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K)
        (HMul.hMul (β := K) k ((algebraMap A K : (a : A) → K) (↑w : A) : K)) :
      CyclotomicField n K)
    ((algebraMap A (CyclotomicField n K) : (a : A) → CyclotomicField n K) z : CyclotomicField n K)
refine_2₄ :
  Eq (α := CyclotomicField n K)
    ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) ((algebraMap A K : (a : A) → K) (z, w).1) :
      CyclotomicField n K)
    ((algebraMap A (CyclotomicField n K) : (a : A) → CyclotomicField n K) z : CyclotomicField n K)
⊢ HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
      ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) z,
                  Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
                    Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
                    ((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) (↑w : 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)
      ((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) z,
          Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
            Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
            ((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) (↑w : A)) ⋯).1
have refine_2₅ : Eq.{w + 1} (α := CyclotomicField n K)
  ((algebraMap A (CyclotomicField n K) : (a : A) → CyclotomicField n K) (z, w).1 : CyclotomicField n K)
  ((algebraMap A (CyclotomicField n K) : (a : A) → CyclotomicField n K) z : CyclotomicField n K)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
        @IsScalarTower.algebraMap_apply A K _ _ _ _ _ (_root_.CyclotomicField.algebra n K) _ _ w,
        ← map_mul, hw, ← IsScalarTower.algebraMap_apply]