awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun (x : Unit) ↦ f
⊢ ∑ i : Unit, (F i).totalDegree < Fintype.card σ

Tactic:
have : (∑ i : Unit, (F i).totalDegree) < Fintype.card σ := h
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun (x : Unit) ↦ f
this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ
⊢ p ∣
    Fintype.card
      { x : σ → K //
        ∀ (i : Unit),
          Membership.mem (γ := Finset Unit) univ i →
            Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (F i) : K) (0 : K) }

Tactic:
char_dvd_card_solutions_of_sum_lt p this

Premises used: char_dvd_card_solutions_of_sum_lt
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun (x : Unit) ↦ f
this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ
h₁ :
  ∀ (x : σ → K),
    Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) f : K) (0 : K) ↔
      ∀ (i : Unit),
        Membership.mem (γ := Finset Unit) univ i →
          Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (F i) : K) (0 : K)
⊢ p ∣ Fintype.card { x : σ → K // Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) f : K) (0 : K) }

Tactic:
convert! char_dvd_card_solutions_of_sum_lt p this

Premises used: char_dvd_card_solutions_of_sum_lt
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun (x : Unit) ↦ f
this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ
x : σ → K
⊢ Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) f : K) (0 : K) ↔
    ∀ (i : Unit),
      Membership.mem (γ := Finset Unit) univ i →
        Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (F i) : K) (0 : K)

Tactic:
aesop
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun (b : Bool) ↦ bif b then f₂ else f₁
⊢ ∑ b : Bool, (F b).totalDegree < Fintype.card σ

Tactic:
have : (∑ b : Bool, (F b).totalDegree) < Fintype.card σ := (add_comm _ _).trans_lt h
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun (b : Bool) ↦ bif b then f₂ else f₁
this : ∑ b : Bool, (F b).totalDegree < Fintype.card σ
⊢ p ∣
    Fintype.card
      { x : σ → K //
        Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) f₁ : K) (0 : K) ∧
          Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) f₂ : K) (0 : K) }

Tactic:
simpa only [Bool.forall_bool] using char_dvd_card_solutions_of_fintype_sum_lt p this

Premises used: Bool.forall_bool, char_dvd_card_solutions_of_fintype_sum_lt
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
⊢ Eq.{u_1 + 1} (α := R) (logDeriv 0) 0

Tactic:
simp [logDeriv]

Premises used: Differential.logDeriv
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
⊢ Eq.{u_1 + 1} (α := R) (logDeriv 1) 0

Tactic:
simp [logDeriv]

Premises used: Differential.logDeriv
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
unfold : HDiv.hDiv (α := R) ((a * b)′ : R) (a * b) = HDiv.hDiv (α := R) (a′ : R) a + HDiv.hDiv (α := R) (b′ : R) b
⊢ logDeriv (a * b) = logDeriv a + logDeriv b

Tactic:
unfold logDeriv

Premises used: Differential.logDeriv
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
simp :
  HMul.hMul (β := R) a (b′ : R) + HMul.hMul (β := R) b (a′ : R) =
    HMul.hMul (β := R) b (a′ : R) + HMul.hMul (β := R) a (b′ : R)
⊢ HDiv.hDiv (α := R) ((a * b)′ : R) (a * b) = HDiv.hDiv (α := R) (a′ : R) a + HDiv.hDiv (α := R) (b′ : R) b

Tactic:
simp [field]
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ HMul.hMul (β := R) a (b′ : R) + HMul.hMul (β := R) b (a′ : R) =
    HMul.hMul (β := R) b (a′ : R) + HMul.hMul (β := R) a (b′ : R)

Tactic:
ring
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
unfold : HDiv.hDiv (α := R) ((a / b)′ : R) (a / b) = HDiv.hDiv (α := R) (a′ : R) a - HDiv.hDiv (α := R) (b′ : R) b
⊢ logDeriv (a / b) = logDeriv a - logDeriv b

Tactic:
unfold logDeriv

Premises used: Differential.logDeriv
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ HDiv.hDiv (α := R) ((a / b)′ : R) (a / b) = HDiv.hDiv (α := R) (a′ : R) a - HDiv.hDiv (α := R) (b′ : R) b

Tactic:
simp [field, Derivation.leibniz_div]

Premises used: Derivation.leibniz_div
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
⊢ logDeriv (HPow.hPow (β := ℕ) a 0) = (↑0 : R) * logDeriv a

Tactic:
simp
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = (↑n : R) * logDeriv a
succ :
  ∀ (h2 : logDeriv (HPow.hPow (α := R) 0 n) = HMul.hMul (α := R) (↑n : R) (logDeriv 0)),
    logDeriv (HPow.hPow (α := R) 0 (n + 1)) = HMul.hMul (α := R) (↑(n + 1) : R) (logDeriv 0)
succ₁ : ∀ (hb : a ≠ 0), logDeriv (a ^ (n + 1)) = (↑(n + 1) : R) * logDeriv a
⊢ logDeriv (a ^ (n + 1)) = (↑(n + 1) : R) * logDeriv a

Tactic:
obtain rfl | hb := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
n : ℕ
h2 : logDeriv (HPow.hPow (α := R) 0 n) = HMul.hMul (α := R) (↑n : R) (logDeriv 0)
⊢ logDeriv (HPow.hPow (α := R) 0 (n + 1)) = HMul.hMul (α := R) (↑(n + 1) : R) (logDeriv 0)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = (↑n : R) * logDeriv a
hb : a ≠ 0
succ : a ^ n ≠ 0
succ₁ : a ≠ 0
⊢ logDeriv (a ^ (n + 1)) = (↑(n + 1) : R) * logDeriv a

Tactic:
rw [Nat.cast_add, Nat.cast_one, add_mul, one_mul, ← h2, pow_succ, logDeriv_mul]

Premises used: add_mul, pow_succ, Differential.logDeriv_mul, Nat.cast_add, Nat.cast_one, one_mul
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = (↑n : R) * logDeriv a
hb : a ≠ 0
⊢ a ^ n ≠ 0

Tactic:
simp [hb]
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = (↑n : R) * logDeriv a
hb : a ≠ 0
⊢ a ≠ 0

Tactic:
simp [hb]
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
n : ℕ
a : R
zero : logDeriv (HPow.hPow (β := ℕ) a 0) = (↑0 : R) * logDeriv a
succ : ∀ (n : ℕ) (h2 : logDeriv (a ^ n) = (↑n : R) * logDeriv a), logDeriv (a ^ (n + 1)) = (↑(n + 1) : R) * logDeriv a
⊢ logDeriv (a ^ n) = (↑n : R) * logDeriv a

Tactic:
induction n with
  | zero => simp
  | succ n h2 =>
    obtain rfl | hb := eq_or_ne a 0
    · simp
    · rw [Nat.cast_add, Nat.cast_one, add_mul, one_mul, ← h2, pow_succ, logDeriv_mul] <;>
      simp [hb]

Premises used: add_mul, pow_succ, Differential.logDeriv_mul, Nat.cast_add, eq_or_ne, OfNat.ofNat, Nat.cast_one, one_mul, rfl
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
h : logDeriv a = 0
⊢ Eq (α := R) (a′ : R) (0 : R) ∨ a = 0

Tactic:
simp only [logDeriv, _root_.div_eq_zero_iff] at h

Premises used: Differential.logDeriv, div_eq_zero_iff
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
h : Eq (α := R) (a′ : R) (0 : R) ∨ a = 0
inl : ∀ (h : Eq (α := R) (a′ : R) (0 : R)), Eq (α := R) (a′ : R) (0 : R)
inr : ∀ (h : a = 0), Eq (α := R) (a′ : R) (0 : R)
⊢ Eq (α := R) (a′ : R) (0 : R)

Tactic:
rcases h with h|h
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
h : Eq (α := R) (a′ : R) (0 : R)
⊢ Eq (α := R) (a′ : R) (0 : R)

Tactic:
simp [h]
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
h : a = 0
⊢ Eq (α := R) (a′ : R) (0 : R)

Tactic:
simp [h]
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
h : Eq (α := R) (a′ : R) (0 : R)
unfold : HDiv.hDiv (α := R) (a′ : R) a = 0
⊢ logDeriv a = 0

Tactic:
unfold logDeriv at *

Premises used: Differential.logDeriv
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a : R
h : Eq (α := R) (a′ : R) (0 : R)
⊢ HDiv.hDiv (α := R) (a′ : R) a = 0

Tactic:
simp [h]
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
s : Multiset ι
f : ι → R
h : ∀ x ∈ s, f x ≠ 0
empty :
  ∀ (h : ∀ (x : ι), Membership.mem (γ := Multiset ι) 0 x → f x ≠ 0),
    logDeriv (Multiset.map f 0).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) 0)
cons :
  ∀ (a : ι) (s : Multiset ι),
    (∀ (h : ∀ x ∈ s, f x ≠ 0),
        logDeriv (Multiset.map f s).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)) →
      ∀ (h : ∀ x ∈ a ::ₘ s, f x ≠ 0),
        logDeriv (Multiset.map f (a ::ₘ s)).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) (a ::ₘ s))
⊢ logDeriv (Multiset.map f s).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)

Tactic:
induction s using Multiset.induction_on
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
f : ι → R
h : ∀ (x : ι), Membership.mem (γ := Multiset ι) 0 x → f x ≠ 0
⊢ logDeriv (Multiset.map f 0).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) 0)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
f : ι → R
a : ι
s : Multiset ι
h₂ :
  ∀ (h : ∀ x ∈ s, f x ≠ 0),
    logDeriv (Multiset.map f s).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)
h : ∀ x ∈ a ::ₘ s, f x ≠ 0
cons :
  logDeriv (f a * (Multiset.map f s).prod) =
    logDeriv (f a) + Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)
⊢ logDeriv (Multiset.map f (a ::ₘ s)).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) (a ::ₘ s))

Tactic:
simp only [Multiset.map_cons, Multiset.sum_cons, Multiset.prod_cons]

Premises used: Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
f : ι → R
a : ι
s : Multiset ι
h₂ :
  ∀ (h : ∀ x ∈ s, f x ≠ 0),
    logDeriv (Multiset.map f s).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)
h : ∀ x ∈ a ::ₘ s, f x ≠ 0
cons : logDeriv (f a * (Multiset.map f s).prod) = logDeriv (f a) + logDeriv (Multiset.map f s).prod
cons₁ : ∀ x ∈ s, f x ≠ 0
⊢ logDeriv (f a * (Multiset.map f s).prod) =
    logDeriv (f a) + Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)

Tactic:
rw [← h₂]
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
f : ι → R
a : ι
s : Multiset ι
h₂ :
  ∀ (h : ∀ x ∈ s, f x ≠ 0),
    logDeriv (Multiset.map f s).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)
h : ∀ x ∈ a ::ₘ s, f x ≠ 0
cons : f a ≠ 0
cons₁ : (Multiset.map f s).prod ≠ 0
⊢ logDeriv (f a * (Multiset.map f s).prod) = logDeriv (f a) + logDeriv (Multiset.map f s).prod

Tactic:
apply logDeriv_mul

Premises used: Differential.logDeriv_mul
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
f : ι → R
a : ι
s : Multiset ι
h₂ :
  ∀ (h : ∀ x ∈ s, f x ≠ 0),
    logDeriv (Multiset.map f s).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)
h : ∀ x ∈ a ::ₘ s, f x ≠ 0
⊢ f a ≠ 0

Tactic:
simp [h]
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
f : ι → R
a : ι
s : Multiset ι
h₂ :
  ∀ (h : ∀ x ∈ s, f x ≠ 0),
    logDeriv (Multiset.map f s).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)
h : ∀ x ∈ a ::ₘ s, f x ≠ 0
⊢ (Multiset.map f s).prod ≠ 0

Tactic:
simp_all
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
f : ι → R
a : ι
s : Multiset ι
h₂ :
  ∀ (h : ∀ x ∈ s, f x ≠ 0),
    logDeriv (Multiset.map f s).prod = Multiset.sum (Multiset.map (fun (x : ι) ↦ logDeriv (f x)) s)
h : ∀ x ∈ a ::ₘ s, f x ≠ 0
⊢ ∀ x ∈ s, f x ≠ 0

Tactic:
simp_all
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
s : Finset ι
f : ι → R
h : ∀ x ∈ s, f x ≠ 0
⊢ Eq.{u_1 + 1} (α := R) (logDeriv (∏ x ∈ s, f x)) (∑ x ∈ s, logDeriv (f x))

Tactic:
logDeriv_multisetProd _ h

Premises used: Finset.prod, Differential.logDeriv_multisetProd, Finset.sum
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
s : Finset ι
f : ι → R
h : ∀ x ∈ s, f x = 0
unfold :
  HDiv.hDiv (α := R) (β := R) ((∏ x ∈ s, f x)′ : R) (∏ x ∈ s, f x : R) = ∑ x ∈ s, HDiv.hDiv (α := R) ((f x)′ : R) (f x)
⊢ Eq.{u_1 + 1} (α := R) (logDeriv (∏ x ∈ s, f x)) (∑ x ∈ s, logDeriv (f x))

Tactic:
unfold logDeriv

Premises used: Differential.logDeriv
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
ι : Type u_2
s : Finset ι
f : ι → R
h : ∀ x ∈ s, f x = 0
⊢ HDiv.hDiv (α := R) (β := R) ((∏ x ∈ s, f x)′ : R) (∏ x ∈ s, f x : R) = ∑ x ∈ s, HDiv.hDiv (α := R) ((f x)′ : R) (f x)

Tactic:
simp_all
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
F : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
a : F
unfold :
  HDiv.hDiv (α := K) (β := K) (((algebraMap F K : (a : F) → K) a : K)′ : K) ((algebraMap F K : (a : F) → K) a : K) =
    (algebraMap F K : (a : F) → K) (HDiv.hDiv (α := F) (a′ : F) a)
⊢ Eq.{u_3 + 1} (α := K) (logDeriv ((algebraMap F K : (a : F) → K) a) : K)
    ((algebraMap F K : (a : F) → K) (logDeriv a) : K)

Tactic:
unfold logDeriv

Premises used: Differential.logDeriv
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
F : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
a : F
⊢ HDiv.hDiv (α := K) (β := K) (((algebraMap F K : (a : F) → K) a : K)′ : K) ((algebraMap F K : (a : F) → K) a : K) =
    (algebraMap F K : (a : F) → K) (HDiv.hDiv (α := F) (a′ : F) a)

Tactic:
simp [deriv_algebraMap]

Premises used: DifferentialAlgebra.deriv_algebraMap
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
F : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
a : F
⊢ Eq.{u_3 + 1} (α := K) (↑(logDeriv a) : K) (logDeriv (↑a : K))

Tactic:
(logDeriv_algebraMap a).symm

Premises used: Differential.logDeriv_algebraMap, Eq.symm
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
p : F[X]
inst_5 : Fact (Irreducible p)
inst_6 : Fact p.Monic
x : F[X]
hx :
  Eq (α := AdjoinRoot p) (((AdjoinRoot.mk p).toIntAlgHom : (a : F[X]) → AdjoinRoot p) x : AdjoinRoot p)
    (0 : AdjoinRoot p)
simp_all :
  ∀ (hx : p ∣ x),
    p ∣
      (implicitDeriv
            ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
              (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
                (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                  AdjoinRoot p)
                ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                  AdjoinRoot p))) :
          (a : F[X]) → F[X])
        x
⊢ Eq (α := AdjoinRoot p)
    (((AdjoinRoot.mk p).toIntAlgHom : (a : F[X]) → AdjoinRoot p)
        ((implicitDeriv
              ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
                (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
                  (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                    AdjoinRoot p)
                  ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                    AdjoinRoot p))) :
            (a : F[X]) → F[X])
          x) :
      AdjoinRoot p)
    (0 : AdjoinRoot p)

Tactic:
simp_all only [RingHom.toIntAlgHom_apply, AdjoinRoot.mk_eq_zero]

Premises used: RingHom.toIntAlgHom_apply, AdjoinRoot.mk_eq_zero
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
p : F[X]
inst_5 : Fact (Irreducible p)
inst_6 : Fact p.Monic
x : F[X]
hx : p ∣ x
obtain :
  ∀ (q : F[X]),
    p ∣
      (implicitDeriv
            ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
              (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
                (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                  AdjoinRoot p)
                ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                  AdjoinRoot p))) :
          (a : F[X]) → F[X])
        (p * q)
⊢ p ∣
    (implicitDeriv
          ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
            (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
              (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                AdjoinRoot p)
              ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                AdjoinRoot p))) :
        (a : F[X]) → F[X])
      x

Tactic:
obtain ⟨q, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
p : F[X]
inst_5 : Fact (Irreducible p)
inst_6 : Fact p.Monic
q : F[X]
simp :
  p ∣
    HMul.hMul (β := F[X]) p
        ((implicitDeriv
                ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
                  (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
                    (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                      AdjoinRoot p)
                    ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                      AdjoinRoot p))) :
              (a : F[X]) → F[X])
            q :
          F[X]) +
      HMul.hMul (β := F[X]) q
        ((implicitDeriv
                ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
                  (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
                    (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                      AdjoinRoot p)
                    ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                      AdjoinRoot p))) :
              (a : F[X]) → F[X])
            p :
          F[X])
⊢ p ∣
    (implicitDeriv
          ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
            (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
              (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                AdjoinRoot p)
              ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                AdjoinRoot p))) :
        (a : F[X]) → F[X])
      (p * q)

Tactic:
simp only [Derivation.leibniz, smul_eq_mul]

Premises used: Derivation.leibniz, smul_eq_mul
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
p : F[X]
inst_5 : Fact (Irreducible p)
inst_6 : Fact p.Monic
q : F[X]
apply :
  p ∣
    HMul.hMul (β := F[X]) q
      ((implicitDeriv
              ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
                (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
                  (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                    AdjoinRoot p)
                  ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                    AdjoinRoot p))) :
            (a : F[X]) → F[X])
          p :
        F[X])
⊢ p ∣
    HMul.hMul (β := F[X]) p
        ((implicitDeriv
                ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
                  (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
                    (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                      AdjoinRoot p)
                    ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                      AdjoinRoot p))) :
              (a : F[X]) → F[X])
            q :
          F[X]) +
      HMul.hMul (β := F[X]) q
        ((implicitDeriv
                ((AdjoinRoot.modByMonicHom ⋯ : (a : AdjoinRoot p) → F[X])
                  (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
                    (-(aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) :
                      AdjoinRoot p)
                    ((aeval (AdjoinRoot.root p) : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) :
                      AdjoinRoot p))) :
              (a : F[X]) → F[X])
            p :
          F[X])

Tactic:
apply dvd_add (dvd_mul_right ..)

Premises used: dvd_mul_right, dvd_add