refine' Algebra.adjoin_induction this _ _ _ _
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∃ m, a ^ ↑p - ↑m ∈ span {↑↑p}
case refine'_1
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∀ x ∈ {b | ∃ n ∈ {p}, b ^ ↑n = 1}, ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}

case refine'_2
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∀ (r : ℤ), ∃ m, (algebraMap ℤ A) r ^ ↑p - ↑m ∈ span {↑↑p}

case refine'_3
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∀ (x y : A), (∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}) → (∃ m, y ^ ↑p - ↑m ∈ span {↑↑p}) → ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}

case refine'_4
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∀ (x y : A), (∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}) → (∃ m, y ^ ↑p - ↑m ∈ span {↑↑p}) → ∃ m, (x * y) ^ ↑p - ↑m ∈ span {↑↑p}