Theorem: div_one_sub_zeta_mem (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) }
⊢ IsIntegral ℤ (↑(x + y * ↑η) / (ζ - 1))
Tactic:
obtain ⟨⟨a, ha⟩, e⟩ := one_sub_zeta_dvd_zeta_pow_sub hp hζ e η
State after:
case intro.mk
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) }
a : K
ha : a ∈ integralClosure ℤ K
e : x + y * ↑η = π * ⟨a, ha⟩
⊢ IsIntegral ℤ (↑(x + y * ↑η) / (ζ - 1))

State before:
case intro.mk
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) }
a : K
ha : a ∈ integralClosure ℤ K
e : x + y * ↑η = π * ⟨a, ha⟩
⊢ IsIntegral ℤ (↑(x + y * ↑η) / (ζ - 1))
Tactic:
rw [e, mul_comm]
State after:
case intro.mk
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) }
a : K
ha : a ∈ integralClosure ℤ K
e : x + y * ↑η = π * ⟨a, ha⟩
⊢ IsIntegral ℤ (↑(⟨a, ha⟩ * π) / (ζ - 1))

State before:
case intro.mk
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) }
a : K
ha : a ∈ integralClosure ℤ K
e : x + y * ↑η = π * ⟨a, ha⟩
⊢ IsIntegral ℤ (↑(⟨a, ha⟩ * π) / (ζ - 1))
Tactic:
simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub, IsPrimitiveRoot.coe_unit'_coe,
  map_one]
State after:
case intro.mk
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) }
a : K
ha : a ∈ integralClosure ℤ K
e : x + y * ↑η = π * ⟨a, ha⟩
⊢ IsIntegral ℤ (a * (ζ - 1) / (ζ - 1))

State before:
case intro.mk
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) }
a : K
ha : a ∈ integralClosure ℤ K
e : x + y * ↑η = π * ⟨a, ha⟩
⊢ IsIntegral ℤ (a * (ζ - 1) / (ζ - 1))
Tactic:
rwa [mul_div_cancel_right₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
State after:
no goals