awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this_1 : ∀ (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) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹) x
h₁ : (↑m : 𝕜) * x ^ (m - 1) = (↑m : 𝕜) * x ^ (-m - 1 + (m + m))
⊢ (↑m : 𝕜) * x ^ (m - 1) = (↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (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]

Premises used: Int.cast_neg, mul_inv, mul_assoc, sq, zpow_add₀, inv_inv, neg_mul_neg, neg_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this_1 : ∀ (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) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹) x
h₁ : m - 1 = -m - 1 + (m + m)
⊢ (↑m : 𝕜) * x ^ (m - 1) = (↑m : 𝕜) * x ^ (-m - 1 + (m + m))

Tactic:
congr
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this_1 : ∀ (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) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹) x
⊢ m - 1 = -m - 1 + (m + m)

Tactic:
abel
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : 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]

Premises used: Int.cast_zero, MulZeroClass.zero_mul, zpow_zero, hasStrictDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : 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:
this m hm
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : 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
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
⊢ HasDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x

Tactic:
(hasStrictDerivAt_zpow m x h).hasDerivAt

Premises used: hasStrictDerivAt_zpow, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
s : Set 𝕜
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) s x

Tactic:
(hasDerivAt_zpow m x h).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, hasDerivAt_zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
m : ℤ
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m

Tactic:
⟨fun H => NormedField.continuousAt_zpow.1 H.continuousAt, fun H =>
    (hasDerivAt_zpow m x H).differentiableAt⟩

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.continuousAt, NormedField.continuousAt_zpow, Iff.intro, Iff.mp, hasDerivAt_zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
⊢ DifferentiableWithinAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x ^ m) s x

Tactic:
(differentiableAt_zpow.mpr h).differentiableWithinAt

Premises used: Iff.mpr, differentiableAt_zpow, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
s : Set 𝕜
h : 0 ∉ s ∨ 0 ≤ m
⊢ DifferentiableOn 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x ^ m) s

Tactic:
fun x hxs =>
  differentiableWithinAt_zpow m x <| h.imp_left <| ne_of_mem_of_not_mem hxs

Premises used: Or.imp_left, ne_of_mem_of_not_mem, DifferentiableOn, differentiableWithinAt_zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
pos : ∀ (H : x ≠ 0 ∨ 0 ≤ m), deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)
neg : ∀ (H : ¬(x ≠ 0 ∨ 0 ≤ m)), deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)
⊢ deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)

Tactic:
by_cases H : x ≠ 0 ∨ 0 ≤ m
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : x ≠ 0 ∨ 0 ≤ m
⊢ deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)

Tactic:
(hasDerivAt_zpow m x H).deriv

Premises used: HasDerivAt.deriv, hasDerivAt_zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : x ≠ 0 ∨ 0 ≤ m
⊢ deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)

Tactic:
exact (hasDerivAt_zpow m x H).deriv

Premises used: HasDerivAt.deriv, hasDerivAt_zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
neg : 0 = (↑m : 𝕜) * x ^ (m - 1)
⊢ deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_zpow.1 H)]

Premises used: deriv_zero_of_not_differentiableAt, mt
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ x = 0 ∧ m < 0

Tactic:
push Not at H

Premises used: Not
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : x = 0 ∧ m < 0
neg : ∀ (hm : m < 0), 0 = (↑m : 𝕜) * HPow.hPow (α := 𝕜) 0 (m - 1)
⊢ 0 = (↑m : 𝕜) * x ^ (m - 1)

Tactic:
rcases H with ⟨rfl, hm⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
neg : 0 = HMul.hMul (α := 𝕜) (↑m : 𝕜) 0
neg₁ neg₂ : Eq.{u + 1} (α := 𝕜) 0 0
⊢ 0 = (↑m : 𝕜) * HPow.hPow (α := 𝕜) 0 (m - 1)

Tactic:
rw [zero_zpow _ ((sub_one_lt _).trans hm).ne, mul_zero]

Premises used: zero_zpow, sub_one_lt, MulZeroClass.mul_zero, LT.lt.trans, LT.lt.ne
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
⊢ Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (deriv fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦ (↑m : 𝕜) * x ^ (m - 1)

Tactic:
funext <| deriv_zpow m

Premises used: funext, deriv_zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
m : ℤ
hxs : UniqueDiffWithinAt 𝕜 s x
h : x ≠ 0 ∨ 0 ≤ m
⊢ derivWithin (fun (x : 𝕜) ↦ x ^ m) s x = (↑m : 𝕜) * x ^ (m - 1)

Tactic:
(hasDerivWithinAt_zpow m x h s).derivWithin hxs

Premises used: HasDerivWithinAt.derivWithin, hasDerivWithinAt_zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[0] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
    (∏ i ∈ Finset.range 0, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑0 : ℤ))

Tactic:
simp only [one_mul, Int.ofNat_zero, id, sub_zero, Finset.prod_range_zero, Function.iterate_zero]

Premises used: sub_zero, Function.iterate_zero, id, Int.ofNat_zero, Finset.prod_range_zero, one_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
    (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑k : ℤ))
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k + 1] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
    (∏ i ∈ Finset.range (k + 1), HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑(k + 1) : ℤ))

Tactic:
simp only [Function.iterate_succ_apply', ihk, deriv_const_mul_field', deriv_zpow',
      Finset.prod_range_succ, Int.natCast_succ, ← sub_sub, Int.cast_sub, Int.cast_natCast,
      mul_assoc]

Premises used: Function.iterate_succ_apply', Int.cast_natCast, Int.cast_sub, mul_assoc, deriv_const_mul_field', deriv_zpow', sub_sub, Int.natCast_succ, Finset.prod_range_succ
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
k : ℕ
zero :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[0] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
    (∏ i ∈ Finset.range 0, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑0 : ℤ))
succ :
  ∀ (k : ℕ)
    (ihk :
      Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
        (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑k : ℤ))),
    Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k + 1] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
      (∏ i ∈ Finset.range (k + 1), HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑(k + 1) : ℤ))
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
    (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑k : ℤ))

Tactic:
induction k with
  | zero =>
    simp only [one_mul, Int.ofNat_zero, id, sub_zero, Finset.prod_range_zero, Function.iterate_zero]
  | succ k ihk =>
    simp only [Function.iterate_succ_apply', ihk, deriv_const_mul_field', deriv_zpow',
      Finset.prod_range_succ, Int.natCast_succ, ← sub_sub, Int.cast_sub, Int.cast_natCast,
      mul_assoc]

Premises used: Function.iterate_succ_apply', Int.cast_natCast, sub_zero, Int.cast_sub, Function.iterate_zero, mul_assoc, deriv_const_mul_field', id, deriv_zpow', Int.ofNat_zero, sub_sub, Int.natCast_succ, Finset.prod_range_zero, Finset.prod_range_succ, one_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
k : ℕ
⊢ deriv^[k] (fun (y : 𝕜) ↦ y ^ m) x = (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑k : ℤ))

Tactic:
congr_fun (iter_deriv_zpow' m k) x

Premises used: iter_deriv_zpow', congr_fun
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
simp :
  (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * x ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * HPow.hPow (β := ℤ) x (↑(n - k) : ℤ)
⊢ deriv^[k] (fun (x : 𝕜) ↦ x ^ n) x = (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑i : 𝕜)) * x ^ (n - k)

Tactic:
simp only [← zpow_natCast, iter_deriv_zpow, Int.cast_natCast]

Premises used: zpow_natCast, Int.cast_natCast, iter_deriv_zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
inl :
  ∀ (hkn : k ≤ n),
    (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * x ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
      (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * HPow.hPow (β := ℤ) x (↑(n - k) : ℤ)
inr :
  ∀ (hnk : n < k),
    (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * x ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
      (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * HPow.hPow (β := ℤ) x (↑(n - k) : ℤ)
⊢ (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * x ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * HPow.hPow (β := ℤ) x (↑(n - k) : ℤ)

Tactic:
rcases le_or_gt k n with hkn | hnk

Premises used: le_or_gt
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hkn : k ≤ n
inl inl₁ :
  (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * x ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * x ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑k : ℤ)
⊢ (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * x ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * HPow.hPow (β := ℤ) x (↑(n - k) : ℤ)

Tactic:
rw [Int.ofNat_sub hkn]

Premises used: Int.ofNat_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
⊢ Eq.{u + 1} (α := 𝕜) (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑i : 𝕜)) 0

Tactic:
have : (∏ i ∈ Finset.range k, (n - i : 𝕜)) = 0 :=
      Finset.prod_eq_zero (Finset.mem_range.2 hnk) (sub_self _)
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
this : Eq.{u + 1} (α := 𝕜) (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑i : 𝕜)) 0
⊢ (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * x ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    (∏ x ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑x : 𝕜)) * HPow.hPow (β := ℤ) x (↑(n - k) : ℤ)

Tactic:
simp only [this, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n k : ℕ
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ x ^ n) fun (x : 𝕜) ↦
    (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑i : 𝕜)) * x ^ (n - k)

Tactic:
funext fun x => iter_deriv_pow n x k

Premises used: funext, iter_deriv_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
⊢ Eq.{u + 1} (α := 𝕜) (deriv^[k] Inv.inv x : 𝕜) (deriv^[k] (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (-1)) x : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
simp :
  (HPow.hPow (α := 𝕜) (-1) (Finset.range k).card * ∏ x ∈ Finset.range k, HAdd.hAdd (α := 𝕜) 1 (↑x : 𝕜)) *
      x ^ (-HAdd.hAdd (α := ℤ) 1 (↑k : ℤ)) =
    HPow.hPow (α := 𝕜) (-1) k * (↑(∏ k ∈ Finset.range (k + 1 - 1), (1 + k)) : 𝕜) * x ^ (-HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
⊢ (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (-1) (↑i : 𝕜)) * x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) =
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
simp only [← neg_add', Finset.prod_neg, ← Finset.prod_Ico_id_eq_factorial,
      Finset.prod_Ico_eq_prod_range]

Premises used: Finset.prod_Ico_id_eq_factorial, neg_add', Finset.prod_neg, Finset.prod_Ico_eq_prod_range
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
⊢ (HPow.hPow (α := 𝕜) (-1) (Finset.range k).card * ∏ x ∈ Finset.range k, HAdd.hAdd (α := 𝕜) 1 (↑x : 𝕜)) *
      x ^ (-HAdd.hAdd (α := ℤ) 1 (↑k : ℤ)) =
    HPow.hPow (α := 𝕜) (-1) k * (↑(∏ k ∈ Finset.range (k + 1 - 1), (1 + k)) : 𝕜) * x ^ (-HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] Inv.inv) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
funext (iter_deriv_inv k)

Premises used: funext, iter_deriv_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[0] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (β := ℕ) (-1) 0 * (↑0! : 𝕜) * HPow.hPow (β := ℕ) c 0 *
      (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑0 : ℤ)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
succ :
  Eq.{u + 1} (α := 𝕜 → 𝕜)
    (deriv^[1] fun (x : 𝕜) ↦
      HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
    fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
      (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑(1 + k) : ℤ)
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k + 1] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) (k + 1) * (↑(k + 1)! : 𝕜) * c ^ (k + 1) *
      (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑(k + 1) : ℤ)

Tactic:
rw [factorial_succ, add_comm k 1, iterate_add_apply, ihk]

Premises used: Function.iterate_add_apply, Nat.factorial_succ, add_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
succ :
  ∀ (z : 𝕜),
    deriv^[1]
        (fun (x : 𝕜) ↦ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
        z =
      HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
        (c * z + d) ^ HSub.hSub (α := ℤ) (-1) (↑(1 + k) : ℤ)
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜)
    (deriv^[1] fun (x : 𝕜) ↦
      HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
    fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
      (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑(1 + k) : ℤ)

Tactic:
ext z
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
succ :
  HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
      deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
⊢ deriv^[1]
      (fun (x : 𝕜) ↦ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
      z =
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
      (c * z + d) ^ HSub.hSub (α := ℤ) (-1) (↑(1 + k) : ℤ)

Tactic:
simp only [Int.reduceNeg, iterate_one, deriv_const_mul_field', cast_add, cast_one]

Premises used: Int.reduceNeg, deriv_const_mul_field', Nat.cast_add, Function.iterate_one, Nat.cast_one
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
pos :
  ∀ (hd : c = 0),
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
        deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
      HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
        (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
neg :
  ∀ (hd : ¬c = 0),
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
        deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
      HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
        (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
⊢ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
      deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))

Tactic:
by_cases hd : c = 0
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : c = 0
⊢ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
      deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))

Tactic:
simp [hd]
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z)
    (deriv (fun (x : 𝕜) ↦ (c * x) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (z + d / c))

Tactic:
have := deriv_comp_add_const (fun x ↦ (c * x) ^ (-1 - k : ℤ)) (d / c) z
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
this :
  Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z)
    (deriv (fun (x : 𝕜) ↦ (c * x) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (z + d / c))
h : ∀ (y : 𝕜), (c * (y + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) = (c * y + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
this :
  Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z)
    (deriv (fun (x : 𝕜) ↦ (c * x) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (z + d / c))
y : 𝕜
⊢ (c * (y + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) = (c * y + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
this :
  Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z)
    (deriv (fun (x : 𝕜) ↦ (c * x) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (z + d / c))
⊢ Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
have h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - (k : ℤ))) =
        (fun x ↦ (c * x + d) ^ (-1 - (k : ℤ))) := by
        ext y
        field_simp
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
this :
  Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z)
    (deriv (fun (x : 𝕜) ↦ (c * x) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (z + d / c))
h0 :
  Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HSMul.hSMul (β := 𝕜) c (deriv (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (c * (z + d / c)))

Tactic:
rw [h0, deriv_comp_mul_left c (fun x ↦ (x) ^ (-1 - k : ℤ)) (z + d / c)] at this

Premises used: HSub.hSub, HDiv.hDiv, Nat.cast, HPow.hPow, HAdd.hAdd, deriv_comp_mul_left, OfNat.ofNat, Neg.neg