-- Mathlib/RingTheory/Derivation/Basic.lean
theorem leibniz_pow (n : ℕ) : D (a ^ n) = n • a ^ (n - 1) • D a

Proof state:
case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Tactic:
have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]

Result:
case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
this : a * a ^ (n - 1) = a ^ n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Proof state:
case succ
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Tactic:
rcases (zero_le n).eq_or_lt with (rfl | hpos)

Result:
case succ.inl
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
ihn : D (a ^ 0) = 0 • a ^ (0 - 1) • D a
⊢ D (a ^ (0 + 1)) = (0 + 1) • a ^ (0 + 1 - 1) • D a

case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
rw [← pow_succ', Nat.sub_add_cancel hpos]

Result:
no goals

Proof state:
case succ.inl
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
ihn : D (a ^ 0) = 0 • a ^ (0 - 1) • D a
⊢ D (a ^ (0 + 1)) = (0 + 1) • a ^ (0 + 1 - 1) • D a

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
induction' n with n ihn

Result:
case zero
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
⊢ D (a ^ 0) = 0 • a ^ (0 - 1) • D a

case succ
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Proof state:
case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
this : a * a ^ (n - 1) = a ^ n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Tactic:
simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this,
  Nat.succ_eq_add_one, Nat.add_succ_sub_one, add_zero, one_nsmul]

Result:
no goals

Proof state:
case zero
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
⊢ D (a ^ 0) = 0 • a ^ (0 - 1) • D a

Tactic:
rw [pow_zero, map_one_eq_zero, zero_smul]

Result:
no goals