refine ⟨_, _, ?_, ?_, h⟩
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'
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'