-- Mathlib/FieldTheory/KummerExtension.lean
theorem X_pow_sub_C_irreducible_of_odd
    {n : ℕ} (hn : Odd n) {a : K} (ha : ∀ p : ℕ, p.Prime → p ∣ n → ∀ b : K, b ^ p ≠ a) :
    Irreducible (X ^ n - C a)

Proof state:
case h
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
this : IsIntegral K x
q : ℕ
hq : Nat.Prime q
hqn : q ∣ n
b : ↥K⟮x⟯
hb : b ^ q = AdjoinSimple.gen K x
⊢ (-1) ^ (adjoin.powerBasis this).dim * (minpoly K (adjoin.powerBasis this).gen).coeff 0 = a

Tactic:
simp [minpoly_gen, hx, hp.ne_zero.symm, (Nat.odd_mul.mp hn).1.neg_pow]

Result:
no goals

Proof state:
case h₁
K : Type u
inst✝ : Field K
hn : Odd 1
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 1 → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ 1 - C a)

Tactic:
simpa using irreducible_X_sub_C a

Result:
no goals

Proof state:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
h : ¬IsIntegral K x
⊢ False

Tactic:
simpa only [degree_zero, degree_X_pow_sub_C hp.pos,
  WithBot.natCast_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h))

Result:
no goals

Proof state:
case h
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝ : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
⊢ Irreducible (X ^ (p * n) - C a)

Tactic:
rw [mul_comm]

Result:
case h
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝ : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
⊢ Irreducible (X ^ (n * p) - C a)

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hn : Odd n
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ n - C a)

Tactic:
induction n using induction_on_primes generalizing K a with
| h₀ => simp [← Nat.not_even_iff_odd] at hn
| h₁ => simpa using irreducible_X_sub_C a
| h p n hp IH =>
  rw [mul_comm]
  apply X_pow_mul_sub_C_irreducible
    (X_pow_sub_C_irreducible_of_prime hp (ha p hp (dvd_mul_right _ _)))
  intro E _ _ x hx
  have : IsIntegral K x := not_not.mp fun h ↦ by
    simpa only [degree_zero, degree_X_pow_sub_C hp.pos,
      WithBot.natCast_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h))
  apply IH (Nat.odd_mul.mp hn).2
  intros q hq hqn b hb
  apply ha q hq (dvd_mul_of_dvd_right hqn p) (Algebra.norm _ b)
  rw [← map_pow, hb, ← adjoin.powerBasis_gen this,
    Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly]
  simp [minpoly_gen, hx, hp.ne_zero.symm, (Nat.odd_mul.mp hn).1.neg_pow]

Result:
no goals