awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
t : Multiset R
hs :
  Separable (R := R)
    (Multiset.prod
      (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
        (a ::ₘ a ::ₘ t)))
refine :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    Multiset.prod
      (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) (a ::ₘ a ::ₘ t))
⊢ False

Tactic:
refine not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs ?_)

Premises used: Polynomial.isUnit_of_self_mul_dvd_separable, Polynomial.not_isUnit_X_sub_C
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
t : Multiset R
hs :
  Separable (R := R)
    (Multiset.prod
      (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
        (a ::ₘ a ::ₘ t)))
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    Multiset.prod
      (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) (a ::ₘ a ::ₘ t))

Tactic:
simpa only [Multiset.map_cons, Multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)

Premises used: Multiset.map_cons, Multiset.prod_cons, mul_dvd_mul_left, dvd_mul_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
inl :
  ∀ (hn : IsUnit.{u} (M := R) (↑0 : R)),
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) ((C : (a : R) → R[X]) (↑u : R) : R[X])).Separable
inr :
  ∀ (hpos : n > 0), (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])).Separable
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])).Separable

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
u : Rˣ
h : Nontrivial R
hn : IsUnit.{u} (M := R) (↑0 : R)
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) ((C : (a : R) → R[X]) (↑u : R) : R[X])).Separable

Tactic:
simp at hn
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
inr :
  ∀ (n' : R) (hn' : n' * (↑n : R) = 1),
    ∃ (a : R[X]) (b : R[X]),
      a * HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X]) +
          HMul.hMul (β := R[X]) b
            ((derivative : (a : R[X]) → R[X])
                (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) :
              R[X]) =
        1
⊢ ∃ (a : R[X]) (b : R[X]),
    a * HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X]) +
        HMul.hMul (β := R[X]) b
          ((derivative : (a : R[X]) → R[X])
              (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) :
            R[X]) =
      1

Tactic:
obtain ⟨n', hn'⟩ := hn.exists_left_inv

Premises used: IsUnit.exists_left_inv
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * (↑n : R) = 1
⊢ ∃ (a : R[X]) (b : R[X]),
    a * HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X]) +
        HMul.hMul (β := R[X]) b
          ((derivative : (a : R[X]) → R[X])
              (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) :
            R[X]) =
      1

Tactic:
⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, ?_⟩

Premises used: Units.val, Polynomial.C, HMul.hMul, Inv.inv, Exists.intro, Polynomial.X, DFunLike.coe, Neg.neg
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * (↑n : R) = 1
inr :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
        (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) +
      HMul.hMul (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) n' : R[X]) *
          X)
        ((derivative : (a : R[X]) → R[X])
            (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) :
          R[X]) =
    1
⊢ ∃ (a : R[X]) (b : R[X]),
    a * HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X]) +
        HMul.hMul (β := R[X]) b
          ((derivative : (a : R[X]) → R[X])
              (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) :
            R[X]) =
      1

Tactic:
refine ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, ?_⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * (↑n : R) = 1
inr :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
        (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) n' : R[X]) * X *
        ((C : (a : R) → R[X]) (↑n : R) * HPow.hPow (α := R[X]) X (n - 1)) =
    1
⊢ HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
        (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) +
      HMul.hMul (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) n' : R[X]) *
          X)
        ((derivative : (a : R[X]) → R[X])
            (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) :
          R[X]) =
    1

Tactic:
rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]

Premises used: Polynomial.derivative_X, sub_zero, Polynomial.derivative_pow, Polynomial.derivative_sub, Polynomial.derivative_C, mul_one, Polynomial.X
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * (↑n : R) = 1
simp :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
        (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) n' : R[X]) * X *
        ((↑n : R[X]) * HPow.hPow (α := R[X]) X (n - 1)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) -
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
          (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) n' : R[X]) ((↑n : R[X]) : R[X])) *
        (X * HPow.hPow (α := R[X]) X (n - 1))
⊢ HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
        (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) n' : R[X]) * X *
        ((↑n : R[X]) * HPow.hPow (α := R[X]) X (n - 1)) =
    HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) ((↑u⁻¹ : R) * (↑u : R)) : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) (HPow.hPow (α := R[X]) X n)) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
          ((C : (a : R) → R[X]) (n' * (↑n : R)) : R[X]) *
        (X * HPow.hPow (α := R[X]) X (n - 1))

Tactic:
simp only [C.map_mul, C_eq_natCast]

Premises used: Polynomial.C, Polynomial.C_eq_natCast, RingHom.map_mul
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * (↑n : R) = 1
⊢ HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
        (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) n' : R[X]) * X *
        ((↑n : R[X]) * HPow.hPow (α := R[X]) X (n - 1)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) -
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
          (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) n' : R[X]) ((↑n : R[X]) : R[X])) *
        (X * HPow.hPow (α := R[X]) X (n - 1))

Tactic:
ring
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * (↑n : R) = 1
⊢ HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) ((↑u⁻¹ : R) * (↑u : R)) : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) (HPow.hPow (α := R[X]) X n)) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
          ((C : (a : R) → R[X]) (n' * (↑n : R)) : R[X]) *
        (X * HPow.hPow (α := R[X]) X (n - 1)) =
    1

Tactic:
simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ',
        Nat.sub_add_cancel (show 1 ≤ n from hpos), sub_add_cancel]

Premises used: Polynomial.C, Units.inv_mul, RingHom.map_one, Nat.sub_add_cancel, mul_one, sub_add_cancel, pow_succ'
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * (↑n : R) = 1
n₁ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
        (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) n' : R[X]) * X *
        ((↑n : R[X]) * HPow.hPow (α := R[X]) X (n - 1)) =
    HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) ((↑u⁻¹ : R) * (↑u : R)) : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) (HPow.hPow (α := R[X]) X n)) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
          ((C : (a : R) → R[X]) (n' * (↑n : R)) : R[X]) *
        (X * HPow.hPow (α := R[X]) X (n - 1))
n₂ :
  HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) ((↑u⁻¹ : R) * (↑u : R)) : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) (HPow.hPow (α := R[X]) X n)) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
          ((C : (a : R) → R[X]) (n' * (↑n : R)) : R[X]) *
        (X * HPow.hPow (α := R[X]) X (n - 1)) =
    1
⊢ HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X])
        (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u⁻¹ : R) : R[X]) ((C : (a : R) → R[X]) n' : R[X]) * X *
        ((C : (a : R) → R[X]) (↑n : R) * HPow.hPow (α := R[X]) X (n - 1)) =
    1

Tactic:
calc
    -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
        C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) := by
      simp only [C.map_mul, C_eq_natCast]
      ring
    _ = 1 := by
      simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ',
        Nat.sub_add_cancel (show 1 ≤ n from hpos), sub_add_cancel]

Premises used: Polynomial.C, HMul.hMul, HSub.hSub, HPow.hPow, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb : IsUnit b
set :
  let f :=
    HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X]);
  f.Separable
⊢ (HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X])).Separable

Tactic:
set f := C a * X ^ n + C b * X + C c

Premises used: Polynomial.C, Polynomial.X, DFunLike.coe
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
obtain : ∀ (e : R) (hb : e * b = 1), f.Separable
⊢ f.Separable

Tactic:
obtain ⟨e, hb⟩ := hb.exists_left_inv

Premises used: IsUnit.exists_left_inv
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
⊢ f.Separable

Tactic:
⟨-derivative f, f + C e, ?_⟩

Premises used: Polynomial.derivative, Polynomial.C, HAdd.hAdd, Exists.intro, Polynomial.Separable, DFunLike.coe, Neg.neg, IsCoprime
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
refine :
  HMul.hMul (α := R[X]) (-(derivative : (a : R[X]) → R[X]) f : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X]))
        ((derivative : (a : R[X]) → R[X]) f : R[X]) =
    1
⊢ f.Separable

Tactic:
refine ⟨-derivative f, f + C e, ?_⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) b : R[X])

Tactic:
simp [hn, f, map_add derivative, derivative_C, derivative_X_pow]

Premises used: Polynomial.derivative, map_add, Polynomial.derivative_X_pow, Polynomial.derivative_C
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) b : R[X])

Tactic:
have hderiv : derivative f = C b := by
    simp [hn, f, map_add derivative, derivative_C, derivative_X_pow]
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
hderiv : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) b : R[X])
rw :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X])) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₁ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X])) =
    1
rw₂ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₃ :
  -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₄ :
  -HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₅ : 0 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
rw₆ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
rw₇ : Eq (α := R[X]) ((C : (a : R) → R[X]) (e * b) : R[X]) (1 : R[X])
rw₈ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
rw₉ rw₁₀ : Eq.{u + 1} (α := R[X]) 1 1
⊢ HMul.hMul (α := R[X]) (-(derivative : (a : R[X]) → R[X]) f : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X]))
        ((derivative : (a : R[X]) → R[X]) f : R[X]) =
    1

Tactic:
rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]

Premises used: add_assoc, zero_add, map_mul, neg_add_cancel, map_one, mul_comm, neg_mul, right_distrib
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
p n : ℕ
a b c : R
inst_1 : CharP R p
hn : p ∣ n
hb : IsUnit b
⊢ (HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X])).Separable

Tactic:
separable_C_mul_X_pow_add_C_mul_X_add_C a b c ((CharP.cast_eq_zero_iff R p n).2 hn) hb

Premises used: Iff.mpr, CharP.cast_eq_zero_iff, Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
pos : ∀ (hp : p = 0), rootMultiplicity x p ≤ 1
neg : ∀ (hp : ¬p = 0), rootMultiplicity x p ≤ 1
⊢ rootMultiplicity x p ≤ 1

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : p = 0
⊢ rootMultiplicity x p ≤ 1

Tactic:
simp [hp]
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
neg : emultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p ≤ 1
⊢ rootMultiplicity x p ≤ 1

Tactic:
rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
    Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Polynomial.rootMultiplicity_eq_multiplicity, Nat.cast_le, Polynomial.finiteMultiplicity_X_sub_C, if_neg, Nat.cast_one
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ emultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p ≤ 1

Tactic:
apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep

Premises used: Polynomial.emultiplicity_le_one_of_separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
pos : ∀ (hp : p = 0), rootMultiplicity x p ≤ 1
neg neg₁ : ∀ (hp : ¬p = 0), rootMultiplicity x p ≤ 1
neg₂ : ∀ (hp : ¬p = 0), emultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p ≤ 1
⊢ rootMultiplicity x p ≤ 1

Tactic:
classical
  by_cases hp : p = 0
  · simp [hp]
  rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
    Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]
  apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep

Premises used: Polynomial.rootMultiplicity_eq_multiplicity, Nat.cast_le, Nat.cast_one, Polynomial.emultiplicity_le_one_of_separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
rw : rootMultiplicity x p ≤ 1
⊢ Multiset.count x p.roots ≤ 1

Tactic:
rw [count_roots p]

Premises used: Polynomial.count_roots
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1

Tactic:
rootMultiplicity_le_one_of_separable hsep x

Premises used: Polynomial.rootMultiplicity_le_one_of_separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1

Tactic:
exact rootMultiplicity_le_one_of_separable hsep x

Premises used: Polynomial.rootMultiplicity_le_one_of_separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hsep : p.Separable
⊢ p.roots.Nodup

Tactic:
Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)

Premises used: Iff.mpr, Multiset.nodup_iff_count_le_one, Polynomial.count_roots_le_one
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hsep : p.Separable
⊢ p.roots.Nodup

Tactic:
exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)

Premises used: Iff.mpr, Multiset.nodup_iff_count_le_one, Polynomial.count_roots_le_one
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hsep : p.Separable
⊢ p.roots.Nodup

Tactic:
classical
  exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
h : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
g : F[X]
hg1 : Membership.mem (γ := Set F[X]) (nonunits F[X]) g
_hg2 : g ≠ 0
h_1 : g ∣ f
hg4 : g ∣ (derivative : (a : F[X]) → F[X]) f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : (↑u : F[X]) = p
rw : g * (↑u : F[X])
| f

Tactic:
rw [hg3, ← hu]
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
h : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
g : F[X]
hg1 : Membership.mem (γ := Set F[X]) (nonunits F[X]) g
_hg2 : g ≠ 0
h_1 : g ∣ f
hg4 : g ∣ (derivative : (a : F[X]) → F[X]) f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : (↑u : F[X]) = p
conv_lhs : g * (↑u : F[X]) ∣ (derivative : (a : F[X]) → F[X]) f
⊢ f ∣ (derivative : (a : F[X]) → F[X]) f

Tactic:
conv_lhs => rw [hg3, ← hu]