awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
x : A
p : A[X]
⊢ (d : (a : A) → M) (eval x p) =
    HAdd.hAdd (α := M)
      ((PolynomialModule.eval x : (a : PolynomialModule A M) → M)
          ((d.mapCoeffs : (a : A[X]) → PolynomialModule A M) p : PolynomialModule A M) :
        M)
      (HSMul.hSMul (β := M) (eval x ((derivative : (a : A[X]) → A[X]) p)) ((d : (a : A) → M) x : M))

Tactic:
apply_aeval_eq d x p

Premises used: Polynomial.eval, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Derivation.apply_aeval_eq
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
p : A[X]
i : ℕ
⊢ Eq (α := A) (coeff ((mapCoeffs : (a : A[X]) → A[X]) p) i : A) ((p.coeff i)′ : A)

Tactic:
rfl

Premises used: Polynomial.coeff, rfl
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
n : ℕ
x : A
⊢ Eq (α := A[X]) ((mapCoeffs : (a : A[X]) → A[X]) ((monomial n : (a : A) → A[X]) x) : A[X])
    ((monomial n : (a : A) → A[X]) x′ : A[X])

Tactic:
simp [mapCoeffs]

Premises used: Differential.mapCoeffs
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
⊢ Eq.{u_1 + 1} (α := A[X]) ((mapCoeffs : (a : A[X]) → A[X]) X : A[X]) (0 : A[X])

Tactic:
simp [← monomial_one_one_eq_X]

Premises used: Polynomial.monomial_one_one_eq_X
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
x : A
⊢ Eq (α := A[X]) ((mapCoeffs : (a : A[X]) → A[X]) ((C : (a : A) → A[X]) x) : A[X]) ((C : (a : A) → A[X]) x′ : A[X])

Tactic:
simp [← monomial_zero_left]

Premises used: Polynomial.monomial_zero_left
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ((aeval x : (a : A[X]) → R) p : R)′ =
    HAdd.hAdd (α := R)
      ((PolynomialModule.eval x : (a : PolynomialModule R R) → R)
          ((PolynomialModule.map R (Algebra.linearMap A R) : (a : PolynomialModule A A) → PolynomialModule R R)
              ((Derivation.mapCoeffs deriv : (a : A[X]) → PolynomialModule A A) p) :
            PolynomialModule R R) :
        R)
      (HSMul.hSMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
        (x′ : R))

Tactic:
Derivation.apply_aeval_eq' Differential.deriv _ (Algebra.linearMap A R) ..

Premises used: Algebra.linearMap, Derivation.apply_aeval_eq'
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
x : R
p : A[X]
h :
  Eq.{u_2 + 1} (α := R) ((aeval x : (a : A[X]) → R) ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) : R)
    ((PolynomialModule.eval x : (a : PolynomialModule R R) → R)
        ((PolynomialModule.map R (Algebra.linearMap A R) : (a : PolynomialModule A A) → PolynomialModule R R)
            ((Derivation.mapCoeffs deriv : (a : A[X]) → PolynomialModule A A) p) :
          PolynomialModule R R) :
      R)
convert_7 :
  ∀ (a : A),
    Eq (α := R) ((Algebra.linearMap A R : (a : A) → R) (a′ : A) : R) (((algebraMap A R : (a : A) → R) a : R)′ : R)
⊢ ((aeval x : (a : A[X]) → R) p : R)′ =
    HAdd.hAdd (α := R) ((aeval x : (a : A[X]) → R) ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) : R)
      (HMul.hMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
        (x′ : R))

Tactic:
convert! Derivation.apply_aeval_eq' Differential.deriv _ (Algebra.linearMap A R) ..

Premises used: Algebra.linearMap, Derivation.apply_aeval_eq'
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
x : R
p : A[X]
⊢ Eq.{u_2 + 1} (α := R) ((aeval x : (a : A[X]) → R) ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) : R)
    ((PolynomialModule.eval x : (a : PolynomialModule R R) → R)
        ((PolynomialModule.map R (Algebra.linearMap A R) : (a : PolynomialModule A A) → PolynomialModule R R)
            ((Derivation.mapCoeffs deriv : (a : A[X]) → PolynomialModule A A) p) :
          PolynomialModule R R) :
      R)

Tactic:
simp [mapCoeffs]

Premises used: Differential.mapCoeffs
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ∀ (a : A),
    Eq (α := R) ((Algebra.linearMap A R : (a : A) → R) (a′ : A) : R) (((algebraMap A R : (a : A) → R) a : R)′ : R)

Tactic:
simp [deriv_algebraMap]

Premises used: DifferentialAlgebra.deriv_algebraMap
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
v : A[X]
b : A
⊢ Eq (α := A[X]) ((implicitDeriv v : (a : A[X]) → A[X]) ((C : (a : A) → A[X]) b) : A[X])
    ((C : (a : A) → A[X]) b′ : A[X])

Tactic:
simp [implicitDeriv]

Premises used: Differential.implicitDeriv
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
v : A[X]
⊢ (implicitDeriv v : (a : A[X]) → A[X]) X = v

Tactic:
simp [implicitDeriv]

Premises used: Differential.implicitDeriv
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
x : R
v : A[X]
h : Eq (α := R) (x′ : R) ((aeval x : (a : A[X]) → R) v : R)
p : A[X]
⊢ Eq (α := R) (((aeval x : (a : A[X]) → R) p : R)′ : R)
    ((aeval x : (a : A[X]) → R) ((implicitDeriv v : (a : A[X]) → A[X]) p : A[X]) : R)

Tactic:
simp [deriv_aeval_eq, implicitDeriv, h, mul_comm]

Premises used: Differential.implicitDeriv, Differential.deriv_aeval_eq, mul_comm
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
ha :
  Ne.{u_3 + 1} (α := R')
    (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
      R')
    (0 : R')
h₁ :
  HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      ((f : (a : R) → R') (x′ : R) : R') =
    HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (((f : (a : R) → R') x : R')′ : R')
⊢ Eq (α := R') ((f : (a : R) → R') (x′ : R) : R') (((f : (a : R) → R') x : R')′ : R')

Tactic:
apply mul_left_cancel₀ (a := aeval (f x) (derivative p))

Premises used: mul_left_cancel₀
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
ha :
  Ne.{u_3 + 1} (α := R') ((f.comp (aeval x) : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) : R')
    (0 : R')
⊢ Ne.{u_3 + 1} (α := R')
    (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
      R')
    (0 : R')

Tactic:
rw [Polynomial.aeval_algHom]

Premises used: Polynomial.aeval_algHom
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
ha : ¬Eq.{u_2 + 1} (α := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R) (0 : R)
⊢ Ne.{u_3 + 1} (α := R') ((f.comp (aeval x) : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) : R')
    (0 : R')

Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply, ne_eq, map_eq_zero_iff f hf]

Premises used: ne_eq, AlgHom.coe_comp, map_eq_zero_iff, Function.comp_apply
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ ¬Eq.{u_2 + 1} (α := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R) (0 : R)

Tactic:
apply Separable.aeval_derivative_ne_zero h (minpoly.aeval A x)

Premises used: minpoly.aeval, Polynomial.Separable.aeval_derivative_ne_zero
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
lhs :
  HMul.hMul (α := R') (β := R')
    (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
      R')
    ((f : (a : R) → R') (x′ : R) : R')
| HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      ((f : (a : R) → R') (x′ : R) : R') =
    HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (((f : (a : R) → R') x : R')′ : R')

Tactic:
lhs
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
rw :
  HMul.hMul (α := R') (β := R') ((f.comp (aeval x) : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) : R')
    ((f : (a : R) → R') (x′ : R) : R')
| HMul.hMul (α := R') (β := R')
    (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
      R')
    ((f : (a : R) → R') (x′ : R) : R')

Tactic:
rw [Polynomial.aeval_algHom]

Premises used: Polynomial.aeval_algHom
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
rw :
  HMul.hMul (α := R') (β := R') ((f.comp (aeval x) : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) : R')
    ((f : (a : R) → R') (x′ : R) : R')
| HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      ((f : (a : R) → R') (x′ : R) : R') =
    HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (((f : (a : R) → R') x : R')′ : R')

Tactic:
lhs; rw [Polynomial.aeval_algHom]

Premises used: Polynomial.aeval_algHom
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
h₁ :
  HMul.hMul (α := R') (β := R') ((f.comp (aeval x) : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) : R')
      ((f : (a : R) → R') (x′ : R) : R') =
    HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (((f : (a : R) → R') x : R')′ : R')
⊢ HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      ((f : (a : R) → R') (x′ : R) : R') =
    HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (((f : (a : R) → R') x : R')′ : R')

Tactic:
conv => lhs; rw [Polynomial.aeval_algHom]

Premises used: Polynomial.aeval_algHom
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
h₁ :
  (f : (a : R) → R')
      (HMul.hMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
        (x′ : R)) =
    HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (((f : (a : R) → R') x : R')′ : R')
⊢ HMul.hMul (α := R') (β := R') ((f.comp (aeval x) : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) : R')
      ((f : (a : R) → R') (x′ : R) : R') =
    HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (((f : (a : R) → R') x : R')′ : R')

Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply, ← map_mul]

Premises used: map_mul, AlgHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
h₁ :
  HAdd.hAdd (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) :
        R')
      ((f : (a : R) → R')
          (HMul.hMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
            (x′ : R)) :
        R') =
    HAdd.hAdd (α := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (HMul.hMul (α := R') (β := R')
        (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R')
            ((derivative : (a : A[X]) → A[X]) p : A[X]) :
          R')
        (((f : (a : R) → R') x : R')′ : R'))
⊢ (f : (a : R) → R')
      (HMul.hMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
        (x′ : R)) =
    HMul.hMul (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((derivative : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (((f : (a : R) → R') x : R')′ : R')

Tactic:
apply add_left_cancel (a := aeval (f x) (mapCoeffs p))

Premises used: add_left_cancel
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
h₁ :
  HAdd.hAdd (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) :
        R')
      ((f : (a : R) → R')
          (HMul.hMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
            (x′ : R)) :
        R') =
    (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') p : R')′
⊢ HAdd.hAdd (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) :
        R')
      ((f : (a : R) → R')
          (HMul.hMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
            (x′ : R)) :
        R') =
    HAdd.hAdd (α := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) :
        R')
      (HMul.hMul (α := R') (β := R')
        (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R')
            ((derivative : (a : A[X]) → A[X]) p : A[X]) :
          R')
        (((f : (a : R) → R') x : R')′ : R'))

Tactic:
rw [← deriv_aeval_eq]

Premises used: Differential.deriv_aeval_eq
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ HAdd.hAdd (α := R') (β := R')
      (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) :
        R')
      ((f : (a : R) → R')
          (HMul.hMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
            (x′ : R)) :
        R') =
    (((aeval ((f : (a : R) → R') x) : A[X] →ₐ[A] R') : (a : A[X]) → R') p : R')′

Tactic:
simp only [aeval_algHom, AlgHom.coe_comp, Function.comp_apply, ← map_add, ← deriv_aeval_eq,
    minpoly.aeval, map_zero, p]

Premises used: map_zero, map_add, minpoly.aeval, AlgHom.coe_comp, Differential.deriv_aeval_eq, Function.comp_apply, Polynomial.aeval_algHom
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
f : R ≃ₐ[A] R'
x : R
h : IsSeparable A x
⊢ Eq (α := R') ((f : (a : R) → R') (x′ : R) : R') (((f : (a : R) → R') x : R')′ : R')

Tactic:
haveI := f.nontrivial
  algHom_deriv f.toAlgHom f.injective x h

Premises used: Differential.algHom_deriv, AlgEquiv.toAlgHom, AlgEquiv.injective
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Nontrivial R
inst_12 : Algebra.IsSeparable A R
f : R →ₐ[A] R'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
x : R
⊢ Eq (α := R') ((f : (a : R) → R') (x′ : R) : R') (((f : (a : R) → R') x : R')′ : R')

Tactic:
algHom_deriv f hf x (Algebra.IsSeparable.isSeparable' x)

Premises used: Differential.algHom_deriv, Algebra.IsSeparable.isSeparable'
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
R' : Type u_3
inst_6 : CommRing R'
inst_7 : Differential R'
inst_8 : Algebra A R'
inst_9 : DifferentialAlgebra A R'
inst_10 : IsDomain R'
inst_11 : Algebra.IsSeparable A R
f : R ≃ₐ[A] R'
x : R
⊢ Eq (α := R') ((f : (a : R) → R') (x′ : R) : R') (((f : (a : R) → R') x : R')′ : R')

Tactic:
haveI := f.nontrivial
  algHom_deriv' f.toAlgHom f.injective x

Premises used: AlgEquiv.toAlgHom, Differential.algHom_deriv', AlgEquiv.injective
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
f₁ f₂ : A →ₐ[R] B
e :
  Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x : A
⊢ Membership.mem (α := B) (γ := Submodule R B) (Submodule.restrictScalars R I)
    ((f₁.toLinearMap - f₂.toLinearMap : (a : A) → B) x : B)

Tactic:
simpa [Ideal.Quotient.eq] using congr($e x)

Premises used: Ideal.Quotient.eq
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
f₁ f₂ : A →ₐ[R] B
e :
  Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x : A
⊢ (↑((diffToIdealOfQuotientCompEq I f₁ f₂ e : (a : A) → ↥I) x) : B) =
    HSub.hSub (α := B) (β := B) ((f₁ : (a : A) → B) x : B) ((f₂ : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl