Theorem: exists_int_sub_pow_prime_dvd (FltRegular/NumberTheory/Cyclotomic/CyclRat.lean)

State before:
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
⊢ ∃ m, a ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
have : a ∈ Algebra.adjoin ℤ _ := @adjoin_roots {p} ℤ A _ _ _ _ a
State after:
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}

State before:
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}
Tactic:
refine' Algebra.adjoin_induction this _ _ _ _
State after:
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}

State before:
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}
Tactic:
intro x hx
State after:
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 : A
hx : x ∈ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}

State before:
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 : A
hx : x ∈ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rcases hx with ⟨hx_w, hx_m, hx_p⟩
State after:
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_m : hx_w ∈ {p}
hx_p : x ^ ↑hx_w = 1
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}

State before:
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_m : hx_w ∈ {p}
hx_p : x ^ ↑hx_w = 1
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
simp only [Set.mem_singleton_iff] at hx_m
State after:
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 ^ ↑hx_w = 1
hx_m : hx_w = p
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}

State before:
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 ^ ↑hx_w = 1
hx_m : hx_w = p
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rw [hx_m] at hx_p
State after:
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}

State before:
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}
Tactic:
simp only [hx_p]
State after:
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}

State before:
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}
Tactic:
use 1
State after:
case h
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
⊢ 1 - ↑1 ∈ span {↑↑p}

State before:
case h
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
⊢ 1 - ↑1 ∈ span {↑↑p}
Tactic:
simp
State after:
no goals

State before:
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}
Tactic:
intro r
State after:
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}

State before:
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}
Tactic:
use r ^ (p : ℕ)
State after:
case h
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 : ℤ
⊢ (algebraMap ℤ A) r ^ ↑p - ↑(r ^ ↑p) ∈ span {↑↑p}

State before:
case h
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 : ℤ
⊢ (algebraMap ℤ A) r ^ ↑p - ↑(r ^ ↑p) ∈ span {↑↑p}
Tactic:
simp
State after:
no goals

State before:
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}
Tactic:
rintro x y ⟨b, hb⟩ ⟨c, hc⟩
State after:
case refine'_3.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}

State before:
case refine'_3.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
obtain ⟨r, hr⟩ := exists_add_pow_prime_eq hp.out x y
State after:
case refine'_3.intro.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}

State before:
case refine'_3.intro.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rw [hr]
State after:
case refine'_3.intro.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ∃ m, x ^ ↑p + y ^ ↑p + ↑↑p * r - ↑m ∈ span {↑↑p}

State before:
case refine'_3.intro.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ∃ m, x ^ ↑p + y ^ ↑p + ↑↑p * r - ↑m ∈ span {↑↑p}
Tactic:
use c + b
State after:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + ↑↑p * r - ↑(c + b) ∈ span {↑↑p}

State before:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + ↑↑p * r - ↑(c + b) ∈ span {↑↑p}
Tactic:
push_cast
State after:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + ↑↑p * r - (↑c + ↑b) ∈ span {↑↑p}

State before:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + ↑↑p * r - (↑c + ↑b) ∈ span {↑↑p}
Tactic:
rw [sub_add_eq_sub_sub, sub_eq_add_neg, sub_eq_add_neg, add_comm _ (↑↑p * r), add_assoc,
  add_assoc]
State after:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r + (x ^ ↑p + y ^ ↑p + (-↑c + -↑b)) ∈ span {↑↑p}

State before:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r + (x ^ ↑p + y ^ ↑p + (-↑c + -↑b)) ∈ span {↑↑p}
Tactic:
apply Ideal.add_mem _ _
State after:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + (-↑c + -↑b) ∈ span {↑↑p}

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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r ∈ span {↑↑p}

State before:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + (-↑c + -↑b) ∈ span {↑↑p}
Tactic:
convert Ideal.add_mem _ hb hc using 1
State after:
case h.e'_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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + (-↑c + -↑b) = x ^ ↑p - ↑b + (y ^ ↑p - ↑c)

State before:
case h.e'_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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + (-↑c + -↑b) = x ^ ↑p - ↑b + (y ^ ↑p - ↑c)
Tactic:
ring
State after:
no goals

State before:
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r ∈ span {↑↑p}
Tactic:
rw [mem_span_singleton]
State after:
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p ∣ ↑↑p * r

State before:
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p ∣ ↑↑p * r
Tactic:
exact dvd_mul_right _ _
State after:
no goals

State before:
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}
Tactic:
rintro x y ⟨b, hb⟩ ⟨c, hc⟩
State after:
case refine'_4.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, (x * y) ^ ↑p - ↑m ∈ span {↑↑p}

State before:
case refine'_4.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, (x * y) ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rw [mul_pow]
State after:
case refine'_4.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, x ^ ↑p * y ^ ↑p - ↑m ∈ span {↑↑p}

State before:
case refine'_4.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 y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, x ^ ↑p * y ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
use b * c
State after:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}

State before:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Tactic:
have := Ideal.mul_mem_left _ (x ^ (p : ℕ)) hc
State after:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : x ^ ↑p * (y ^ ↑p - ↑c) ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}

State before:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : x ^ ↑p * (y ^ ↑p - ↑c) ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Tactic:
rw [mul_sub] at this
State after:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : x ^ ↑p * y ^ ↑p - x ^ ↑p * ↑c ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}

State before:
case h
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
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : x ^ ↑p * y ^ ↑p - x ^ ↑p * ↑c ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub] at this hb ⊢
State after:
case h
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
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑(b * c) = 0

State before:
case h
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
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑(b * c) = 0
Tactic:
convert this using 2
State after:
case h.e'_2.h.e'_6
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
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑(b * c) = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c)

State before:
case h.e'_2.h.e'_6
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
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑(b * c) = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c)
Tactic:
rw [Int.cast_mul, _root_.map_mul, _root_.map_mul]
State after:
case h.e'_2.h.e'_6
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
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b * (Ideal.Quotient.mk (span {↑↑p})) ↑c =
    (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) * (Ideal.Quotient.mk (span {↑↑p})) ↑c

State before:
case h.e'_2.h.e'_6
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
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b * (Ideal.Quotient.mk (span {↑↑p})) ↑c =
    (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) * (Ideal.Quotient.mk (span {↑↑p})) ↑c
Tactic:
congr 1
State after:
case h.e'_2.h.e'_6.e_a
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
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p)

State before:
case h.e'_2.h.e'_6.e_a
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
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p)
Tactic:
exact (sub_eq_zero.mp hb).symm
State after:
no goals