-- Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
theorem cyclotomic_irreducible_pow_of_irreducible_pow {p : ℕ} (hp : Nat.Prime p) {R} [CommRing R]
    [IsDomain R] {n m : ℕ} (hmn : m ≤ n) (h : Irreducible (cyclotomic (p ^ n) R)) :
    Irreducible (cyclotomic (p ^ m) R)

Proof state:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
rcases m.eq_zero_or_pos with (rfl | hm)

Result:
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : Irreducible (cyclotomic (p ^ n) R)
hmn : 0 ≤ n
⊢ Irreducible (cyclotomic (p ^ 0) R)

case inr
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
hm : m > 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Proof state:
case inr.intro
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn : m ≤ m + k
h : Irreducible (cyclotomic (p ^ (m + k)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
induction' k with k hk

Result:
case inr.intro.zero
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
hmn : m ≤ m + 0
h : Irreducible (cyclotomic (p ^ (m + 0)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (cyclotomic (p ^ (m + (k + 1))) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

Proof state:
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : Irreducible (cyclotomic (p ^ n) R)
hmn : 0 ≤ n
⊢ Irreducible (cyclotomic (p ^ 0) R)

Tactic:
simpa using irreducible_X_sub_C (1 : R)

Result:
no goals

Proof state:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible ((expand R p) (cyclotomic (p ^ (m + k)) R))
this : m + k ≠ 0
⊢ m ≤ m + k

Tactic:
omega

Result:
no goals

Proof state:
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible ((expand R p) (cyclotomic (p ^ (m + k)) R))
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
exact hk (by omega) (of_irreducible_expand hp.ne_zero h)

Result:
no goals

Proof state:
case inr.intro.zero
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
hmn : m ≤ m + 0
h : Irreducible (cyclotomic (p ^ (m + 0)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
simpa using h

Result:
no goals

Proof state:
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (cyclotomic (p ^ (m + (k + 1))) R)
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
rw [Nat.add_succ, pow_succ, ← cyclotomic_expand_eq_cyclotomic hp <| dvd_pow_self p this] at h

Result:
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible ((expand R p) (cyclotomic (p ^ (m + k)) R))
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Proof state:
case inr
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
hm : m > 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Result:
case inr.intro
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn : m ≤ m + k
h : Irreducible (cyclotomic (p ^ (m + k)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

Proof state:
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (cyclotomic (p ^ (m + (k + 1))) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'

Result:
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (cyclotomic (p ^ (m + (k + 1))) R)
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)