Theorem: stuff (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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + (↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    (↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
Tactic:
rw [← mul_right_inj' (x_plus_y_mul_ne_zero hp hζ e hz η₀), mul_add]
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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (x + y * ↑η₀) * ((↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p) +
      (x + y * ↑η₀) * ((↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p) =
    (x + y * ↑η₀) * ((↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ 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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (x + y * ↑η₀) * ((↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p) +
      (x + y * ↑η₀) * ((↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p) =
    (x + y * ↑η₀) * ((↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p)
Tactic:
simp_rw [mul_left_comm (x + y * η₀), mul_pow, mul_assoc, mul_left_comm (η₂ - η₀ : 𝓞 K),
  mul_left_comm (η₀ - η₁ : 𝓞 K), ← mul_assoc,
  associated_eta_zero_unit_spec, mul_assoc, ← mul_left_comm (η₂ - η₀ : 𝓞 K),
  ← mul_left_comm (η₀ - η₁ : 𝓞 K), pow_mul, ← mul_pow, mul_comm (β η₂ hη₂), ← mul_assoc]
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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * (x + y * ↑η₁) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p +
      (↑η₀ - ↑η₁) * (x + y * ↑η₂) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p =
    (↑η₂ - ↑η₁) * (x + y * ↑η₀) * (π ^ m * β η₁ hη₁ * β η₂ 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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * (x + y * ↑η₁) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p +
      (↑η₀ - ↑η₁) * (x + y * ↑η₂) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p =
    (↑η₂ - ↑η₁) * (x + y * ↑η₀) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p
Tactic:
rw [← add_mul]
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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ ((↑η₂ - ↑η₀) * (x + y * ↑η₁) + (↑η₀ - ↑η₁) * (x + y * ↑η₂)) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p =
    (↑η₂ - ↑η₁) * (x + y * ↑η₀) * (π ^ m * β η₁ hη₁ * β η₂ 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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ ((↑η₂ - ↑η₀) * (x + y * ↑η₁) + (↑η₀ - ↑η₁) * (x + y * ↑η₂)) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p =
    (↑η₂ - ↑η₁) * (x + y * ↑η₀) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p
Tactic:
congr 1
State after:
case e_a
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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * (x + y * ↑η₁) + (↑η₀ - ↑η₁) * (x + y * ↑η₂) = (↑η₂ - ↑η₁) * (x + y * ↑η₀)

State before:
case e_a
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η₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * (x + y * ↑η₁) + (↑η₀ - ↑η₁) * (x + y * ↑η₂) = (↑η₂ - ↑η₁) * (x + y * ↑η₀)
Tactic:
ring
State after:
no goals