-- Mathlib/FieldTheory/KummerExtension.lean
theorem X_pow_mul_sub_C_irreducible
    {n m : ℕ} {a : K} (hm : Irreducible (X ^ m - C a))
    (hn : ∀ (E : Type u) [Field E] [Algebra K E] (x : E) (_ : minpoly K x = X ^ m - C a),
      Irreducible (X ^ n - C (AdjoinSimple.gen K x))) :
    Irreducible (X ^ (n * m) - C a)

Proof state:
K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ m ≠ 0

Tactic:
rintro rfl

Result:
K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (X ^ 0 - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (X ^ 0 - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False

Tactic:
rw [pow_zero, ← C.map_one, ← map_sub] at hm

Result:
K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (C (1 - a))
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False

Proof state:
K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ Irreducible (X ^ (n * m) - C a)

Tactic:
have hm' : m ≠ 0 := by
  rintro rfl
  rw [pow_zero, ← C.map_one, ← map_sub] at hm
  exact not_irreducible_C _ hm

Result:
K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ Irreducible (X ^ (n * m) - C a)

Proof state:
K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ Irreducible (X ^ (n * m) - C a)

Tactic:
simpa [pow_mul] using irreducible_comp (monic_X_pow_sub_C a hm') (monic_X_pow n) hm
  (by simpa only [Polynomial.map_pow, map_X] using hn)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) (X ^ n) - C (AdjoinSimple.gen K x))

Tactic:
simpa only [Polynomial.map_pow, map_X] using hn

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (C (1 - a))
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False

Tactic:
exact not_irreducible_C _ hm

Result:
no goals