-- Mathlib/RingTheory/Derivation/Basic.lean
lemma leibniz_zpow (a : K) (n : ℤ) : D (a ^ n) = n • a ^ (n - 1) • D a

Proof state:
case e_a.e_a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -↑n.natAbs = ↑(-↑n.natAbs)

Tactic:
norm_cast

Result:
no goals

Proof state:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
rw [h]

Result:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ D (a ^ ↑n.natAbs) = ↑n.natAbs • a ^ (↑n.natAbs - 1) • D a

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-↑n.natAbs * a ^ (↑(n.natAbs - 1) - ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a

Tactic:
congr 3

Result:
case e_a.e_a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -↑n.natAbs = ↑(-↑n.natAbs)

case e_a.e_a.e_a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ ↑(n.natAbs - 1) - ↑(n.natAbs * 2) = -↑n.natAbs - 1

Proof state:
case e_a.e_a.e_a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ ↑(n.natAbs - 1) - ↑(n.natAbs * 2) = -↑n.natAbs - 1

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Proof state:
case neg.inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs * a ^ ↑(n.natAbs - 1)) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a

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

Result:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs * a ^ ↑(n.natAbs - 1)) • D a =
    (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a

R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs * a ^ ↑(n.natAbs - 1)) • D a =
    (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a

Tactic:
ring_nf

Result:
no goals

Proof state:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ ↑(n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a

Tactic:
congr

Result:
case neg.inl.e_a.e_a.e_a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ ↑(n.natAbs - 1) = ↑n.natAbs - 1

Proof state:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
simp [hn]

Result:
no goals

Proof state:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ D (a ^ ↑n.natAbs) = ↑n.natAbs • a ^ (↑n.natAbs - 1) • D a

Tactic:
simp only [zpow_natCast, leibniz_pow, natCast_zsmul]

Result:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ (n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a

Proof state:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ (n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a

Tactic:
rw [← zpow_natCast]

Result:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ ↑(n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a

Proof state:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : a = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
simp [ha, zero_zpow n hn]

Result:
no goals