-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_prime_pow_eq_geom_sum {R : Type*} [CommRing R] {p n : ℕ} (hp : p.Prime) :
    cyclotomic (p ^ (n + 1)) R = ∑ i ∈ Finset.range p, (X ^ p ^ n) ^ i

Proof state:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) *
      ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (n_n + 1 + 1) - 1

Tactic:
rw [mul_comm _ (∑ i ∈ _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul]

Result:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ X ^ (p ^ (n_n + 1) * p) = X ^ p ^ (n_n + 1 + 1)

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this✝ :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
this : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (0 + 1)) R = ∑ i ∈ range p, (X ^ p ^ 0) ^ i

Tactic:
simp [cyclotomic_prime]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
⊢ ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1

Tactic:
intro m

Result:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1

Tactic:
have := eq_cyclotomic_iff (R := R) (P := ∑ i ∈ range p, (X ^ p ^ m) ^ i)
  (pow_pos hp.pos (m + 1))

Result:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  ∑ i ∈ range p, (X ^ p ^ m) ^ i = cyclotomic (p ^ (m + 1)) R ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n) ^ i

Tactic:
induction' n with n_n n_ih

Result:
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (0 + 1)) R = ∑ i ∈ range p, (X ^ p ^ 0) ^ i

case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ cyclotomic (p ^ (n_n + 1 + 1)) R = ∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ cyclotomic (p ^ (n_n + 1 + 1)) R = ∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i

Tactic:
rw [((eq_cyclotomic_iff (pow_pos hp.pos (n_n + 1 + 1)) _).mpr _).symm]

Result:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) * ∏ i ∈ (p ^ (n_n + 1 + 1)).properDivisors, cyclotomic i R =
    X ^ p ^ (n_n + 1 + 1) - 1

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (0 + 1)) R = ∑ i ∈ range p, (X ^ p ^ 0) ^ i

Tactic:
haveI := Fact.mk hp

Result:
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this✝ :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
this : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (0 + 1)) R = ∑ i ∈ range p, (X ^ p ^ 0) ^ i

Proof state:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) * ∏ i ∈ (p ^ (n_n + 1 + 1)).properDivisors, cyclotomic i R =
    X ^ p ^ (n_n + 1 + 1) - 1

Tactic:
rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]

Result:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) *
      ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (n_n + 1 + 1) - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1

Tactic:
rw [this, Nat.prod_properDivisors_prime_pow hp]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ X ^ (p ^ (n_n + 1) * p) = X ^ p ^ (n_n + 1 + 1)

Tactic:
simp only [pow_add, pow_one]

Result:
no goals