awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
have refine : ∀ (z : ℝ) (hxz : x < z) (hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
Tactic: refine this.mp (Eventually.mono self_mem_nhdsWithin fun z hxz hz ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
have rwa : ∀ (hz : |z - x|⁻¹ * (‖f z‖ - ‖f x‖) < r), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
Tactic: rwa [Real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
rwa : ∀ (hz : |z - x|⁻¹ * (‖f z‖ - ‖f x‖) < r), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
have rwa₁ : ∀ (hz : (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
Tactic: rwa [Real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst_7 : TrivialStar 𝕜
s : Set 𝕜
⊢ derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)
have pos : ∀ (hxs : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)
Tactic: by_cases hxs : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst_7 : TrivialStar 𝕜
s : Set 𝕜
pos : ∀ (hxs : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)
⊢ derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)
have neg : ∀ (hxs : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)
Tactic: by_cases hxs : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
f' : F
hf : HasDerivAt f f' x
⊢ HasFDerivAt (𝕜 := 𝕜) (E := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) : 𝕜 → F)
    (ContinuousLinearMap.toSpanSingleton 𝕜 (star f') : 𝕜 →L[𝕜] F) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
have h : Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜) →
    Eq (α := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (star f'))
      ((↑(starL 𝕜) : F →L⋆[𝕜] F) ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 f' ∘SL (↑(starL 𝕜) : 𝕜 →L⋆[𝕜] 𝕜))
Tactic: convert! hf.hasFDerivAt.star_star
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
f' : F
hf : HasDerivAt f f' x
e_4 : Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜)
⊢ Eq (α := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (star f'))
    ((↑(starL 𝕜) : F →L⋆[𝕜] F) ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 f' ∘SL (↑(starL 𝕜) : 𝕜 →L⋆[𝕜] 𝕜))
have h : Eq.{v + 1} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 (star f') : (a : 𝕜) → F) 1 : F)
  (((↑(starL 𝕜) : F →L⋆[𝕜] F) ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 f' ∘SL (↑(starL 𝕜) : 𝕜 →L⋆[𝕜] 𝕜) : (a : 𝕜) → F)
      1 :
    F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) f' x
⊢ HasDerivAt f (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
have h : f = star ∘ Function.comp (β := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)
Tactic: convert! hf.star_conj
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt f (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
⊢ HasDerivAt (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) f' x
have h : f' = star (star f')
Tactic: convert! hf.star_conj
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt f (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
h : f' = star (star f')
⊢ HasDerivAt (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) f' x
have h₁ : x = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
Tactic: convert! hf.star_conj
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) x
⊢ DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
have h : f = star ∘ Function.comp (β := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)
Tactic: convert! hf.star_conj
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)
⊢ DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) x
have h : x = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
Tactic: convert! hf.star_conj
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
⊢ Eq (α := (x : 𝕜) → F) (deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)))
    (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜))
have h : ∀ (z : 𝕜), deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
⊢ deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
have pos : ∀ (hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)),
  deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
Tactic: by_cases hf : DifferentiableAt 𝕜 f (conj z)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
pos :
  ∀ (hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)),
    deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
⊢ deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
have neg : ∀ (hf : ¬DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)),
  deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
Tactic: by_cases hf : DifferentiableAt 𝕜 f (conj z)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
hf : DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)
⊢ deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
have h : z = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
Tactic: convert! hf.hasDerivAt.star_conj.deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Star (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
z : 𝕜
hf : ¬DifferentiableAt 𝕜 f ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z)
⊢ deriv (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z = (star ∘ deriv f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
have this : ¬DifferentiableAt 𝕜 (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) z
Tactic: have := differentiableAt_star_conj_iff.not.2 hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Support (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : x ∉ tsupport f
⊢ HasStrictDerivAt f 0 x
have h₁ : f =ᶠ[nhds x] 0
Tactic: rw [notMem_tsupport_iff_eventuallyEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Support (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : x ∉ tsupport f
⊢ deriv f x = 0
have h₁ : f =ᶠ[nhds x] 0
Tactic: rw [notMem_tsupport_iff_eventuallyEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Support (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∈ support (deriv f) → x ∈ tsupport f
have rw : x ∉ tsupport f → deriv f x = 0
Tactic: rw [← not_imp_not, notMem_support]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℤ
hm : 0 < m
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have lift : ∀ (m : ℕ) (hm : LT.lt (α := ℤ) 0 (↑m : ℤ)),
  HasStrictDerivAt (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (↑m : ℤ)) ((↑(↑m : ℤ) : 𝕜) * x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1) x
Tactic: lift m to ℕ using hm.le
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (↑m : ℤ)) ((↑(↑m : ℤ) : 𝕜) * x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1) x
have simp : HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1) x
Tactic: simp only [zpow_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1) x
have h₁ : x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1 = x ^ (m - 1)
Tactic: convert! hasStrictDerivAt_pow m x using 2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
⊢ x ^ HSub.hSub (α := ℤ) (↑m : ℤ) 1 = x ^ (m - 1)
have h₁ : 1 ≤ m
Tactic: rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m_1 : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m_1
m : ℕ
hm : LT.lt (α := ℤ) 0 (↑m : ℤ)
⊢ 1 ≤ m
have h₁ : ∀ (hm : 0 < m), 1 ≤ m
Tactic: norm_cast at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
Tactic: have : ∀ m : ℤ, 0 < m → HasStrictDerivAt (· ^ m) ((m : 𝕜) * x ^ (m - 1)) x := fun m hm ↦ by
    lift m to ℕ using hm.le
    simp only [zpow_natCast, Int.cast_natCast]
    convert! hasStrictDerivAt_pow m x using 2
    rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_natCast]
    norm_cast at hm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have inl : ∀ (hm : m < 0), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
Tactic: rcases lt_trichotomy m 0 with (hm | hm | hm)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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
inl : ∀ (hm : m < 0), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have inr : ∀ (hm : m = 0), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
Tactic: rcases lt_trichotomy m 0 with (hm | hm | hm)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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
inl : ∀ (hm : m < 0), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
inr : ∀ (hm : m = 0), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have inr₁ : ∀ (hm : 0 < m), HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
Tactic: rcases lt_trichotomy m 0 with (hm | hm | hm)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
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
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := h.resolve_right hm.not_ge
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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
hx : x ≠ 0
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have inl : ∀
  (this :
    HasStrictDerivAt (Inv.inv ∘ fun (x : 𝕜) ↦ x ^ (-m))
      (((↑(-m) : 𝕜) * x ^ (-m - 1)) • -(HPow.hPow (β := ℕ) (x ^ (-m)) 2)⁻¹) x),
  HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
Tactic: have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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
hx : x ≠ 0
inl :
  ∀
    (this :
      HasStrictDerivAt (Inv.inv ∘ fun (x : 𝕜) ↦ x ^ (-m))
        (((↑(-m) : 𝕜) * x ^ (-m - 1)) • -(HPow.hPow (β := ℕ) (x ^ (-m)) 2)⁻¹) x),
    HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have inl₁ : x ^ (-m) ≠ 0
Tactic: have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
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
hx : x ≠ 0
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have this₁ : HasStrictDerivAt (Inv.inv ∘ fun (x : 𝕜) ↦ x ^ (-m))
  (((↑(-m) : 𝕜) * x ^ (-m - 1)) • -(HPow.hPow (β := ℕ) (x ^ (-m)) 2)⁻¹) x
Tactic: have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm)) <;>
      [skip; exact zpow_ne_zero _ hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
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 (Inv.inv ∘ fun (x : 𝕜) ↦ x ^ (-m))
    (((↑(-m) : 𝕜) * x ^ (-m - 1)) • -(HPow.hPow (β := ℕ) (x ^ (-m)) 2)⁻¹) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have this₁ : HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹) x
Tactic: simp only [Function.comp_def, zpow_neg, inv_inv, smul_eq_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ m) ((↑m : 𝕜) * x ^ (m - 1)) x
have h₁ : (↑m : 𝕜) * x ^ (m - 1) = (↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : 𝕜) * x ^ (m - 1) = (↑(-m) : 𝕜) * x ^ (-m - 1) * -(HPow.hPow (β := ℕ) (x ^ m)⁻¹ 2)⁻¹
have h₁ : (↑m : 𝕜) * x ^ (m - 1) = (↑m : 𝕜) * x ^ (-m - 1 + (m + m))
Tactic: rw [sq, mul_inv, inv_inv, Int.cast_neg, neg_mul, neg_mul_neg, ← zpow_add₀ hx, mul_assoc, ←
      zpow_add₀ hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
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 : 𝕜) * x ^ (m - 1) = (↑m : 𝕜) * x ^ (-m - 1 + (m + m))
have h₁ : m - 1 = -m - 1 + (m + m)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)
have pos : ∀ (H : x ≠ 0 ∨ 0 ≤ m), deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)
Tactic: by_cases H : x ≠ 0 ∨ 0 ≤ m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
pos : ∀ (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)
have neg : ∀ (H : ¬(x ≠ 0 ∨ 0 ≤ m)), deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)
Tactic: by_cases H : x ≠ 0 ∨ 0 ≤ m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ deriv (fun (x : 𝕜) ↦ x ^ m) x = (↑m : 𝕜) * x ^ (m - 1)
have neg : 0 = (↑m : 𝕜) * x ^ (m - 1)
Tactic: rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_zpow.1 H)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ 0 = (↑m : 𝕜) * x ^ (m - 1)
have H₁ : x = 0 ∧ m < 0
Tactic: push Not at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : x = 0 ∧ m < 0
⊢ 0 = (↑m : 𝕜) * x ^ (m - 1)
have neg : ∀ (hm : m < 0), 0 = (↑m : 𝕜) * HPow.hPow (α := 𝕜) 0 (m - 1)
Tactic: rcases H with ⟨rfl, hm⟩
Cleared hypotheses: x, H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
⊢ 0 = (↑m : 𝕜) * HPow.hPow (α := 𝕜) 0 (m - 1)
have neg : 0 = HMul.hMul (α := 𝕜) (↑m : 𝕜) 0
Tactic: rw [zero_zpow _ ((sub_one_lt _).trans hm).ne, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
neg : 0 = HMul.hMul (α := 𝕜) (↑m : 𝕜) 0
⊢ 0 = (↑m : 𝕜) * HPow.hPow (α := 𝕜) 0 (m - 1)
have neg₁ : Eq.{u + 1} (α := 𝕜) 0 0
Tactic: rw [zero_zpow _ ((sub_one_lt _).trans hm).ne, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.ZPow (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
m : ℤ
k : ℕ
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
    (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑k : ℤ))
have zero : Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[0] fun (x : 𝕜) ↦ x ^ m) fun (x : 𝕜) ↦
  (∏ i ∈ Finset.range 0, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * x ^ (m - (↑0 : ℤ))
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