Theorem: associated_eta_zero (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) }
hη : η ≠ η₀
⊢ Associated ((x + y * ↑η₀) * α η hη ^ ↑p) ((x + y * ↑η) * π ^ (m * ↑p) * β η hη ^ ↑p)
Tactic:
simp_rw [← Ideal.span_singleton_eq_span_singleton,
  ← Ideal.span_singleton_mul_span_singleton, ← Ideal.span_singleton_pow,
  ← m_mul_c_mul_p hp hζ e hy, ← root_div_zeta_sub_one_dvd_gcd_spec, ← a_eta_zero_dvd_p_pow_spec]
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) }
hη : η ≠ η₀
⊢ 𝔪 * (𝔭 ^ m * 𝔞₀) ^ ↑p * 𝔭 * Ideal.span {α η hη} ^ ↑p = 𝔪 * 𝔞 η ^ ↑p * 𝔭 * 𝔭 ^ (m * ↑p) * Ideal.span {β η hη} ^ ↑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) }
hη : η ≠ η₀
⊢ 𝔪 * (𝔭 ^ m * 𝔞₀) ^ ↑p * 𝔭 * Ideal.span {α η hη} ^ ↑p = 𝔪 * 𝔞 η ^ ↑p * 𝔭 * 𝔭 ^ (m * ↑p) * Ideal.span {β η hη} ^ ↑p
Tactic:
rw [mul_comm _ 𝔞₀, mul_pow]
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) }
hη : η ≠ η₀
⊢ 𝔪 * (𝔞₀ ^ ↑p * (𝔭 ^ m) ^ ↑p) * 𝔭 * Ideal.span {α η hη} ^ ↑p =
    𝔪 * 𝔞 η ^ ↑p * 𝔭 * 𝔭 ^ (m * ↑p) * Ideal.span {β η hη} ^ ↑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) }
hη : η ≠ η₀
⊢ 𝔪 * (𝔞₀ ^ ↑p * (𝔭 ^ m) ^ ↑p) * 𝔭 * Ideal.span {α η hη} ^ ↑p =
    𝔪 * 𝔞 η ^ ↑p * 𝔭 * 𝔭 ^ (m * ↑p) * Ideal.span {β η hη} ^ ↑p
Tactic:
simp only [mul_assoc, mul_left_comm _ 𝔭]
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) }
hη : η ≠ η₀
⊢ 𝔭 * (𝔪 * (𝔞₀ ^ ↑p * ((𝔭 ^ m) ^ ↑p * Ideal.span {α η hη} ^ ↑p))) =
    𝔭 * (𝔪 * (𝔞 η ^ ↑p * (𝔭 ^ (m * ↑p) * Ideal.span {β η hη} ^ ↑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) }
hη : η ≠ η₀
⊢ 𝔭 * (𝔪 * (𝔞₀ ^ ↑p * ((𝔭 ^ m) ^ ↑p * Ideal.span {α η hη} ^ ↑p))) =
    𝔭 * (𝔪 * (𝔞 η ^ ↑p * (𝔭 ^ (m * ↑p) * Ideal.span {β η hη} ^ ↑p)))
Tactic:
rw [mul_left_comm (𝔞 η ^ (p : ℕ)), mul_left_comm (𝔞₀ ^ (p : ℕ)), ← pow_mul, ← mul_pow, ← mul_pow,
  a_mul_denom_eq_a_zero_mul_num]
State after:
no goals