case zero
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
⊢ ↑D (a ^ Nat.zero) = Nat.zero • a ^ (Nat.zero - 1) • ↑D a

case succ
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
⊢ ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
induction' n with n ihn
no goals
case zero
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
⊢ ↑D (a ^ Nat.zero) = Nat.zero • a ^ (Nat.zero - 1) • ↑D a
rw [Nat.zero_eq, pow_zero, map_one_eq_zero, zero_smul]
case succ.inl
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
ihn : ↑D (a ^ 0) = 0 • a ^ (0 - 1) • ↑D a
⊢ ↑D (a ^ Nat.succ 0) = Nat.succ 0 • a ^ (Nat.succ 0 - 1) • ↑D a

case succ.inr
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
hpos : 0 < n
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
case succ
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
rcases (zero_le n).eq_or_lt with (rfl | hpos)
no goals
case succ.inl
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
ihn : ↑D (a ^ 0) = 0 • a ^ (0 - 1) • ↑D a
⊢ ↑D (a ^ Nat.succ 0) = Nat.succ 0 • a ^ (Nat.succ 0 - 1) • ↑D a
erw [pow_one, one_smul, pow_zero, one_smul]
case succ.inr
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
hpos : 0 < n
this : a * a ^ (n - 1) = a ^ n
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
case succ.inr
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
hpos : 0 < n
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ, Nat.sub_add_cancel hpos]
no goals
case succ.inr
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
hpos : 0 < n
this : a * a ^ (n - 1) = a ^ n
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
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]
no goals
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
hpos : 0 < n
⊢ a * a ^ (n - 1) = a ^ n
rw [← pow_succ, Nat.sub_add_cancel hpos]