awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[(s ∩ t) \ {x}] x,
    slope f x x_1 ∈ (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
have h₁ : ∀ (y : 𝕜) (hy : y ∈ (s ∩ t) \ {x}), slope f x y ∈ (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ slope f x y ∈ (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
have h₁ : Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) ((y - x)⁻¹ • (f y - f x))
Tactic: simp only [slope, vsub_eq_sub, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t)))
    ((y - x)⁻¹ • (f y - f x))
have h₁ : Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f y)
Tactic: refine Submodule.smul_mem _ _ (Submodule.sub_mem _ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
h₁ : Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f y)
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t)))
    ((y - x)⁻¹ • (f y - f x))
have h₂ : Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f x)
Tactic: refine Submodule.smul_mem _ _ (Submodule.sub_mem _ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f y)
have h₁ : Membership.mem (γ := Submodule 𝕜 F) (Submodule.span 𝕜 (f '' t)) (f y)
Tactic: apply Submodule.le_topologicalClosure
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.span 𝕜 (f '' t)) (f y)
have h₁ : f y ∈ f '' t
Tactic: apply Submodule.subset_span
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f x)
have h₁ : f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' t)
Tactic: apply Submodule.closure_subset_topologicalClosure_span
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' t)
have h₁ : f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' (s ∩ t))
Tactic: suffices A : f x ∈ closure (f '' (s ∩ t)) from
      closure_mono (image_mono inter_subset_right) A
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' (s ∩ t))
have h₁ : ContinuousWithinAt f (s ∩ t) x
Tactic: apply ContinuousWithinAt.mem_closure_image
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
h₁ : ContinuousWithinAt f (s ∩ t) x
⊢ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' (s ∩ t))
have h₂ : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
Tactic: apply ContinuousWithinAt.mem_closure_image
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
have h₁ : (𝓝[s ∩ t] x).NeBot
Tactic: rw [mem_closure_iff_nhdsWithin_neBot]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ range (deriv f) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have rw : range (derivWithin f univ) ⊆
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
Tactic: rw [← derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ range (derivWithin f univ) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have h₁ : univ ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (univ ∩ t)
Tactic: apply range_derivWithin_subset_closure_span_image
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
s : Set 𝕜
⊢ IsSeparable (range (derivWithin f s))
have obtain : ∀ (t : Set 𝕜) (ts : t ⊆ s) (t_count : t.Countable)
  (ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t), IsSeparable (range (derivWithin f s))
Tactic: obtain ⟨t, ts, t_count, ht⟩ : ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t :=
    (IsSeparable.of_separableSpace s).exists_countable_dense_subset
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ IsSeparable (range (derivWithin f s))
have this : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
Tactic: have : s ⊆ closure (s ∩ t) := by rwa [inter_eq_self_of_subset_right ts]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
this : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
⊢ IsSeparable (range (derivWithin f s))
have apply : IsSeparable (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F))
Tactic: apply IsSeparable.mono _ (range_derivWithin_subset_closure_span_image f this)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (deriv f))
have rw : IsSeparable (range (derivWithin f univ))
Tactic: rw [← derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Y := 𝕜) (Function.update (β := fun (a : 𝕜) ↦ 𝕜) (fun (x : 𝕜) ↦ (f x - f c) / (x - c)) c a) c
have rw : ContinuousAt (Function.update (β := fun (a : 𝕜) ↦ 𝕜) (slope f c) c a) c
Tactic: rw [← slope_fun_def_field]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
⊢ 0 ≤ g'
have this : (𝓝[s \ {x}] x).NeBot
Tactic: have : (𝓝[s \ {x}] x).NeBot := accPt_principal_iff_nhdsWithin.mp hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this : (𝓝[s \ {x}] x).NeBot
⊢ 0 ≤ g'
have h'g : MonotoneOn g (insert x s)
Tactic: have h'g : MonotoneOn g (insert x s) :=
    hg.insert_of_continuousWithinAt hx.clusterPt hd.continuousWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
⊢ 0 ≤ g'
have this₁ : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
Tactic: have : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g') := hasDerivWithinAt_iff_tendsto_slope.mp hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this_1 : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
⊢ 0 ≤ g'
have apply : ∀ᶠ (c : 𝕜) in 𝓝[s \ {x}] x, 0 ≤ slope g x c
Tactic: apply ge_of_tendsto this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this_1 : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
⊢ ∀ᶠ (c : 𝕜) in 𝓝[s \ {x}] x, 0 ≤ slope g x c
have h : ∀ (y : 𝕜) (hy : y ∈ s \ {x}), 0 ≤ slope g x y
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this_1 : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
y : 𝕜
hy : y ∈ s \ {x}
⊢ 0 ≤ slope g x y
have hy₁ : y ∈ s ∧ ¬y = x
Tactic: simp only [mem_diff, mem_singleton_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
⊢ 0 ≤ derivWithin g s x
have pos : ∀ (hd : DifferentiableWithinAt 𝕜 g s x), 0 ≤ derivWithin g s x
Tactic: by_cases hd : DifferentiableWithinAt 𝕜 g s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
pos : ∀ (hd : DifferentiableWithinAt 𝕜 g s x), 0 ≤ derivWithin g s x
⊢ 0 ≤ derivWithin g s x
have neg : ∀ (hd : ¬DifferentiableWithinAt 𝕜 g s x), 0 ≤ derivWithin g s x
Tactic: by_cases hd : DifferentiableWithinAt 𝕜 g s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
hd : DifferentiableWithinAt 𝕜 g s x
⊢ 0 ≤ derivWithin g s x
have pos : ∀ (hx : AccPt x (𝓟 s)), 0 ≤ derivWithin g s x
Tactic: by_cases hx : AccPt x (𝓟 s)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
hd : DifferentiableWithinAt 𝕜 g s x
pos : ∀ (hx : AccPt x (𝓟 s)), 0 ≤ derivWithin g s x
⊢ 0 ≤ derivWithin g s x
have neg : ∀ (hx : ¬AccPt x (𝓟 s)), 0 ≤ derivWithin g s x
Tactic: by_cases hx : AccPt x (𝓟 s)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivAt g g' x
hg : Monotone g
⊢ 0 ≤ g'
have hd₁ : HasDerivWithinAt g g' univ x
Tactic: rw [← hasDerivWithinAt_univ] at hd
Cleared hypotheses: hd, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Monotone g
⊢ 0 ≤ g'
have apply : AccPt x (𝓟 univ)
Tactic: apply hd.nonneg_of_monotoneOn _ (hg.monotoneOn _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Monotone g
⊢ 0 ≤ deriv g x
have rw : 0 ≤ derivWithin g univ x
Tactic: rw [← derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : AntitoneOn g s
⊢ g' ≤ 0
have this : MonotoneOn (-g) s
Tactic: have : MonotoneOn (-g) s := fun x hx y hy hxy ↦ by simpa using hg hx hy hxy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivAt g g' x
hg : Antitone g
⊢ g' ≤ 0
have hd₁ : HasDerivWithinAt g g' univ x
Tactic: rw [← hasDerivWithinAt_univ] at hd
Cleared hypotheses: hd, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Antitone g
⊢ g' ≤ 0
have apply : AccPt x (𝓟 univ)
Tactic: apply hd.nonpos_of_antitoneOn _ (hg.antitoneOn _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Antitone g
⊢ deriv g x ≤ 0
have rw : derivWithin g univ x ≤ 0
Tactic: rw [← derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
have hr₀ : 0 < r
Tactic: have hr₀ : 0 < r := lt_of_le_of_lt (norm_nonneg f') hr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
have A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
Tactic: have A : ∀ᶠ z in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
    (hasDerivWithinAt_iff_tendsto_slope.1 hf).norm (IsOpen.mem_nhds isOpen_Iio hr)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
have B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
Tactic: have B : ∀ᶠ z in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
    mem_of_superset self_mem_nhdsWithin (singleton_subset_iff.2 <| by simp [hr₀])
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
have C : {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s \ {x}] x ⊔ 𝓝[{x}] x
Tactic: have C := mem_sup.2 ⟨A, B⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C : {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s \ {x}] x ⊔ 𝓝[{x}] x
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
have C₁ : {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
  {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
Tactic: rw [← nhdsWithin_union, diff_union_self, nhdsWithin_union, mem_sup] at C
Cleared hypotheses: C
-- 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
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
have h : ∀ (a : ℝ), ‖(a - x)⁻¹ • (f a - f x)‖ ∈ Iio r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
Tactic: filter_upwards [C.1]
-- 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
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ (a : ℝ), ‖(a - x)⁻¹ • (f a - f x)‖ ∈ Iio r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
have h : ∀ (a : ℝ), ‖a - x‖⁻¹ * ‖f a - f x‖ < r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
Tactic: simp only [norm_smul, mem_Iio, norm_inv]
-- 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
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
have apply : ∀ (x_1 : ℝ), ‖x_1 - x‖⁻¹ * ‖f x_1 - f x‖ < r → ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
Tactic: apply (hf.limsup_norm_slope_le hr).mono
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
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
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
have this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
Tactic: have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently