Theorem: exists_solution' (FltRegular/CaseII/InductionStep.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ∃ x' y' z' ε₃, ¬π ∣ y' ∧ ¬π ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
obtain ⟨x', y', z', ε₁, ε₂, ε₃, hx', hy', hz', e'⟩ := exists_solution hp hreg hζ e hy hz
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
⊢ ∃ x' y' z' ε₃, ¬π ∣ y' ∧ ¬π ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
⊢ ∃ x' y' z' ε₃, ¬π ∣ y' ∧ ¬π ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
obtain ⟨ε', hε'⟩ : ∃ ε', ε₁ / ε₂ = ε' ^ (p : ℕ) := by
  apply eq_pow_prime_of_unit_of_congruent hp hreg
  have : p - 1 ≤ m * p := (Nat.sub_le _ _).trans
    ((le_of_eq (one_mul _).symm).trans (Nat.mul_le_mul_right p (one_le_m hp hζ e hy hz)))
  obtain ⟨u, hu⟩ := (associated_zeta_sub_one_pow_prime hζ).symm
  rw [mul_pow, ← pow_mul, mul_comm (ε₃ : 𝓞 K), mul_assoc, ← Nat.sub_add_cancel this,
    add_comm _ (p - 1 : ℕ), pow_add, mul_assoc] at e'
  apply_fun Ideal.Quotient.mk (Ideal.span <| singleton (p : 𝓞 K)) at e'
  rw [map_mul, (Ideal.Quotient.eq_zero_iff_dvd _ _).mpr
    (associated_zeta_sub_one_pow_prime hζ).symm.dvd, zero_mul, Ideal.Quotient.eq_zero_iff_dvd] at e'
  obtain ⟨a, ha⟩ := exists_solution'_aux hp hζ hx' e'
  obtain ⟨b, hb⟩ := exists_dvd_pow_sub_Int_pow hp a
  have := dvd_add ha hb
  rw [sub_add_sub_cancel, ← Int.cast_pow] at this
  exact ⟨b ^ (p : ℕ), this⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
ε' : (𝓞 K)ˣ
hε' : ε₁ / ε₂ = ε' ^ ↑p
⊢ ∃ x' y' z' ε₃, ¬π ∣ y' ∧ ¬π ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
ε' : (𝓞 K)ˣ
hε' : ε₁ / ε₂ = ε' ^ ↑p
⊢ ∃ x' y' z' ε₃, ¬π ∣ y' ∧ ¬π ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
refine ⟨ε' * x', y', z', ε₃ / ε₂, hy', hz', ?_⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
ε' : (𝓞 K)ˣ
hε' : ε₁ / ε₂ = ε' ^ ↑p
⊢ (↑ε' * x') ^ ↑p + y' ^ ↑p = ↑(ε₃ / ε₂) * (π ^ m * z') ^ ↑p

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
ε' : (𝓞 K)ˣ
hε' : ε₁ / ε₂ = ε' ^ ↑p
⊢ (↑ε' * x') ^ ↑p + y' ^ ↑p = ↑(ε₃ / ε₂) * (π ^ m * z') ^ ↑p
Tactic:
rwa [mul_pow, ← Units.val_pow_eq_pow_val, ← hε', ← mul_right_inj' ε₂.isUnit.ne_zero,
  mul_add, ← mul_assoc, ← Units.val_mul, mul_div_cancel,
  ← mul_assoc, ← Units.val_mul, mul_div_cancel]
State after:
no goals

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
⊢ ∃ ε', ε₁ / ε₂ = ε' ^ ↑p
Tactic:
apply eq_pow_prime_of_unit_of_congruent hp hreg
State after:
case hcong
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
have : p - 1 ≤ m * p := (Nat.sub_le _ _).trans
  ((le_of_eq (one_mul _).symm).trans (Nat.mul_le_mul_right p (one_le_m hp hζ e hy hz)))
State after:
case hcong
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
obtain ⟨u, hu⟩ := (associated_zeta_sub_one_pow_prime hζ).symm
State after:
case hcong.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
rw [mul_pow, ← pow_mul, mul_comm (ε₃ : 𝓞 K), mul_assoc, ← Nat.sub_add_cancel this,
  add_comm _ (p - 1 : ℕ), pow_add, mul_assoc] at e'
State after:
case hcong.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃))
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃))
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
apply_fun Ideal.Quotient.mk (Ideal.span <| singleton (p : 𝓞 K)) at e'
State after:
case hcong.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' :
  (Ideal.Quotient.mk (Ideal.span {↑↑p})) (↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p) =
    (Ideal.Quotient.mk (Ideal.span {↑↑p})) (π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃)))
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' :
  (Ideal.Quotient.mk (Ideal.span {↑↑p})) (↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p) =
    (Ideal.Quotient.mk (Ideal.span {↑↑p})) (π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃)))
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
rw [map_mul, (Ideal.Quotient.eq_zero_iff_dvd _ _).mpr
  (associated_zeta_sub_one_pow_prime hζ).symm.dvd, zero_mul, Ideal.Quotient.eq_zero_iff_dvd] at e'
State after:
case hcong.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
obtain ⟨a, ha⟩ := exists_solution'_aux hp hζ hx' e'
State after:
case hcong.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
obtain ⟨b, hb⟩ := exists_dvd_pow_sub_Int_pow hp a
State after:
case hcong.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
have := dvd_add ha hb
State after:
case hcong.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this✝ : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
this : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p + (a ^ ↑p - ↑b ^ ↑p)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this✝ : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
this : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p + (a ^ ↑p - ↑b ^ ↑p)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
rw [sub_add_sub_cancel, ← Int.cast_pow] at this
State after:
case hcong.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this✝ : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
this : ↑↑p ∣ ↑(ε₁ / ε₂) - ↑(b ^ ↑p)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n

State before:
case hcong.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this✝ : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
this : ↑↑p ∣ ↑(ε₁ / ε₂) - ↑(b ^ ↑p)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
exact ⟨b ^ (p : ℕ), this⟩
State after:
no goals