Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
⊢ ∃ x_1,
    x * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.2 =
      (algebraMap (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 => ?_) ?_ ?_

Goal state after:
case refine_1
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ ∃ x,
    y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.2 =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.1

case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
k : K
⊢ ∃ x,
    (algebraMap K (CyclotomicField n K)) k * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.2 =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.1

case refine_3
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
⊢ ∀ (x y : CyclotomicField n K),
    x ∈ adjoin K {b | b ^ n = 1} →
      y ∈ adjoin K {b | b ^ n = 1} →
        (∃ x_1,
            x * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.2 =
              (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.1) →
          (∃ x,
              y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.2 =
                (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.1) →
            ∃ x_1,
              (x + y) * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.2 =
                (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.1

case refine_4
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
⊢ ∀ (x y : CyclotomicField n K),
    x ∈ adjoin K {b | b ^ n = 1} →
      y ∈ adjoin K {b | b ^ n = 1} →
        (∃ x_1,
            x * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.2 =
              (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.1) →
          (∃ x,
              y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.2 =
                (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.1) →
            ∃ x_1,
              x * y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.2 =
                (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.1