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' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
letI : Fact (Nat.Prime p) := hpri
State after:
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) }
this : Fact (↑p).Prime := hpri
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

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) }
this : Fact (↑p).Prime := hpri
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
let η₁ : nthRootsFinset p (𝓞 K) := ⟨η₀ * hζ.unit', mul_mem_nthRootsFinset
  (η₀ : _).prop (hζ.unit'_coe.mem_nthRootsFinset hpri.out.pos)⟩
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
let η₂ : nthRootsFinset p (𝓞 K) := ⟨η₀ * hζ.unit' * hζ.unit', mul_mem_nthRootsFinset
  η₁.prop (hζ.unit'_coe.mem_nthRootsFinset hpri.out.pos)⟩
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
have hη₁ : η₁ ≠ η₀ := by
  rw [← Subtype.coe_injective.ne_iff]
  show (η₀ * hζ.unit' : 𝓞 K) ≠ η₀
  rw [Ne, mul_right_eq_self₀, not_or]
  exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
    ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
have hη₂ : η₂ ≠ η₀ := by
  rw [← Subtype.coe_injective.ne_iff]
  show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀
  rw [Ne, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or]
  exact ⟨hζ.unit'_coe.pow_ne_one_of_pos_of_lt zero_lt_two
    (hpri.out.two_le.lt_or_eq.resolve_right (PNat.coe_injective.ne hp.symm)),
    ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
have hη : η₂ ≠ η₁ := by
  rw [← Subtype.coe_injective.ne_iff]
  show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀ * hζ.unit'
  rw [Ne, mul_right_eq_self₀, not_or]
  exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
    mul_ne_zero (ne_zero_of_mem_nthRootsFinset (η₀ : _).prop)
    (hζ.unit'_coe.ne_zero hpri.out.ne_zero)⟩
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
obtain ⟨u₁, hu₁⟩ := hζ.unit'_coe.associated_sub_one hpri.out η₂.prop (η₀ : _).prop
  (Subtype.coe_injective.ne_iff.mpr hη₂)
State after:
case 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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

State before:
case 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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
obtain ⟨u₂, hu₂⟩ := hζ.unit'_coe.associated_sub_one hpri.out (η₀ : _).prop η₁.prop
  (Subtype.coe_injective.ne_iff.mpr hη₁.symm)
State after:
case 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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

State before:
case 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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
obtain ⟨u₃, hu₃⟩ := hζ.unit'_coe.associated_sub_one hpri.out η₂.prop (η₁ : _).prop
  (Subtype.coe_injective.ne_iff.mpr hη)
State after:
case 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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

State before:
case 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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
have := stuff hp hreg hζ e hy hz η₁ hη₁ η₂ hη₂
State after:
case 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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  (↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + (↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    (↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

State before:
case 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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  (↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + (↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    (↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
rw [← hu₁, ← hu₂, ← hu₃, mul_assoc _ (u₁ : 𝓞 K), mul_assoc _ (u₂ : 𝓞 K), mul_assoc _ (u₃ : 𝓞 K),
  mul_assoc (π), mul_assoc (π), ← mul_add,
  mul_right_inj' (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt), ← Units.val_mul,
  ← Units.val_mul] at this
State after:
case 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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p

State before:
case 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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
refine ⟨_, _, _, _, _, _, ?_, ?_, ?_, this⟩
State after:
case intro.intro.intro.refine_1
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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ α η₁ hη₁ * β η₂ hη₂

case intro.intro.intro.refine_2
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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ α η₂ hη₂ * β η₁ hη₁

case intro.intro.intro.refine_3
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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ β η₁ hη₁ * β η₂ hη₂

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ η₁ ≠ η₀
Tactic:
rw [← Subtype.coe_injective.ne_iff]
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ ↑η₁ ≠ ↑η₀

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ ↑η₁ ≠ ↑η₀
Tactic:
show (η₀ * hζ.unit' : 𝓞 K) ≠ η₀
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ ↑η₀ * ↑hζ.unit' ≠ ↑η₀

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ ↑η₀ * ↑hζ.unit' ≠ ↑η₀
Tactic:
rw [Ne, mul_right_eq_self₀, not_or]
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ ¬↑hζ.unit' = 1 ∧ ¬↑η₀ = 0

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
⊢ ¬↑hζ.unit' = 1 ∧ ¬↑η₀ = 0
Tactic:
exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
  ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ η₂ ≠ η₀
Tactic:
rw [← Subtype.coe_injective.ne_iff]
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ ↑η₂ ≠ ↑η₀

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ ↑η₂ ≠ ↑η₀
Tactic:
show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ ↑η₀ * ↑hζ.unit' * ↑hζ.unit' ≠ ↑η₀

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ ↑η₀ * ↑hζ.unit' * ↑hζ.unit' ≠ ↑η₀
Tactic:
rw [Ne, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or]
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ ¬↑hζ.unit' ^ 2 = 1 ∧ ¬↑η₀ = 0

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ ¬↑hζ.unit' ^ 2 = 1 ∧ ¬↑η₀ = 0
Tactic:
exact ⟨hζ.unit'_coe.pow_ne_one_of_pos_of_lt zero_lt_two
  (hpri.out.two_le.lt_or_eq.resolve_right (PNat.coe_injective.ne hp.symm)),
  ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ η₂ ≠ η₁
Tactic:
rw [← Subtype.coe_injective.ne_iff]
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ ↑η₂ ≠ ↑η₁

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ ↑η₂ ≠ ↑η₁
Tactic:
show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀ * hζ.unit'
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ ↑η₀ * ↑hζ.unit' * ↑hζ.unit' ≠ ↑η₀ * ↑hζ.unit'

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ ↑η₀ * ↑hζ.unit' * ↑hζ.unit' ≠ ↑η₀ * ↑hζ.unit'
Tactic:
rw [Ne, mul_right_eq_self₀, not_or]
State after:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ ¬↑hζ.unit' = 1 ∧ ¬↑η₀ * ↑hζ.unit' = 0

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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ ¬↑hζ.unit' = 1 ∧ ¬↑η₀ * ↑hζ.unit' = 0
Tactic:
exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
  mul_ne_zero (ne_zero_of_mem_nthRootsFinset (η₀ : _).prop)
  (hζ.unit'_coe.ne_zero hpri.out.ne_zero)⟩
State after:
no goals

State before:
case intro.intro.intro.refine_1
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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ α η₁ hη₁ * β η₂ hη₂
Tactic:
exact hζ.zeta_sub_one_prime'.not_dvd_mul
  (a_div_a_zero_num_spec hp hreg hζ e hy hz η₁ hη₁)
  (a_div_a_zero_denom_spec hp hreg hζ e hy hz η₂ hη₂)
State after:
no goals

State before:
case intro.intro.intro.refine_2
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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ α η₂ hη₂ * β η₁ hη₁
Tactic:
exact hζ.zeta_sub_one_prime'.not_dvd_mul
  (a_div_a_zero_num_spec hp hreg hζ e hy hz η₂ hη₂)
  (a_div_a_zero_denom_spec hp hreg hζ e hy hz η₁ hη₁)
State after:
no goals

State before:
case intro.intro.intro.refine_3
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) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ β η₁ hη₁ * β η₂ hη₂
Tactic:
exact hζ.zeta_sub_one_prime'.not_dvd_mul
  (a_div_a_zero_denom_spec hp hreg hζ e hy hz η₁ hη₁)
  (a_div_a_zero_denom_spec hp hreg hζ e hy hz η₂ hη₂)
State after:
no goals