awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : ℤ))
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
    (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑k : ℤ))
have 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) : ℤ))
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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
⊢ deriv^[k] (fun (x : 𝕜) ↦ x ^ n) x = (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑n : 𝕜) (↑i : 𝕜)) * x ^ (n - k)
have 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) : ℤ)
Tactic: simp only [← zpow_natCast, iter_deriv_zpow, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
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) : ℤ)
have 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) : ℤ)
Tactic: rcases le_or_gt k n with hkn | hnk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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) : ℤ)
⊢ (∏ 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) : ℤ)
have 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) : ℤ)
Tactic: rcases le_or_gt k n with hkn | hnk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
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) : ℤ)
have 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 : ℤ)
Tactic: rw [Int.ofNat_sub hkn]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
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) : ℤ)
have this : 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 _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
⊢ (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (-1) (↑i : 𝕜)) * x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) =
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have 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 : ℤ))
Tactic: simp only [← neg_add', Finset.prod_neg, ← Finset.prod_Ico_id_eq_factorial,
      Finset.prod_Ico_eq_prod_range]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : ℤ)
⊢ 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) : ℤ)
have 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) : ℤ)
Tactic: rw [factorial_succ, add_comm k 1, iterate_add_apply, ihk]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : ℤ)
⊢ 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) : ℤ)
have 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) : ℤ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : 𝕜
⊢ 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) : ℤ)
have 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 : ℤ))
Tactic: simp only [Int.reduceNeg, iterate_one, deriv_const_mul_field', cast_add, cast_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : 𝕜
⊢ 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 : ℤ))
have 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 : ℤ))
Tactic: by_cases hd : c = 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : ℤ))
⊢ 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 : ℤ))
have 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 : ℤ))
Tactic: by_cases hd : c = 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
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 : ℤ))
have 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))
Tactic: have := deriv_comp_add_const (fun x ↦ (c * x) ^ (-1 - k : ℤ)) (d / c) z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : ℤ)
have h : ∀ (y : 𝕜), (c * (y + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) = (c * y + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
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))
⊢ 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 : ℤ))
have h0 : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
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 : ℤ)
⊢ 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 : ℤ))
have this₁ : 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
Cleared hypotheses: this, h0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 :
  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)))
h0 :
  Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-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 : ℤ))
have neg : HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
    (c * (HSub.hSub (α := 𝕜) (-1) (↑k : 𝕜) * (c * (z + d / c)) ^ (HSub.hSub (α := ℤ) (-1) (↑k : ℤ) - 1))) =
  HPow.hPow (α := 𝕜) (-1) (1 + k) * (HAdd.hAdd (α := 𝕜) 1 (↑k : 𝕜) * (↑k ! : 𝕜)) * c ^ (1 + k) *
    (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
Tactic: simp [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 :
  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)))
h0 :
  Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
      (c * (HSub.hSub (α := 𝕜) (-1) (↑k : 𝕜) * (c * (z + d / c)) ^ (HSub.hSub (α := ℤ) (-1) (↑k : ℤ) - 1))) =
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (HAdd.hAdd (α := 𝕜) 1 (↑k : 𝕜) * (↑k ! : 𝕜)) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
have neg : HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * c * HSub.hSub (α := 𝕜) (-1) (↑k : 𝕜) *
    (c * z + d) ^ (HSub.hSub (α := ℤ) (-1) (↑k : ℤ) - 1) =
  (↑k ! : 𝕜) * HPow.hPow (α := 𝕜) (-1) (1 + k) * HAdd.hAdd (α := 𝕜) 1 (↑k : 𝕜) * c ^ (1 + k) *
    (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
c d : 𝕜
⊢ 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 : ℤ)
have zero : 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: induction k with
  | zero => simp
  | succ k ihk =>
    rw [factorial_succ, add_comm k 1, iterate_add_apply, ihk]
    ext z
    simp only [Int.reduceNeg, iterate_one, deriv_const_mul_field', cast_add, cast_one]
    by_cases hd : c = 0
    · simp [hd]
    · have := deriv_comp_add_const (fun x ↦ (c * x) ^ (-1 - k : ℤ)) (d / c) z
      have h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - (k : ℤ))) =
        (fun x ↦ (c * x + d) ^ (-1 - (k : ℤ))) := by
        ext y
        field_simp
      rw [h0, deriv_comp_mul_left c (fun x ↦ (x) ^ (-1 - k : ℤ)) (z + d / c)] at this
      simp [this]
      field_simp
      ring_nf
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
c d : 𝕜
zero :
  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 : ℤ)
⊢ 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 : ℤ)
have succ : ∀ (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 : ℤ)),
  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: induction k with
  | zero => simp
  | succ k ihk =>
    rw [factorial_succ, add_comm k 1, iterate_add_apply, ihk]
    ext z
    simp only [Int.reduceNeg, iterate_one, deriv_const_mul_field', cast_add, cast_one]
    by_cases hd : c = 0
    · simp [hd]
    · have := deriv_comp_add_const (fun x ↦ (c * x) ^ (-1 - k : ℤ)) (d / c) z
      have h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - (k : ℤ))) =
        (fun x ↦ (c * x + d) ^ (-1 - (k : ℤ))) := by
        ext y
        field_simp
      rw [h0, deriv_comp_mul_left c (fun x ↦ (x) ^ (-1 - k : ℤ)) (z + d / c)] at this
      simp [this]
      field_simp
      ring_nf
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
⊢ ContinuousOn f (Ioc a b)
have pos : ∀ (g₀ : a < b), ContinuousOn f (Ioc a b)
Tactic: by_cases! g₀ : a < b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
pos : ∀ (g₀ : a < b), ContinuousOn f (Ioc a b)
⊢ ContinuousOn f (Ioc a b)
have neg : ∀ (g₀ : b ≤ a), ContinuousOn f (Ioc a b)
Tactic: by_cases! g₀ : a < b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioo a b)
⊢ ContinuousOn f (Ico a b)
have pos : ∀ (g₀ : a < b), ContinuousOn f (Ico a b)
Tactic: by_cases! g₀ : a < b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioo a b)
pos : ∀ (g₀ : a < b), ContinuousOn f (Ico a b)
⊢ ContinuousOn f (Ico a b)
have neg : ∀ (g₀ : b ≤ a), ContinuousOn f (Ico a b)
Tactic: by_cases! g₀ : a < b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
⊢ ContinuousOn f (Icc a b)
have pos : ∀ (g₀ : a ≤ b), ContinuousOn f (Icc a b)
Tactic: by_cases! g₀ : a ≤ b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
pos : ∀ (g₀ : a ≤ b), ContinuousOn f (Icc a b)
⊢ ContinuousOn f (Icc a b)
have neg : ∀ (g₀ : b < a), ContinuousOn f (Icc a b)
Tactic: by_cases! g₀ : a ≤ b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
⊢ ContinuousOn f (Iic b)
have simp_rw : ContinuousOn f (Iio b ∪ {b})
Tactic: simp_rw [← Iio_union_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioi a)
⊢ ContinuousOn f (Ici a)
have rw : ContinuousOn f (Ioi a ∪ {a})
Tactic: rw [← Ioi_union_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Ioo a c) b
have refine_1 : MonotoneOn f (Ioc a b)
Tactic: refine isMaxOn_Ioo_of_mono_anti ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Ioc a b)
⊢ IsMaxOn f (Ioo a c) b
have refine_2 : AntitoneOn f (Ico b c)
Tactic: refine isMaxOn_Ioo_of_mono_anti ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ MonotoneOn f (Ioc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc h hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
⊢ MonotoneOn f (Ioc a b)
have refine_1₁ : ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc h hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ AntitoneOn f (Ico b c)
have refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico h hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
⊢ AntitoneOn f (Ico b c)
have refine_2₁ : ∀ x ∈ interior (Ico b c), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico h hd₁)