awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ (D : (a : K) → M) a⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) a⁻¹ 2) ((D : (a : K) → M) a : M)

Tactic:
D.leibniz_of_mul_eq_one (inv_mul_cancel₀ ha)

Premises used: Derivation.leibniz_of_mul_eq_one, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ (D : (a : K) → M) a⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) a⁻¹ 2) ((D : (a : K) → M) a : M)

Tactic:
exact D.leibniz_of_mul_eq_one (inv_mul_cancel₀ ha)

Premises used: Derivation.leibniz_of_mul_eq_one, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a b : K
simp :
  HSMul.hSMul (β := M) b⁻¹ ((D : (a : K) → M) a : M) +
      -HSMul.hSMul (β := M) (a * (HPow.hPow (β := ℕ) b 2)⁻¹) ((D : (a : K) → M) b : M) =
    HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * b) ((D : (a : K) → M) a : M) +
      -HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * a) ((D : (a : K) → M) b : M)
⊢ (D : (a : K) → M) (a / b) =
    HPow.hPow (β := ℕ) b⁻¹ 2 •
      (HSMul.hSMul (β := M) b ((D : (a : K) → M) a : M) - HSMul.hSMul (β := M) a ((D : (a : K) → M) b : M))

Tactic:
simp only [div_eq_mul_inv, leibniz, leibniz_inv, inv_pow, neg_smul, smul_neg, smul_smul, add_comm,
    sub_eq_add_neg, smul_add]

Premises used: neg_smul, sub_eq_add_neg, Derivation.leibniz_inv, smul_smul, smul_neg, inv_pow, div_eq_mul_inv, add_comm, Derivation.leibniz, smul_add
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a b : K
rw :
  HSMul.hSMul (β := M) (b * b⁻¹ * b⁻¹) ((D : (a : K) → M) a : M) +
      -HSMul.hSMul (β := M) (a * (HPow.hPow (β := ℕ) b 2)⁻¹) ((D : (a : K) → M) b : M) =
    HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * b) ((D : (a : K) → M) a : M) +
      -HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * a) ((D : (a : K) → M) b : M)
⊢ HSMul.hSMul (β := M) b⁻¹ ((D : (a : K) → M) a : M) +
      -HSMul.hSMul (β := M) (a * (HPow.hPow (β := ℕ) b 2)⁻¹) ((D : (a : K) → M) b : M) =
    HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * b) ((D : (a : K) → M) a : M) +
      -HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * a) ((D : (a : K) → M) b : M)

Tactic:
rw [← inv_mul_mul_self b⁻¹, inv_inv]

Premises used: inv_mul_mul_self, Inv.inv, inv_inv
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a b : K
⊢ HSMul.hSMul (β := M) (b * b⁻¹ * b⁻¹) ((D : (a : K) → M) a : M) +
      -HSMul.hSMul (β := M) (a * (HPow.hPow (β := ℕ) b 2)⁻¹) ((D : (a : K) → M) b : M) =
    HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * b) ((D : (a : K) → M) a : M) +
      -HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * a) ((D : (a : K) → M) b : M)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a b : K
h : Eq.{u_3 + 1} (α := M) ((D : (a : K) → M) b : M) (0 : M)
simp :
  HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * b) ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) b⁻¹ ((D : (a : K) → M) a : M)
⊢ (D : (a : K) → M) (a / b) = HSMul.hSMul (β := M) b⁻¹ ((D : (a : K) → M) a : M)

Tactic:
simp only [leibniz_div, inv_pow, h, smul_zero, sub_zero, smul_smul]

Premises used: sub_zero, Derivation.leibniz_div, smul_zero, smul_smul, inv_pow
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a b : K
h : Eq.{u_3 + 1} (α := M) ((D : (a : K) → M) b : M) (0 : M)
rw :
  HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * b) ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) (b⁻¹ * b⁻¹ * b) ((D : (a : K) → M) a : M)
⊢ HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * b) ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) b⁻¹ ((D : (a : K) → M) a : M)

Tactic:
rw [← mul_self_mul_inv b⁻¹, inv_inv]

Premises used: mul_self_mul_inv, Inv.inv, inv_inv
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a b : K
h : Eq.{u_3 + 1} (α := M) ((D : (a : K) → M) b : M) (0 : M)
⊢ HSMul.hSMul (β := M) ((HPow.hPow (β := ℕ) b 2)⁻¹ * b) ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) (b⁻¹ * b⁻¹ * b) ((D : (a : K) → M) a : M)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
pos : ∀ (hn : n = 0), (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
neg : ∀ (hn : ¬n = 0), (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : n = 0
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
pos : ∀ (ha : a = 0), (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
neg : ∀ (ha : ¬a = 0), (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : a = 0
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)

Tactic:
simp [ha, zero_zpow n hn]

Premises used: zero_zpow
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
neg :
  ∀ (h : n = (↑n.natAbs : ℤ)),
    (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
neg₁ :
  ∀ (h : n = -(↑n.natAbs : ℤ)),
    (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)

Tactic:
rcases Int.natAbs_eq n with h | h

Premises used: Int.natAbs_eq
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = (↑n.natAbs : ℤ)
neg :
  (D : (a : K) → M) (HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ)) =
    HSMul.hSMul (α := ℤ) (↑n.natAbs : ℤ)
      (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1) ((D : (a : K) → M) a : M))
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = (↑n.natAbs : ℤ)
neg :
  n.natAbs • HSMul.hSMul (β := M) (a ^ (n.natAbs - 1)) ((D : (a : K) → M) a : M) =
    n.natAbs • HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1) ((D : (a : K) → M) a : M)
⊢ (D : (a : K) → M) (HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ)) =
    HSMul.hSMul (α := ℤ) (↑n.natAbs : ℤ)
      (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1) ((D : (a : K) → M) a : M))

Tactic:
simp only [zpow_natCast, leibniz_pow, natCast_zsmul]

Premises used: zpow_natCast, Derivation.leibniz_pow, natCast_zsmul
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = (↑n.natAbs : ℤ)
neg :
  n.natAbs • HSMul.hSMul (β := M) (HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ)) ((D : (a : K) → M) a : M) =
    n.natAbs • HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1) ((D : (a : K) → M) a : M)
⊢ n.natAbs • HSMul.hSMul (β := M) (a ^ (n.natAbs - 1)) ((D : (a : K) → M) a : M) =
    n.natAbs • HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1) ((D : (a : K) → M) a : M)

Tactic:
rw [← zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = (↑n.natAbs : ℤ)
neg : (↑(n.natAbs - 1) : ℤ) = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1
⊢ n.natAbs • HSMul.hSMul (β := M) (HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ)) ((D : (a : K) → M) a : M) =
    n.natAbs • HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1) ((D : (a : K) → M) a : M)

Tactic:
congr
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = (↑n.natAbs : ℤ)
⊢ (↑(n.natAbs - 1) : ℤ) = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -(↑n.natAbs : ℤ)
neg :
  HSMul.hSMul (β := M)
      (-(HPow.hPow (β := ℤ) a (↑(n.natAbs * 2) : ℤ))⁻¹ * (↑n.natAbs : K) * HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ))
      ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) ((↑(-(↑n.natAbs : ℤ)) : K) * a ^ HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1)
      ((D : (a : K) → M) a : M)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)

Tactic:
rw [h, zpow_neg, zpow_natCast, leibniz_inv, leibniz_pow, inv_pow, ← pow_mul, ← zpow_natCast,
      ← zpow_natCast, ← Nat.cast_smul_eq_nsmul K, ← Int.cast_smul_eq_zsmul K, smul_smul, smul_smul,
      smul_smul]

Premises used: zpow_natCast, Derivation.leibniz_inv, smul_smul, inv_pow, pow_mul, zpow_neg, Derivation.leibniz_pow, Nat.cast_smul_eq_nsmul, Int.cast_smul_eq_zsmul
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -(↑n.natAbs : ℤ)
trans :
  HSMul.hSMul (β := M)
      (-(HPow.hPow (β := ℤ) a (↑(n.natAbs * 2) : ℤ))⁻¹ * (↑n.natAbs : K) * HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ))
      ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M)
      (-(↑n.natAbs : K) * (HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ) / HPow.hPow (β := ℤ) a (↑(n.natAbs * 2) : ℤ)))
      ((D : (a : K) → M) a : M)
trans₁ :
  HSMul.hSMul (β := M)
      (-(↑n.natAbs : K) * (HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ) / HPow.hPow (β := ℤ) a (↑(n.natAbs * 2) : ℤ)))
      ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) ((↑(-(↑n.natAbs : ℤ)) : K) * a ^ HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1)
      ((D : (a : K) → M) a : M)
⊢ HSMul.hSMul (β := M)
      (-(HPow.hPow (β := ℤ) a (↑(n.natAbs * 2) : ℤ))⁻¹ * (↑n.natAbs : K) * HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ))
      ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) ((↑(-(↑n.natAbs : ℤ)) : K) * a ^ HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1)
      ((D : (a : K) → M) a : M)

Tactic:
trans (-n.natAbs * (a ^ ((n.natAbs - 1 : ℕ) : ℤ) / (a ^ ((n.natAbs * 2 : ℕ) : ℤ)))) • D a

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.cast, HPow.hPow, Int.natAbs, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -(↑n.natAbs : ℤ)
⊢ HSMul.hSMul (β := M)
      (-(HPow.hPow (β := ℤ) a (↑(n.natAbs * 2) : ℤ))⁻¹ * (↑n.natAbs : K) * HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ))
      ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M)
      (-(↑n.natAbs : K) * (HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ) / HPow.hPow (β := ℤ) a (↑(n.natAbs * 2) : ℤ)))
      ((D : (a : K) → M) a : M)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -(↑n.natAbs : ℤ)
rw :
  HSMul.hSMul (β := M) (-(↑n.natAbs : K) * a ^ HSub.hSub (α := ℤ) (↑(n.natAbs - 1) : ℤ) (↑(n.natAbs * 2) : ℤ))
      ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) ((↑(-(↑n.natAbs : ℤ)) : K) * a ^ HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1)
      ((D : (a : K) → M) a : M)
⊢ HSMul.hSMul (β := M)
      (-(↑n.natAbs : K) * (HPow.hPow (β := ℤ) a (↑(n.natAbs - 1) : ℤ) / HPow.hPow (β := ℤ) a (↑(n.natAbs * 2) : ℤ)))
      ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) ((↑(-(↑n.natAbs : ℤ)) : K) * a ^ HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1)
      ((D : (a : K) → M) a : M)

Tactic:
rw [← zpow_sub₀ ha]

Premises used: zpow_sub₀
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -(↑n.natAbs : ℤ)
e_a : Eq.{u_4 + 1} (α := K) (-(↑n.natAbs : K)) (↑(-(↑n.natAbs : ℤ)) : K)
e_a₁ : HSub.hSub (α := ℤ) (↑(n.natAbs - 1) : ℤ) (↑(n.natAbs * 2) : ℤ) = HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1
⊢ HSMul.hSMul (β := M) (-(↑n.natAbs : K) * a ^ HSub.hSub (α := ℤ) (↑(n.natAbs - 1) : ℤ) (↑(n.natAbs * 2) : ℤ))
      ((D : (a : K) → M) a : M) =
    HSMul.hSMul (β := M) ((↑(-(↑n.natAbs : ℤ)) : K) * a ^ HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1)
      ((D : (a : K) → M) a : M)

Tactic:
congr 3
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -(↑n.natAbs : ℤ)
e_a e_a₁ e_a₂ e_a₃ : Eq.{u_4 + 1} (α := K) (↑(-|n|) : K) (↑(-|n|) : K)
⊢ Eq.{u_4 + 1} (α := K) (-(↑n.natAbs : K)) (↑(-(↑n.natAbs : ℤ)) : K)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
K : Type u_4
inst_3 : Field K
inst_4 : Module K M
inst_5 : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -(↑n.natAbs : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(n.natAbs - 1) : ℤ) (↑(n.natAbs * 2) : ℤ) = HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D_1 D1 D2 : Derivation R A M
r : R
a_1 b_1 : A
D : Derivation R A M
a b : A
⊢ (-(↑D : A →ₗ[R] M) : (a : A) → M) (a * b) =
    HSMul.hSMul (β := M) a ((-(↑D : A →ₗ[R] M) : (a : A) → M) b : M) +
      HSMul.hSMul (β := M) b ((-(↑D : A →ₗ[R] M) : (a : A) → M) a : M)

Tactic:
simp only [LinearMap.neg_apply, smul_neg, neg_add_rev, leibniz, coeFn_coe, add_comm]

Premises used: neg_add_rev, LinearMap.neg_apply, smul_neg, add_comm, Derivation.leibniz, Derivation.coeFn_coe
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
⊢ Eq (α := (a : A) → M) (⇑(-D) : (a : A) → M) (-(⇑D : (a : A) → M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
⊢ (↑(-D) : A →ₗ[R] M) = -(↑D : A →ₗ[R] M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
⊢ Eq.{u_3 + 1} (α := M) ((-D : (a : A) → M) a : M) (-(D : (a : A) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D D1_1 D2_1 : Derivation R A M
r : R
a_1 b_1 : A
D1 D2 : Derivation R A M
a b : A
⊢ ((↑D1 : A →ₗ[R] M) - (↑D2 : A →ₗ[R] M) : (a : A) → M) (a * b) =
    HSMul.hSMul (β := M) a (((↑D1 : A →ₗ[R] M) - (↑D2 : A →ₗ[R] M) : (a : A) → M) b : M) +
      HSMul.hSMul (β := M) b (((↑D1 : A →ₗ[R] M) - (↑D2 : A →ₗ[R] M) : (a : A) → M) a : M)

Tactic:
simp only [LinearMap.sub_apply, leibniz, coeFn_coe, smul_sub, add_sub_add_comm]

Premises used: Derivation.leibniz, smul_sub, Derivation.coeFn_coe, add_sub_add_comm, LinearMap.sub_apply
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D1 D2 : Derivation R A M
⊢ (⇑(D1 - D2) : (a : A) → M) = HSub.hSub (α := (a : A) → M) (⇑D1 : (a : A) → M) (⇑D2 : (a : A) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D1 D2 : Derivation R A M
⊢ (↑(D1 - D2) : A →ₗ[R] M) = (↑D1 : A →ₗ[R] M) - (↑D2 : A →ₗ[R] M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
D1 D2 : Derivation R A M
a : A
⊢ (D1 - D2 : (a : A) → M) a = HSub.hSub (α := M) (β := M) ((D1 : (a : A) → M) a : M) ((D2 : (a : A) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.DifferentialRing
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Differential A
inst_4 : Differential B
inst_5 : DifferentialAlgebra A B
a : A
⊢ Eq.{u_2 + 1} (α := B) ((↑(a′ : A) : B) : B) ((↑a : B)′ : B)

Tactic:
(DifferentialAlgebra.deriv_algebraMap _).symm

Premises used: DifferentialAlgebra.deriv_algebraMap, Eq.symm
-- Module: Mathlib.RingTheory.Derivation.DifferentialRing
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Differential B
inst_4 : Differential.ContainConstants A B
x : B
h : Eq (α := B) (x′ : B) (0 : B)
⊢ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A B)) x

Tactic:
Differential.ContainConstants.mem_range_of_deriv_eq_zero h

Premises used: Differential.ContainConstants.mem_range_of_deriv_eq_zero
-- Module: Mathlib.RingTheory.Derivation.DifferentialRing
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommRing R
inst_1 : CommRing R₂
inst_2 : Differential R₂
h : R ≃+* R₂
⊢ ∀ (a b : R),
    (h.symm.toAddMonoidHom.toIntLinearMap ∘ₗ (↑deriv : R₂ →ₗ[ℤ] R₂) ∘ₗ h.toAddMonoidHom.toIntLinearMap : (a : R) → R)
        (a * b) =
      HSMul.hSMul (β := R) a
          ((h.symm.toAddMonoidHom.toIntLinearMap ∘ₗ (↑deriv : R₂ →ₗ[ℤ] R₂) ∘ₗ h.toAddMonoidHom.toIntLinearMap :
                (a : R) → R)
              b :
            R) +
        HSMul.hSMul (β := R) b
          ((h.symm.toAddMonoidHom.toIntLinearMap ∘ₗ (↑deriv : R₂ →ₗ[ℤ] R₂) ∘ₗ h.toAddMonoidHom.toIntLinearMap :
                (a : R) → R)
              a :
            R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.DifferentialRing
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
R₂ : Type u_3
inst_2 : CommRing R
inst_3 : CommRing R₂
inst_4 : Differential R₂
inst_5 : Algebra A R
inst_6 : Algebra A R₂
inst_7 : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
change :
  Eq (α := R)
    ((h.toRingEquiv.symm.toAddMonoidHom.toIntLinearMap ∘ₗ
            (↑Differential.deriv : R₂ →ₗ[ℤ] R₂) ∘ₗ h.toRingEquiv.toAddMonoidHom.toIntLinearMap :
          (a : R) → R)
        ((algebraMap A R : (a : A) → R) a : R) :
      R)
    ((algebraMap A R : (a : A) → R) (a′ : A) : R)
⊢ Eq (α := R) (((algebraMap A R : (a : A) → R) a : R)′ : R) ((algebraMap A R : (a : A) → R) (a′ : A) : R)

Tactic:
change (LinearMap.comp ..) _ = _

Premises used: LinearMap.comp, DFunLike.coe