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
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = 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
this : Fact (↑p).Prime := hpri
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = 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
this : Fact (↑p).Prime := hpri
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = z ^ ↑p
Tactic:
letI : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = z ^ ↑p
Tactic:
rintro ⟨x, y, z, hy, hz, hz', e⟩
State after:
case 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
⊢ False

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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
m : ℕ
z : 𝓞 K
hm : 1 ≤ m
hz'' : ¬↑hζ.unit' - 1 ∣ z
hz : ↑hζ.unit' - 1 ∣ (↑hζ.unit' - 1) ^ m * z
hz' : (↑hζ.unit' - 1) ^ m * z ≠ 0
e : x ^ ↑p + y ^ ↑p = ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
⊢ False
Tactic:
refine not_exists_solution hp hreg hζ hm ⟨x, y, z, 1, 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
m : ℕ
z : 𝓞 K
hm : 1 ≤ m
hz'' : ¬↑hζ.unit' - 1 ∣ z
hz : ↑hζ.unit' - 1 ∣ (↑hζ.unit' - 1) ^ m * z
hz' : (↑hζ.unit' - 1) ^ m * z ≠ 0
e : x ^ ↑p + y ^ ↑p = ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
⊢ x ^ ↑p + y ^ ↑p = ↑1 * ((↑hζ.unit' - 1) ^ 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
m : ℕ
z : 𝓞 K
hm : 1 ≤ m
hz'' : ¬↑hζ.unit' - 1 ∣ z
hz : ↑hζ.unit' - 1 ∣ (↑hζ.unit' - 1) ^ m * z
hz' : (↑hζ.unit' - 1) ^ m * z ≠ 0
e : x ^ ↑p + y ^ ↑p = ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
⊢ x ^ ↑p + y ^ ↑p = ↑1 * ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
Tactic:
rwa [Units.val_one, one_mul]
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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'
Tactic:
have H : multiplicity.Finite ((hζ.unit' : 𝓞 K) - 1) z := WfDvdMonoid.multiplicity_finite
  (M := 𝓞 K) hζ.zeta_sub_one_prime'.not_unit hz'
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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'

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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'
Tactic:
obtain ⟨z', h⟩ := multiplicity.pow_multiplicity_dvd 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'

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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'
Tactic:
refine ⟨_, _, ?_, ?_, h⟩
State after:
case 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ 1 ≤ (multiplicity (↑hζ.unit' - 1) z).get H

case 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ ¬↑hζ.unit' - 1 ∣ z'

State before:
case 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ 1 ≤ (multiplicity (↑hζ.unit' - 1) z).get H
Tactic:
rwa [← PartENat.coe_le_coe, PartENat.natCast_get, ← multiplicity.pow_dvd_iff_le_multiplicity,
  pow_one]
State after:
no goals

State before:
case 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ ¬↑hζ.unit' - 1 ∣ z'
Tactic:
intro h'
State after:
case 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
⊢ False

State before:
case 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
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
⊢ False
Tactic:
have := mul_dvd_mul_left (((hζ.unit' : 𝓞 K) - 1) ^ Part.get (multiplicity _ z) H) h'
State after:
case 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
this✝¹ : Fact (↑p).Prime := hpri
this✝ : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
this :
  (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * (↑hζ.unit' - 1) ∣
    (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ False

State before:
case 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
this✝¹ : Fact (↑p).Prime := hpri
this✝ : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
this :
  (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * (↑hζ.unit' - 1) ∣
    (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ False
Tactic:
rw [← pow_succ, ← h] at this
State after:
case 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
this✝¹ : Fact (↑p).Prime := hpri
this✝ : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
this : (↑hζ.unit' - 1) ^ ((multiplicity (↑hζ.unit' - 1) z).get H + 1) ∣ z
⊢ False

State before:
case 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
this✝¹ : Fact (↑p).Prime := hpri
this✝ : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
this : (↑hζ.unit' - 1) ^ ((multiplicity (↑hζ.unit' - 1) z).get H + 1) ∣ z
⊢ False
Tactic:
exact multiplicity.is_greatest' H (Nat.lt_succ_self _) this
State after:
no goals