awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable.{u} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X]))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
have rw : ∀ {y : ι}
  (hfs :
    (HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f y) : R[X])) 2 *
        ∏ x ∈ (s.erase x).erase y, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f x) : R[X])).Separable)
  (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) (hxy : ¬x = y), False
Tactic: rw [← insert_erase hx, prod_insert (notMem_erase _ _), ←
    insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (notMem_erase _ _), ←
    mul_assoc, hfxy, ← sq] at hfs
Cleared hypotheses: hfs, y, hx, hy, hfxy, hxy
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable.{u} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X]))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
⊢ x = y
have by_contra : ¬x = y → False
Tactic: classical
  by_contra hxy
  rw [← insert_erase hx, prod_insert (notMem_erase _ _), ←
    insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (notMem_erase _ _), ←
    mul_assoc, hfxy, ← sq] at hfs
  cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable.{u} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X]))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
by_contra by_contra₁ by_contra₂ : ∀ (hxy : ¬x = y), False
⊢ x = y
have by_contra₃ : ∀ {y : ι}
  (hfs :
    (HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f y) : R[X])) 2 *
        ∏ x ∈ (s.erase x).erase y, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f x) : R[X])).Separable)
  (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) (hxy : ¬x = y), False
Tactic: classical
  by_contra hxy
  rw [← insert_erase hx, prod_insert (notMem_erase _ _), ←
    insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (notMem_erase _ _), ←
    mul_assoc, hfxy, ← sq] at hfs
  cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2
Cleared hypotheses: hfs, y, hx, hy, hfxy
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
s : 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])) s))
⊢ s.Nodup
have rw : ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t
Tactic: rw [Multiset.nodup_iff_ne_cons_cons]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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)))
⊢ False
have 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))
Tactic: refine not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])).Separable
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])).Separable
have 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
Tactic: rcases n.eq_zero_or_pos with (rfl | hpos)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (↑u : R) : R[X])).Separable
have inr : ∀ (hpos : n > 0), (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)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit.{u} (M := R) (↑n : R)
h : Nontrivial R
hpos : n > 0
⊢ ∃ (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
have 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
Tactic: obtain ⟨n', hn'⟩ := hn.exists_left_inv
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
have 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
Tactic: refine ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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])
        (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
have 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
Tactic: rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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)) =
    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))
have 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))
Tactic: simp only [C.map_mul, C_eq_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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 *
        ((C : (a : R) → R[X]) (↑n : R) * HPow.hPow (α := R[X]) X (n - 1)) =
    1
have 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))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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))
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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])
⊢ f.Separable
have obtain : ∀ (e : R) (hb : e * b = 1), f.Separable
Tactic: obtain ⟨e, hb⟩ := hb.exists_left_inv
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
have 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
Tactic: refine ⟨-derivative f, f + C e, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ 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
have hderiv : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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])
⊢ 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
have 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
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have 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
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have 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
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have 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
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have 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
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]