simp only [hx_p]
case refine'_1.intro.intro
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 : A
hx_w : ℕ+
hx_p : x ^ ↑p = 1
hx_m : hx_w = p
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
case refine'_1.intro.intro
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 : A
hx_w : ℕ+
hx_p : x ^ ↑p = 1
hx_m : hx_w = p
⊢ ∃ m, 1 - ↑m ∈ span {↑↑p}