Theorem: prod_c (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) }
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Tactic:
have e' := span_pow_add_pow_eq hζ e
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) }
e' : Ideal.span {x ^ ↑p + y ^ ↑p} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : Ideal.span {x ^ ↑p + y ^ ↑p} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Tactic:
rw [pow_add_pow_eq_prod_add_zeta_runity_mul
  (hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)) hζ.unit'_coe] at e'
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) }
e' : Ideal.span {∏ ζ ∈ nthRootsFinset (↑p) (𝓞 K), (x + ζ * y)} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : Ideal.span {∏ ζ ∈ nthRootsFinset (↑p) (𝓞 K), (x + ζ * y)} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Tactic:
rw [← Ideal.prod_span_singleton, ← Finset.prod_attach] at e'
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) }
e' : ∏ x_1 ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, Ideal.span {x + ↑x_1 * y} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : ∏ x_1 ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, Ideal.span {x + ↑x_1 * y} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Tactic:
simp_rw [mul_comm _ y, ← m_mul_c_mul_p hp hζ e hy,
  Finset.prod_mul_distrib, Finset.prod_const, Finset.card_attach,
  hζ.unit'_coe.card_nthRootsFinset] at e'
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) }
e' : (𝔪 ^ ↑p * ∏ x_1 ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 x_1) * 𝔭 ^ ↑p = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : (𝔪 ^ ↑p * ∏ x_1 ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 x_1) * 𝔭 ^ ↑p = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Tactic:
rw [← mul_right_inj'
  ((pow_ne_zero_iff hpri.out.ne_zero).mpr (m_ne_zero hζ e hy) : _),
  ← mul_left_inj' ((pow_ne_zero_iff hpri.out.ne_zero).mpr (p_ne_zero hζ) : _), e',
  exists_ideal_pow_eq_c_aux]
State after:
no goals