awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
h :
  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
⊢ 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])

Tactic:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- 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]
h :
  Eq (α := AdjoinRoot p)
    ((AdjoinRoot.mk p : (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])
          p) :
      AdjoinRoot p)
    (0 : AdjoinRoot p)
⊢ 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

Tactic:
rw [← AdjoinRoot.mk_eq_zero]

Premises used: 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
q : F[X]
h :
  HAdd.hAdd (α := AdjoinRoot p)
      ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) : AdjoinRoot p)
      (HMul.hMul (β := AdjoinRoot p)
        (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
          (-(AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) : AdjoinRoot p)
          ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) : AdjoinRoot p))
        ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) : AdjoinRoot p)) =
    0
⊢ Eq (α := AdjoinRoot p)
    ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p)
        ((mapCoeffs +
              HSMul.hSMul (α := F[X]) (β := Derivation ℤ F[X] F[X])
                ((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)) :
                  F[X])
                (Derivation.restrictScalars ℤ derivative') :
            (a : F[X]) → F[X])
          p) :
      AdjoinRoot p)
    (0 : AdjoinRoot p)

Tactic:
simp only [AdjoinRoot.aeval_eq, Derivation.coe_add, Derivation.coe_smul, Pi.add_apply,
        Pi.smul_apply, Derivation.restrictScalars_apply, derivative'_apply, smul_eq_mul, map_add,
        map_mul, AdjoinRoot.mk_leftInverse Fact.out _]

Premises used: Derivation.coe_add, Polynomial.derivative'_apply, AdjoinRoot.mk_leftInverse, map_add, Derivation.restrictScalars_apply, Pi.add_apply, map_mul, Derivation.coe_smul, AdjoinRoot.aeval_eq, smul_eq_mul, Fact.out, Pi.smul_apply
-- 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]
h :
  Ne (α := AdjoinRoot p)
    ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) : AdjoinRoot p)
    (0 : AdjoinRoot p)
⊢ HAdd.hAdd (α := AdjoinRoot p)
      ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) : AdjoinRoot p)
      (HMul.hMul (β := AdjoinRoot p)
        (HDiv.hDiv (α := AdjoinRoot p) (β := AdjoinRoot p)
          (-(AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((mapCoeffs : (a : F[X]) → F[X]) p) : AdjoinRoot p)
          ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) : AdjoinRoot p))
        ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) : AdjoinRoot p)) =
    0

Tactic:
rw [div_mul_cancel₀, add_neg_cancel]

Premises used: add_neg_cancel, div_mul_cancel₀
-- 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]
h : ¬p ∣ (derivative : (a : F[X]) → F[X]) p
⊢ Ne (α := AdjoinRoot p)
    ((AdjoinRoot.mk p : (a : F[X]) → AdjoinRoot p) ((derivative : (a : F[X]) → F[X]) p) : AdjoinRoot p)
    (0 : AdjoinRoot p)

Tactic:
simp only [ne_eq, AdjoinRoot.mk_eq_zero]

Premises used: AdjoinRoot.mk_eq_zero, ne_eq
-- 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]
⊢ 0 < p.natDegree

Tactic:
have : 0 < p.natDegree := Irreducible.natDegree_pos (Fact.out)
-- 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]
this : 0 < p.natDegree
h : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) p : F[X]) (0 : F[X])
h₁ : natDegree.{u_2} (R := F) ((derivative : (a : F[X]) → F[X]) p) < p.natDegree
⊢ ¬p ∣ (derivative : (a : F[X]) → F[X]) p

Tactic:
apply not_dvd_of_natDegree_lt

Premises used: Polynomial.not_dvd_of_natDegree_lt
-- 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]
this : 0 < p.natDegree
nh : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) p : F[X]) (0 : F[X])
⊢ False

Tactic:
simp [natDegree_eq_zero_of_derivative_eq_zero nh] at this

Premises used: Polynomial.natDegree_eq_zero_of_derivative_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
q : F[X]
this : 0 < p.natDegree
h : p.natDegree ≠ 0
⊢ natDegree.{u_2} (R := F) ((derivative : (a : F[X]) → F[X]) p) < p.natDegree

Tactic:
apply natDegree_derivative_lt

Premises used: Polynomial.natDegree_derivative_lt
-- 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]
this : 0 < p.natDegree
⊢ p.natDegree ≠ 0

Tactic:
Nat.ne_zero_of_lt this

Premises used: Nat.ne_zero_of_lt
-- 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]
this : 0 < p.natDegree
⊢ p.natDegree ≠ 0

Tactic:
exact Nat.ne_zero_of_lt this

Premises used: Nat.ne_zero_of_lt
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 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
a : F
change :
  Eq (α := AdjoinRoot p)
    ((Derivation.liftOfSurjective ⋯ (d :=
            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 : AdjoinRoot p) → AdjoinRoot p)
        (((AdjoinRoot.mk p).toIntAlgHom : (a : F[X]) → AdjoinRoot p) ((C : (a : F) → F[X]) a)) :
      AdjoinRoot p)
    ((algebraMap F (AdjoinRoot p) : (a : F) → AdjoinRoot p) a′ : AdjoinRoot p)
⊢ Eq (α := AdjoinRoot p) (((algebraMap F (AdjoinRoot p) : (a : F) → AdjoinRoot p) a)′ : AdjoinRoot p)
    ((algebraMap F (AdjoinRoot p) : (a : F) → AdjoinRoot p) a′ : AdjoinRoot p)

Tactic:
change (Derivation.liftOfSurjective _ _) ((AdjoinRoot.mk p).toIntAlgHom (C a)) = _

Premises used: Polynomial.C, RingHom.toIntAlgHom, Derivation.liftOfSurjective, AdjoinRoot.mk, DFunLike.coe
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 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
a : F
rw :
  Eq (α := AdjoinRoot p)
    (((AdjoinRoot.mk p).toIntAlgHom : (a : F[X]) → AdjoinRoot p) ((C : (a : F) → F[X]) a′) : AdjoinRoot p)
    ((algebraMap F (AdjoinRoot p) : (a : F) → AdjoinRoot p) a′ : AdjoinRoot p)
⊢ Eq (α := AdjoinRoot p)
    ((Derivation.liftOfSurjective ⋯ (d :=
            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 : AdjoinRoot p) → AdjoinRoot p)
        (((AdjoinRoot.mk p).toIntAlgHom : (a : F[X]) → AdjoinRoot p) ((C : (a : F) → F[X]) a)) :
      AdjoinRoot p)
    ((algebraMap F (AdjoinRoot p) : (a : F) → AdjoinRoot p) a′ : AdjoinRoot p)

Tactic:
rw [Derivation.liftOfSurjective_apply, implicitDeriv_C]

Premises used: Differential.implicitDeriv_C, Derivation.liftOfSurjective_apply
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 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
a : F
⊢ Eq (α := AdjoinRoot p)
    (((AdjoinRoot.mk p).toIntAlgHom : (a : F[X]) → AdjoinRoot p) ((C : (a : F) → F[X]) a′) : AdjoinRoot p)
    ((algebraMap F (AdjoinRoot p) : (a : F) → AdjoinRoot p) a′ : AdjoinRoot p)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
F : Type u_2
inst : Field F
inst_1 : Differential F
inst_2 : CharZero F
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : FiniteDimensional F K
k : K := Exists.choose (p := fun (α : K) ↦ Eq (α := IntermediateField F K) F⟮α⟯ ⊤) ⋯
⊢ Eq (α := IntermediateField F K) F⟮k⟯ ⊤

Tactic:
haveI h : F⟮k⟯ = ⊤ := (Field.exists_primitive_element F K).choose_spec
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
F : Type u_2
inst : Field F
inst_1 : Differential F
inst_2 : CharZero F
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : FiniteDimensional F K
k : K := Exists.choose (p := fun (α : K) ↦ Eq (α := IntermediateField F K) F⟮α⟯ ⊤) ⋯
h : Eq (α := IntermediateField F K) F⟮k⟯ ⊤
⊢ Fact (Monic (minpoly F k))

Tactic:
haveI : Fact (minpoly F k).Monic := ⟨minpoly.monic (IsAlgebraic.of_finite ..).isIntegral⟩
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
F : Type u_2
inst : Field F
inst_1 : Differential F
inst_2 : CharZero F
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : FiniteDimensional F K
k : K := Exists.choose (p := fun (α : K) ↦ Eq (α := IntermediateField F K) F⟮α⟯ ⊤) ⋯
h : Eq (α := IntermediateField F K) F⟮k⟯ ⊤
this : Fact (Monic (minpoly F k))
⊢ Fact (Irreducible (M := F[X]) (minpoly F k))

Tactic:
haveI : Fact (Irreducible (minpoly F k)) :=
    ⟨minpoly.irreducible (IsAlgebraic.of_finite ..).isIntegral⟩
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
F : Type u_2
inst : Field F
inst_1 : Differential F
inst_2 : CharZero F
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : FiniteDimensional F K
k : K := Exists.choose (p := fun (α : K) ↦ Eq (α := IntermediateField F K) F⟮α⟯ ⊤) ⋯
h : Eq (α := IntermediateField F K) F⟮k⟯ ⊤
this_1 : Fact (Monic (minpoly F k))
this : Fact (Irreducible (M := F[X]) (minpoly F k))
⊢ DifferentialAlgebra F K

Tactic:
apply DifferentialAlgebra.equiv

Premises used: DifferentialAlgebra.equiv
-- 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
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
refine :
  ∀ (x : { _a : Differential K // DifferentialAlgebra F K }) (a : Differential K) (ha : DifferentialAlgebra F K),
    Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) a ha = Inhabited.default
⊢ Unique { _a : Differential K // DifferentialAlgebra F K }

Tactic:
refine ⟨⟨default⟩, fun ⟨a, ha⟩ ↦ ?_⟩
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
a₁ : ∀ (x : K), Eq (α := K) (x′ : K) (x′ : K)
⊢ Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) a ha = Inhabited.default

Tactic:
ext x
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
a₁ :
  Eq.{u_3 + 1} (α := K)
    ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′)
    ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′)
a₂ :
  Function.Injective (β := K) fun (x_2 : K) ↦
    HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
      (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K) x_2)
⊢ Eq (α := K) (x′ : K) (x′ : K)

Tactic:
apply_fun (aeval x (mapCoeffs (minpoly F x)) + aeval x (derivative (minpoly F x)) * ·)

Premises used: Polynomial.derivative, HMul.hMul, minpoly, HAdd.hAdd, Polynomial.aeval, DFunLike.coe, Differential.mapCoeffs
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
a₁ :
  Eq.{u_3 + 1} (α := K) (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
    ((fun (x_2 : K) ↦
          HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
              x_2))
        x′ :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′)
    ((fun (x_2 : K) ↦
        HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
          (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            x_2))
      x′)

Tactic:
conv_lhs => apply (deriv_aeval_eq ..).symm

Premises used: Differential.deriv_aeval_eq, Eq.symm
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
a₁ :
  Eq.{u_3 + 1} (α := K) (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
    (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
⊢ Eq.{u_3 + 1} (α := K) (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
    ((fun (x_2 : K) ↦
          HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
            (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
              x_2))
        x′ :
      K)

Tactic:
conv_rhs => apply (@deriv_aeval_eq _ _ _ _ _ default.1 _ default.2 _ _).symm

Premises used: Differential.deriv_aeval_eq, Eq.symm
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Eq.{u_3 + 1} (α := K) (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)
    (((aeval x : (a : F[X]) → K) (minpoly F x) : K)′ : K)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
a₁ :
  Function.Injective (α := K)
    (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K))
⊢ Function.Injective (β := K) fun (x_2 : K) ↦
    HAdd.hAdd (α := K) ((aeval x : (a : F[X]) → K) ((mapCoeffs : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K)
      (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K) x_2)

Tactic:
apply (add_right_injective _).comp

Premises used: add_right_injective, Function.Injective.comp
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
a₁ :
  Ne.{u_3 + 1} (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K) (0 : K)
⊢ Function.Injective (α := K)
    (HMul.hMul (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K))

Tactic:
apply mul_right_injective₀

Premises used: mul_right_injective₀
-- Module: Mathlib.FieldTheory.Differential.Basic
Goal:
R : Type u_1
inst : Field R
inst_1 : Differential R
a_1 b : R
F : Type u_2
inst_2 : Field F
inst_3 : Differential F
inst_4 : CharZero F
K : Type u_3
inst_5 : Field K
inst_6 : Algebra F K
inst_7 : FiniteDimensional F K
default : { _a : Differential K // DifferentialAlgebra F K } :=
  Subtype.mk (p := fun (_a : Differential K) ↦ DifferentialAlgebra F K) (differentialFiniteDimensional F K) ⋯
x_1 : { _a : Differential K // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
a₁ : ¬Dvd.dvd (α := F[X]) (minpoly F x) ((derivative : (a : F[X]) → F[X]) (minpoly F x))
⊢ Ne.{u_3 + 1} (α := K) ((aeval x : (a : F[X]) → K) ((derivative : (a : F[X]) → F[X]) (minpoly F x) : F[X]) : K) (0 : K)

Tactic:
rw [ne_eq, ← minpoly.dvd_iff]

Premises used: minpoly.dvd_iff, ne_eq