awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 b : A
h : a * b = 1
rw :
  a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    a • (HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M))
⊢ a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M)
have rw₁ : a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
  a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M)
Tactic: rw [leibniz, smul_add, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 b : A
h : a * b = 1
rw :
  a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    a • (HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M))
rw₁ :
  a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M)
⊢ a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M)
have rw₂ : a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) =
  a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) + a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M)
Tactic: rw [leibniz, smul_add, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 b : A
h : a * b = 1
⊢ HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M) = 0
have rw : HSMul.hSMul (β := M) a ((D : (a : A) → M) 1 : M) = 0
Tactic: rw [h, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 b : A
h : a * b = 1
rw : HSMul.hSMul (β := M) a ((D : (a : A) → M) 1 : M) = 0
⊢ HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M) = 0
have rw₁ : HSMul.hSMul (β := M) a 0 = 0
Tactic: rw [h, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 b : A
h : a * b = 1
rw : HSMul.hSMul (β := M) a ((D : (a : A) → M) 1 : M) = 0
rw₁ : HSMul.hSMul (β := M) a 0 = 0
⊢ HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M) = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [h, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 b : A
h : a * b = 1
⊢ HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    0
have D₁ : HAdd.hAdd (α := M) ((D : (a : A) → M) a : M) (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
  a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M)
Tactic: calc
    D a + a ^ 2 • D b = a • b • D a + a • a • D b := by simp only [smul_smul, h, one_smul, sq]
    _ = a • D (a * b) := by rw [leibniz, smul_add, add_comm]
    _ = 0 := by rw [h, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 b : A
h : a * b = 1
D₁ :
  HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M)
⊢ HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    0
have D₂ : a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
  HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M)
Tactic: calc
    D a + a ^ 2 • D b = a • b • D a + a • a • D b := by simp only [smul_smul, h, one_smul, sq]
    _ = a • D (a * b) := by rw [leibniz, smul_add, add_comm]
    _ = 0 := by rw [h, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 b : A
h : a * b = 1
D₁ :
  HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M)
D₂ :
  a • HSMul.hSMul (β := M) b ((D : (a : A) → M) a : M) + a • HSMul.hSMul (β := M) a ((D : (a : A) → M) b : M) =
    HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M)
⊢ HAdd.hAdd (α := M) ((D : (a : A) → M) a : M)
      (HSMul.hSMul (β := M) (HPow.hPow (β := ℕ) a 2) ((D : (a : A) → M) b : M)) =
    0
have D₃ : HSMul.hSMul (β := M) a ((D : (a : A) → M) (a * b) : M) = 0
Tactic: calc
    D a + a ^ 2 • D b = a • b • D a + a • a • D b := by simp only [smul_smul, h, one_smul, sq]
    _ = a • D (a * b) := by rw [leibniz, smul_add, add_comm]
    _ = 0 := by rw [h, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ (D : (a : K) → M) a⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) a⁻¹ 2) ((D : (a : K) → M) a : M)
have inl : (D : (a : K) → M) 0⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (α := K) (β := ℕ) 0⁻¹ 2) ((D : (a : K) → M) 0 : M)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
inl : (D : (a : K) → M) 0⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (α := K) (β := ℕ) 0⁻¹ 2) ((D : (a : K) → M) 0 : M)
⊢ (D : (a : K) → M) a⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) a⁻¹ 2) ((D : (a : K) → M) a : M)
have inr : ∀ (ha : a ≠ 0), (D : (a : K) → M) a⁻¹ = HSMul.hSMul (β := M) (-HPow.hPow (β := ℕ) a⁻¹ 2) ((D : (a : K) → M) a : M)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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
⊢ (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))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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⁻¹ ((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)
have 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)
Tactic: rw [← inv_mul_mul_self b⁻¹, inv_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
⊢ (D : (a : K) → M) (a / b) = HSMul.hSMul (β := M) b⁻¹ ((D : (a : K) → M) a : M)
have 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)
Tactic: simp only [leibniz_div, inv_pow, h, smul_zero, sub_zero, smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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⁻¹ ((D : (a : K) → M) a : M)
have 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)
Tactic: rw [← mul_self_mul_inv b⁻¹, inv_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 : ℤ
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
have pos : ∀ (hn : n = 0), (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
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
have neg : ∀ (hn : ¬n = 0), (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
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
have pos : ∀ (ha : a = 0), (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
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
have neg : ∀ (ha : ¬a = 0), (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
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
have neg : ∀ (h : n = (↑n.natAbs : ℤ)),
  (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
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
have neg₁ : ∀ (h : n = -(↑n.natAbs : ℤ)),
  (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
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 : ℤ)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
have 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))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 : ℤ)
⊢ (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))
have 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)
Tactic: simp only [zpow_natCast, leibniz_pow, natCast_zsmul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 • 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)
have 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)
Tactic: rw [← zpow_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 • 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)
have neg : (↑(n.natAbs - 1) : ℤ) = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) 1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 : ℤ)
⊢ (D : (a : K) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : K) → M) a : M)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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) * a ^ HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1)
      ((D : (a : K) → M) a : M)
have 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)
Tactic: trans (-n.natAbs * (a ^ ((n.natAbs - 1 : ℕ) : ℤ) / (a ^ ((n.natAbs * 2 : ℕ) : ℤ)))) • D a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: trans (-n.natAbs * (a ^ ((n.natAbs - 1 : ℕ) : ℤ) / (a ^ ((n.natAbs * 2 : ℕ) : ℤ)))) • D a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
      (-(↑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)
have 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)
Tactic: rw [← zpow_sub₀ ha]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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) (-(↑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)
have e_a : Eq.{u_4 + 1} (α := K) (-(↑n.natAbs : K)) (↑(-(↑n.natAbs : ℤ)) : K)
Tactic: congr 3
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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)
⊢ 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)
have e_a₁ : HSub.hSub (α := ℤ) (↑(n.natAbs - 1) : ℤ) (↑(n.natAbs * 2) : ℤ) = HSub.hSub (α := ℤ) (-(↑n.natAbs : ℤ)) 1
Tactic: congr 3
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
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 : ℤ)
⊢ Eq.{u_4 + 1} (α := K) (-(↑n.natAbs : K)) (↑(-(↑n.natAbs : ℤ)) : K)
have e_a : Eq.{u_4 + 1} (α := K) (↑(-|n|) : K) (↑(-|n|) : K)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.DifferentialRing (goal)
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
⊢ Eq (α := R) (((algebraMap A R : (a : A) → R) a : R)′ : R) ((algebraMap A R : (a : A) → R) (a′ : A) : R)
have 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)
Tactic: change (LinearMap.comp ..) _ = _