-- Mathlib/Analysis/Calculus/Deriv/ZPow.lean
theorem hasStrictDerivAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
    HasStrictDerivAt (fun x => x ^ m) ((m : 𝕜) * x ^ (m - 1)) x

Proof state:
case inl.refine_2
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
convert this using 1

Result:
case h.e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹

Proof state:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm)) <;>
  [skip; exact zpow_ne_zero _ hx]

Result:
case inl.refine_2
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (Inv.inv ∘ fun x => x ^ (-m)) ((↑(-m) * x ^ (-m - 1)) • -((x ^ (-m)) ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Proof state:
case h.e'_9.h.e'_6
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ 1 ≤ m

Tactic:
norm_cast at hm

Result:
no goals

Proof state:
case h.e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑m * x ^ (-m - 1 + (m + m))

Tactic:
congr

Result:
case h.e'_9.e_a.e_a
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ m - 1 = -m - 1 + (m + m)

Proof state:
case h.e'_9.h.e'_6
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ x ^ (↑m - 1) = x ^ (m - 1)

Tactic:
rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_natCast]

Result:
case h.e'_9.h.e'_6
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ 1 ≤ m

Proof state:
case intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ HasStrictDerivAt (fun x => x ^ ↑m) (↑↑m * x ^ (↑m - 1)) x

Tactic:
simp only [zpow_natCast, Int.cast_natCast]

Result:
case intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (↑m - 1)) x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
rcases lt_trichotomy m 0 with (hm | hm | hm)

Result:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

case inr.inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m = 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

case inr.inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : 0 < m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Proof state:
case h.e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹

Tactic:
rw [sq, mul_inv, inv_inv, Int.cast_neg, neg_mul, neg_mul_neg, ← zpow_add₀ hx, mul_assoc, ←
  zpow_add₀ hx]

Result:
case h.e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑m * x ^ (-m - 1 + (m + m))

Proof state:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
have hx : x ≠ 0 := h.resolve_right hm.not_le

Result:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℤ
hm : 0 < m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
lift m to ℕ using hm.le

Result:
case intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ HasStrictDerivAt (fun x => x ^ ↑m) (↑↑m * x ^ (↑m - 1)) x

Proof state:
case inr.inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : 0 < m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
exact this m hm

Result:
no goals

Proof state:
case inl.refine_2
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (Inv.inv ∘ fun x => x ^ (-m)) ((↑(-m) * x ^ (-m - 1)) • -((x ^ (-m)) ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
simp only [Function.comp_def, zpow_neg, one_div, inv_inv, smul_eq_mul] at this

Result:
case inl.refine_2
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Proof state:
case inr.inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m = 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
simp only [hm, zpow_zero, Int.cast_zero, zero_mul, hasStrictDerivAt_const]

Result:
no goals

Proof state:
case h.e'_9.e_a.e_a
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ m - 1 = -m - 1 + (m + m)

Tactic:
abel

Result:
no goals