awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : eval a ((derivative : (a : K[X]) → K[X]) f) ≠ 0
refine :
  ¬HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
refine₁ :
  ∀
    (h :
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
        f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])),
    eval a ((derivative : (a : K[X]) → K[X]) f) = 0
refine₂ :
  ∀
    (h :
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
        f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (this : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f),
    eval a ((derivative : (a : K[X]) → K[X]) f) = 0
refine₃ :
  ∀
    (h :
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
        f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (this : Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X]) (0 : K[X])),
    eval a ((derivative : (a : K[X]) → K[X]) f) = 0
⊢ IsCoprime (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))

Tactic:
classical
  refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_
  contrapose hf' with h
  have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
  rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
  rwa [← C_inj, C_0]

Premises used: Polynomial.monic_X_sub_C, Polynomial.C, Polynomial.C_inj, Polynomial.degree_X_sub_C, Polynomial.C_0, HSub.hSub, Polynomial.modByMonic_eq_zero_iff_dvd, Or.resolve_left, Polynomial.divByMonic, Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.X, DFunLike.coe, EuclideanDomain.dvd_or_coprime, Polynomial.irreducible_of_degree_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
rw :
  (∀ (q : R[X]),
      q.degree ≤
          (↑((HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X])).natDegree / 2) : WithBot ℕ) →
        q ∣ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) → IsUnit q) ↔
    ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
rw₁ : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q

Tactic:
rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]

Premises used: Polynomial.irreducible_mul_leadingCoeff_inv, Polynomial.Monic.irreducible_iff_degree_lt, Polynomial.monic_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ (∀ (q : R[X]),
      q.degree ≤
          (↑((HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X])).natDegree / 2) : WithBot ℕ) →
        q ∣ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) → IsUnit q) ↔
    ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q

Tactic:
simp [hp0, natDegree_mul_leadingCoeff_inv]

Premises used: Polynomial.natDegree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
contrapose : ∀ (hpu : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) = 1), IsUnit p
⊢ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1

Tactic:
contrapose hpu
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) = 1
⊢ IsUnit p

Tactic:
.of_mul_eq_one _ hpu

Premises used: IsUnit.of_mul_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) = 1
⊢ IsUnit p

Tactic:
exact .of_mul_eq_one _ hpu
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1

Tactic:
have : p * C (leadingCoeff p)⁻¹ ≠ 1 := by
    contrapose hpu
    exact .of_mul_eq_one _ hpu
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
this : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1
rw :
  (∀ (q : R[X]),
      q.Monic →
        q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) →
          ¬q ∣ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X])) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this,
      natDegree_mul_leadingCoeff_inv _ hp0]

Premises used: Polynomial.natDegree_mul_leadingCoeff_inv, Polynomial.irreducible_mul_leadingCoeff_inv, Polynomial.Monic.irreducible_iff_lt_natDegree_lt, Polynomial.monic_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
this : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1
⊢ (∀ (q : R[X]),
      q.Monic →
        q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) →
          ¬q ∣ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X])) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
simp only [IsUnit.dvd_mul_right
    (isUnit_C.mpr (IsUnit.mk0 (leadingCoeff p)⁻¹ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))]

Premises used: Iff.mpr, Polynomial.leadingCoeff, Polynomial.isUnit_C, Inv.inv, Polynomial.leadingCoeff_ne_zero, IsUnit.mk0, inv_ne_zero, IsUnit.dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
pos : ∀ (ha : a = 0), HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
neg : ∀ (ha : ¬a = 0), HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
ha : a = 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
ha : ¬a = 0
neg : a * (C : (a : R) → R[X]) 1 = a
neg₁ : a.leadingCoeff ≠ 0
neg₂ : a.leadingCoeff ≠ 0
neg₃ : a ≠ 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a

Tactic:
rw [prod_normalizedFactors_eq, normalize_apply, coe_normUnit, CommGroupWithZero.coe_normUnit,
    mul_comm, mul_assoc, ← map_mul, inv_mul_cancel₀]

Premises used: CommGroupWithZero.coe_normUnit, mul_assoc, normalize_apply, map_mul, Polynomial.coe_normUnit, mul_comm, UniqueFactorizationMonoid.prod_normalizedFactors_eq, inv_mul_cancel₀
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a * (C : (a : R) → R[X]) 1 = a

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a.leadingCoeff ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
inst_1 : DecidableEq R
hq : q ≠ 0
pos : ∀ (hp : p = 0), p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
neg : ∀ (hp : ¬p = 0), p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
inst_1 : DecidableEq R
hq : q ≠ 0
hp : p = 0
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q

Tactic:
simpa [hp] using zero_notMem_normalizedFactors _

Premises used: UniqueFactorizationMonoid.zero_notMem_normalizedFactors
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
inst_1 : DecidableEq R
hq : q ≠ 0
hp : ¬p = 0
neg : Irreducible p ∧ (normalize : (a : R[X]) → R[X]) p = p ∧ p ∣ q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
neg₁ neg₂ : Irreducible p ∧ p.Monic ∧ p ∣ q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q

Tactic:
rw [mem_normalizedFactors_iff' hq, normalize_eq_self_iff_monic hp]

Premises used: Polynomial.normalize_eq_self_iff_monic, UniqueFactorizationMonoid.mem_normalizedFactors_iff'
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
p : R[X]
inst_1 : DecidableEq R
inst_2 : Field S
inst_3 : DecidableEq S
f : R →+* S
pos : ∀ (hp : p = 0), map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)
neg : ∀ (hp : ¬p = 0), map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)
⊢ map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
p : R[X]
inst_1 : DecidableEq R
inst_2 : Field S
inst_3 : DecidableEq S
f : R →+* S
hp : p = 0
⊢ map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
p : R[X]
inst_1 : DecidableEq R
inst_2 : Field S
inst_3 : DecidableEq S
f : R →+* S
hp : ¬p = 0
⊢ map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)

Tactic:
simp [normalize_apply, Polynomial.map_mul, normUnit, hp]

Premises used: Polynomial.map_mul, normalize_apply, NormalizationMonoid.normUnit
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : Semiring S
inst_2 : Nontrivial S
inst_3 : Algebra R S
p : R[X]
⊢ Monic.{v} (R := S) (((mapAlg R S : AlgHom.{u, u, v} R R[X] S[X]) : (a : R[X]) → S[X]) p) ↔ p.Monic

Tactic:
simp [mapAlg_eq_map, monic_map_iff]

Premises used: Polynomial.monic_map_iff, Polynomial.mapAlg_eq_map
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
inl : ∀ (h : 0 ∣ p₁ - p₂), p₁ % 0 = p₂ % 0
inr : ∀ (hq : q ≠ 0), p₁ % q = p₂ % q
⊢ p₁ % q = p₂ % q

Tactic:
obtain rfl | hq := eq_or_ne q 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ : R[X]
h : 0 ∣ p₁ - p₂
⊢ p₁ % 0 = p₂ % 0

Tactic:
simpa [sub_eq_zero] using h

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).Monic

Tactic:
simp [Polynomial.Monic.def, hq]

Premises used: Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
inr : HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) ∣ p₁ - p₂
⊢ p₁ %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    p₂ %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])

Tactic:
apply Polynomial.modByMonic_eq_of_dvd_sub (by simp [Polynomial.Monic.def, hq])

Premises used: Polynomial.modByMonic_eq_of_dvd_sub
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
inr : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) q ∣ p₁ - p₂
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) ∣ p₁ - p₂

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ q.leadingCoeff⁻¹ ≠ 0

Tactic:
simpa using hq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) q ∣ p₁ - p₂

Tactic:
exact (Polynomial.C_mul_dvd (by simpa using hq)).mpr h

Premises used: Iff.mpr, Polynomial.C_mul_dvd
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
obtain : ∀ (x : F) (hf : (C : (a : F) → F[X]) x = f), False
⊢ False

Tactic:
obtain ⟨x, hf⟩ := natDegree_eq_zero.1 H

Premises used: Iff.mp, Polynomial.natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
pos : ∀ (hx : x = 0), False
neg : ∀ (hx : ¬x = 0), False
⊢ False

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
hx : x = 0
⊢ Irreducible.{u_1} (M := F[X]) 0

Tactic:
rw [← hf, hx, map_zero] at h

Premises used: map_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
hx : x = 0
h₁ : Irreducible.{u_1} (M := F[X]) 0
⊢ (C : (a : F) → F[X]) x = f

Tactic:
rw [← hf, hx, map_zero] at h

Premises used: map_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
hx : x = 0
h₁ : Irreducible.{u_1} (M := F[X]) 0
hf₁ : (C : (a : F) → F[X]) x = f
⊢ x = 0

Tactic:
rw [← hf, hx, map_zero] at h

Premises used: map_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible.{u_1} (M := F[X]) 0
hf : (C : (a : F) → F[X]) x = f
hx : x = 0
⊢ False

Tactic:
not_irreducible_zero h

Premises used: not_irreducible_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible.{u_1} (M := F[X]) 0
hf : (C : (a : F) → F[X]) x = f
hx : x = 0
⊢ False

Tactic:
exact not_irreducible_zero h

Premises used: not_irreducible_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
hx : ¬x = 0
⊢ False

Tactic:
h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))

Premises used: Iff.mpr, Ne.isUnit, Irreducible.not_isUnit, Eq.rec, Polynomial.isUnit_C
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
hx : ¬x = 0
⊢ False

Tactic:
exact h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))

Premises used: Iff.mpr, Ne.isUnit, Irreducible.not_isUnit, Eq.rec, Polynomial.isUnit_C
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
rw : 0 < f.natDegree
⊢ 0 < f.degree

Tactic:
rw [← natDegree_pos_iff_degree_pos]

Premises used: Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
⊢ 0 < f.natDegree

Tactic:
h.natDegree_pos

Premises used: Irreducible.natDegree_pos
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
⊢ 0 < f.natDegree

Tactic:
exact h.natDegree_pos

Premises used: Irreducible.natDegree_pos
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
R : Type u_2
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
h : ∀ (x : R[X]) (n : ℕ), (m • x).coeff n = (map (MulSemiringAction.toRingHom M R m) x).coeff n
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
R : Type u_2
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
x : R[X]
n : ℕ
⊢ (m • x).coeff n = (map (MulSemiringAction.toRingHom M R m) x).coeff n

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
R : Type u_2
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
⊢ HSMul.hSMul (β := R[X]) m X = X

Tactic:
(smul_eq_map R m).symm ▸ map_X _

Premises used: Eq.rec, Polynomial.map_X, Polynomial.smul_eq_map, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x r : S
rw : eval (m • x) ((C : (a : S) → S[X]) (m • r)) = m • eval x ((C : (a : S) → S[X]) r)
rw₁ : m • r = m • eval x ((C : (a : S) → S[X]) r)
rw₂ rw₃ : m • r = m • r
⊢ eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X])) = m • eval x ((C : (a : S) → S[X]) r)

Tactic:
rw [smul_C, eval_C, eval_C]

Premises used: Polynomial.eval_C, Polynomial.smul_C
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f_1 : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
rw : eval (m • x) (m • f + m • g) = m • eval x (f + g)
rw₁ : eval (m • x) (m • f) + eval (m • x) (m • g) = m • eval x (f + g)
rw₂ : m • eval x f + eval (m • x) (m • g) = m • eval x (f + g)
rw₃ : m • eval x f + m • eval x g = m • eval x (f + g)
rw₄ : m • eval x f + m • eval x g = m • (eval x f + eval x g)
rw₅ rw₆ : m • eval x f + m • eval x g = m • eval x f + m • eval x g
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)

Tactic:
rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]

Premises used: Polynomial.eval_add, smul_add
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₄ :
  eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₅ :
  m • r * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₆ :
  m • r * (m • x) ^ (n + 1) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₇ : m • r * (m • x) ^ (n + 1) = m • (eval x ((C : (a : S) → S[X]) r) * eval x (HPow.hPow (α := S[X]) X (n + 1)))
rw₈ : m • r * (m • x) ^ (n + 1) = m • (r * eval x (HPow.hPow (α := S[X]) X (n + 1)))
rw₉ : m • r * (m • x) ^ (n + 1) = m • (r * x ^ (n + 1))
rw₁₀ : m • r * (m • x) ^ (n + 1) = m • r * m • x ^ (n + 1)
rw₁₁ rw₁₂ : m • r * (m • x) ^ (n + 1) = m • r * (m • x) ^ (n + 1)
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))

Tactic:
rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']

Premises used: smul_pow', Polynomial.eval_C, Polynomial.eval_X_pow, Polynomial.eval_mul, Polynomial.smul_X, Polynomial.smul_C, smul_mul'
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
S : Type u_3
inst : CommSemiring S
G : Type u_4
inst_1 : Group G
inst_2 : MulSemiringAction G S
g : G
f : S[X]
x : S
rw : eval (g • x) f = eval (g • x) (g • g⁻¹ • f)
rw₁ rw₂ : eval (g • x) f = eval (g • x) f
⊢ eval (g • x) f = g • eval x (g⁻¹ • f)

Tactic:
rw [← smul_eval_smul, smul_inv_smul]

Premises used: Polynomial.smul_eval_smul, smul_inv_smul
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
S : Type u_3
inst : CommSemiring S
G : Type u_4
inst_1 : Group G
inst_2 : MulSemiringAction G S
g : G
f : S[X]
x : S
rw : eval x (g • f) = eval (g • g⁻¹ • x) (g • f)
rw₁ rw₂ : eval x (g • f) = eval x (g • f)
⊢ eval x (g • f) = g • eval (g⁻¹ • x) f

Tactic:
rw [← smul_eval_smul, smul_inv_smul]

Premises used: Polynomial.smul_eval_smul, smul_inv_smul
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
⊢ Monic (prodXSubSMul G R x)

Tactic:
Polynomial.monic_prod_of_monic _ _ fun _ _ ↦ Polynomial.monic_X_sub_C _

Premises used: Polynomial.monic_X_sub_C, MulAction.ofQuotientStabilizer, Polynomial.monic_prod_of_monic, prodXSubSMul
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
this : DecidableEq R := Classical.decEq R
⊢ Eq (α := R)
    (((↑(AlgHom.toRingHom (aeval x)) : R[X] →* R) : (a : R[X]) → R)
        (HSub.hSub (α := R[X]) (β := R[X]) X
          ((C : (a : R) → R[X]) (ofQuotientStabilizer G x (↑1 : G ⧸ stabilizer G x)) : R[X])) :
      R)
    (0 : R)

Tactic:
simp