-- Mathlib/FieldTheory/KummerPolynomial.lean
theorem pow_ne_of_irreducible_X_pow_sub_C {n : ℕ} {a : K}
    (H : Irreducible (X ^ n - C a)) {m : ℕ} (hm : m ∣ n) (hm' : m ≠ 1) (b : K) : b ^ m ≠ a

Proof state:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
this : q.degree = 0
hq : m * k = k
⊢ False

Tactic:
exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
⊢ b ^ m ≠ a

Tactic:
have hn : n ≠ 0 := fun e ↦ not_irreducible_C
  (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)

Result:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
hn : n ≠ 0
⊢ b ^ m ≠ a

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
hn : n ≠ 0
⊢ b ^ m ≠ a

Tactic:
obtain ⟨k, rfl⟩ := hm

Result:
case intro
K : Type u
inst✝ : Field K
a : K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
H : Irreducible (X ^ (m * k) - C a)
hn : m * k ≠ 0
⊢ b ^ m ≠ a

Proof state:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
this : q.degree = 0
⊢ False

Tactic:
apply_fun degree at hq

Result:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
this : q.degree = 0
hq : ((X ^ k) ^ m - C b ^ m).degree = ((X ^ k - C b) * q).degree
⊢ False

Proof state:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ False

Tactic:
have : degree q = 0 := by
  simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
    Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 _ q rfl

Result:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
this : q.degree = 0
⊢ False

Proof state:
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ q.degree = 0

Tactic:
simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
  Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 _ q rfl

Result:
no goals

Proof state:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
this : q.degree = 0
hq : ((X ^ k) ^ m - C b ^ m).degree = ((X ^ k - C b) * q).degree
⊢ False

Tactic:
simp only [this, ← pow_mul, mul_comm k m, degree_X_pow_sub_C, Nat.pos_iff_ne_zero.mpr hn,
  Nat.pos_iff_ne_zero.mpr (mul_ne_zero_iff.mp hn).2, degree_mul, ← map_pow, add_zero,
  Nat.cast_injective.eq_iff] at hq

Result:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
this : q.degree = 0
hq : m * k = k
⊢ False

Proof state:
case intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible (X ^ (m * k) - C (b ^ m))
⊢ False

Tactic:
obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m

Result:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible (X ^ (m * k) - C (b ^ m))
q : K[X]
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ False

Proof state:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible (X ^ (m * k) - C (b ^ m))
q : K[X]
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ False

Tactic:
rw [mul_comm, pow_mul, map_pow, hq] at H

Result:
case intro.intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ False

Proof state:
case intro
K : Type u
inst✝ : Field K
a : K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
H : Irreducible (X ^ (m * k) - C a)
hn : m * k ≠ 0
⊢ b ^ m ≠ a

Tactic:
rintro rfl

Result:
case intro
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible (X ^ (m * k) - C (b ^ m))
⊢ False

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
e : n = 0
⊢ Irreducible (C (1 - a))

Tactic:
simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H

Result:
no goals