Theorem: FltRegular.not_exists_solution (FltRegular/CaseII/Statement.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
m : ℕ
hm : 1 ≤ m
⊢ ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m * z') ^ ↑p
Tactic:
induction' m, hm using Nat.le_induction with m' _ IH
State after:
case base
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
m : ℕ
⊢ ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ 1 * z') ^ ↑p

case succ
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
m m' : ℕ
hmn✝ : 1 ≤ m'
IH :
  ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m' * z') ^ ↑p
⊢ ¬∃ x' y' z' ε₃,
      ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ (m' + 1) * z') ^ ↑p

State before:
case base
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
m : ℕ
⊢ ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ 1 * z') ^ ↑p
Tactic:
rintro ⟨x, y, z, ε₃, hy, hz, e⟩
State after:
case base.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
m : ℕ
x y z : 𝓞 K
ε₃ : (𝓞 K)ˣ
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ¬↑hζ.unit' - 1 ∣ z
e : x ^ ↑p + y ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ 1 * z) ^ ↑p
⊢ False

State before:
case base.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
m : ℕ
x y z : 𝓞 K
ε₃ : (𝓞 K)ˣ
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ¬↑hζ.unit' - 1 ∣ z
e : x ^ ↑p + y ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ 1 * z) ^ ↑p
⊢ False
Tactic:
exact zero_lt_one.not_le (one_le_m hp hζ e hy hz)
State after:
no goals

State before:
case succ
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
m m' : ℕ
hmn✝ : 1 ≤ m'
IH :
  ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m' * z') ^ ↑p
⊢ ¬∃ x' y' z' ε₃,
      ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ (m' + 1) * z') ^ ↑p
Tactic:
rintro ⟨x, y, z, ε₃, hy, hz, e⟩
State after:
case succ.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
m m' : ℕ
hmn✝ : 1 ≤ m'
IH :
  ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m' * z') ^ ↑p
x y z : 𝓞 K
ε₃ : (𝓞 K)ˣ
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ¬↑hζ.unit' - 1 ∣ z
e : x ^ ↑p + y ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ (m' + 1) * z) ^ ↑p
⊢ False

State before:
case succ.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
m m' : ℕ
hmn✝ : 1 ≤ m'
IH :
  ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m' * z') ^ ↑p
x y z : 𝓞 K
ε₃ : (𝓞 K)ˣ
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ¬↑hζ.unit' - 1 ∣ z
e : x ^ ↑p + y ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ (m' + 1) * z) ^ ↑p
⊢ False
Tactic:
exact IH (exists_solution' hp hreg hζ e hy hz)
State after:
no goals