Theorem: p_pow_dvd_c_eta_zero_aux (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) }
inst✝ : DecidableEq (𝓞 K)
⊢ gcd (𝔭 ^ (m * ↑p)) (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η) = 1
Tactic:
rw [← Ideal.isCoprime_iff_gcd]
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) }
inst✝ : DecidableEq (𝓞 K)
⊢ IsCoprime (𝔭 ^ (m * ↑p)) (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η)

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) }
inst✝ : DecidableEq (𝓞 K)
⊢ IsCoprime (𝔭 ^ (m * ↑p)) (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η)
Tactic:
apply IsCoprime.pow_left
State after:
case H
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) }
inst✝ : DecidableEq (𝓞 K)
⊢ IsCoprime 𝔭 (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η)

State before:
case H
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) }
inst✝ : DecidableEq (𝓞 K)
⊢ IsCoprime 𝔭 (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η)
Tactic:
rw [Ideal.isCoprime_iff_gcd, hζ.prime_span_sub_one.irreducible.gcd_eq_one_iff,
  hζ.prime_span_sub_one.dvd_finset_prod_iff]
State after:
case H
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) }
inst✝ : DecidableEq (𝓞 K)
⊢ ¬∃ a ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔭 ∣ 𝔠 a

State before:
case H
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) }
inst✝ : DecidableEq (𝓞 K)
⊢ ¬∃ a ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔭 ∣ 𝔠 a
Tactic:
rintro ⟨η, hη, h⟩
State after:
case H.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) }
inst✝ : DecidableEq (𝓞 K)
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}
h : 𝔭 ∣ 𝔠 η
⊢ False

State before:
case H.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) }
inst✝ : DecidableEq (𝓞 K)
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}
h : 𝔭 ∣ 𝔠 η
⊢ False
Tactic:
rw [p_dvd_c_iff] at h
State after:
case H.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) }
inst✝ : DecidableEq (𝓞 K)
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}
h : η = η₀
⊢ False

State before:
case H.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) }
inst✝ : DecidableEq (𝓞 K)
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}
h : η = η₀
⊢ False
Tactic:
simp only [Finset.mem_sdiff, Finset.mem_singleton] at hη
State after:
case H.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) }
inst✝ : DecidableEq (𝓞 K)
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
h : η = η₀
hη : η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach ∧ ¬η = η₀
⊢ False

State before:
case H.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) }
inst✝ : DecidableEq (𝓞 K)
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
h : η = η₀
hη : η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach ∧ ¬η = η₀
⊢ False
Tactic:
exact hη.2 h
State after:
no goals