-- 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)
refine_1 :
  ∀ (y : CyclotomicField n K)
    (hy : Membership.mem (γ := Set (CyclotomicField n K)) {b : CyclotomicField n K | b ^ n = 1} y),
    ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
      HMul.hMul (β := CyclotomicField n K) y
          ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
              (↑x.2 : CyclotomicRing n A K) :
            CyclotomicField n K) =
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x.1
refine_2 :
  ∀ (k : K),
    ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A 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)
              (↑x.2 : CyclotomicRing n A K) :
            CyclotomicField n K) =
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x.1
refine_3 :
  ∀ (x y : CyclotomicField n K)
    (hx : Membership.mem (γ := Subalgebra K (CyclotomicField n K)) (adjoin K {b : CyclotomicField n K | b ^ n = 1}) x)
    (hy : Membership.mem (γ := Subalgebra K (CyclotomicField n K)) (adjoin K {b : CyclotomicField n K | b ^ n = 1}) y),
    (∃ (x_1 : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
        HMul.hMul (β := CyclotomicField n K) x
            ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) :
                  (a : CyclotomicRing n A K) → CyclotomicField n K)
                (↑x_1.2 : CyclotomicRing n A K) :
              CyclotomicField n K) =
          (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            x_1.1) →
      (∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
          HMul.hMul (β := CyclotomicField n K) y
              ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) :
                    (a : CyclotomicRing n A K) → CyclotomicField n K)
                  (↑x.2 : CyclotomicRing n A K) :
                CyclotomicField n K) =
            (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
              x.1) →
        ∃ (x_1 : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
          HMul.hMul (β := CyclotomicField n K) (x + y)
              ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) :
                    (a : CyclotomicRing n A K) → CyclotomicField n K)
                  (↑x_1.2 : CyclotomicRing n A K) :
                CyclotomicField n K) =
            (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
              x_1.1
refine_4 :
  ∀ (x y : CyclotomicField n K)
    (hx : Membership.mem (γ := Subalgebra K (CyclotomicField n K)) (adjoin K {b : CyclotomicField n K | b ^ n = 1}) x)
    (hy : Membership.mem (γ := Subalgebra K (CyclotomicField n K)) (adjoin K {b : CyclotomicField n K | b ^ n = 1}) y),
    (∃ (x_1 : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
        HMul.hMul (β := CyclotomicField n K) x
            ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) :
                  (a : CyclotomicRing n A K) → CyclotomicField n K)
                (↑x_1.2 : CyclotomicRing n A K) :
              CyclotomicField n K) =
          (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            x_1.1) →
      (∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
          HMul.hMul (β := CyclotomicField n K) y
              ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) :
                    (a : CyclotomicRing n A K) → CyclotomicField n K)
                  (↑x.2 : CyclotomicRing n A K) :
                CyclotomicField n K) =
            (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
              x.1) →
        ∃ (x_1 : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
          HMul.hMul (β := CyclotomicField n K) (x * y)
              ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) :
                    (a : CyclotomicRing n A K) → CyclotomicField n K)
                  (↑x_1.2 : CyclotomicRing n A K) :
                CyclotomicField n K) =
            (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
              x_1.1
⊢ ∃ (x_1 : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) x
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            (↑x_1.2 : CyclotomicRing n A K) :
          CyclotomicField n K) =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x_1.1

Tactic:
refine
      Algebra.adjoin_induction
        (hx := ((IsCyclotomicExtension.iff_singleton n K (CyclotomicField n K)).1
            (CyclotomicField.isCyclotomicExtension n K)).2 x)
        (fun y hy => ?_) (fun k => ?_) ?_ ?_