awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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 y ∈ f '' t

Tactic:
mem_image_of_mem _ hy.1.2

Premises used: And.right, And.left, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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 y ∈ f '' t

Tactic:
exact mem_image_of_mem _ hy.1.2

Premises used: And.right, And.left, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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₁ : f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' t)
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f x)

Tactic:
apply Submodule.closure_subset_topologicalClosure_span

Premises used: Submodule.closure_subset_topologicalClosure_span
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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₁ : f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' (s ∩ t))
⊢ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' t)

Tactic:
suffices A : f x ∈ closure (f '' (s ∩ t)) from
      closure_mono (image_mono inter_subset_right) A
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
h₂ : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
⊢ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' (s ∩ t))

Tactic:
apply ContinuousWithinAt.mem_closure_image

Premises used: ContinuousWithinAt.mem_closure_image
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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}
⊢ ContinuousWithinAt f (s ∩ t) x

Tactic:
apply H'.continuousWithinAt.mono inter_subset_left

Premises used: Set.inter_subset_left, DifferentiableWithinAt.continuousWithinAt, ContinuousWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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₁ : (𝓝[s ∩ t] x).NeBot
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot]

Premises used: mem_closure_iff_nhdsWithin_neBot
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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}
⊢ (𝓝[s ∩ t] x).NeBot

Tactic:
I.mono (nhdsWithin_mono _ diff_subset)

Premises used: Set.diff_subset, Filter.NeBot.mono, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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}
⊢ (𝓝[s ∩ t] x).NeBot

Tactic:
exact I.mono (nhdsWithin_mono _ diff_subset)

Premises used: Set.diff_subset, Filter.NeBot.mono, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
rw :
  range (derivWithin f univ) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
⊢ range (deriv f) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
rw [← derivWithin_univ]

Premises used: derivWithin_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
h₁ : univ ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (univ ∩ t)
⊢ range (derivWithin f univ) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
apply range_derivWithin_subset_closure_span_image

Premises used: range_derivWithin_subset_closure_span_image
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ univ ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (univ ∩ t)

Tactic:
simp [dense_iff_closure_eq.1 h]

Premises used: dense_iff_closure_eq, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
s : Set 𝕜
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
(IsSeparable.of_separableSpace s).exists_countable_dense_subset

Premises used: TopologicalSpace.IsSeparable.of_separableSpace, TopologicalSpace.IsSeparable.exists_countable_dense_subset
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
s : Set 𝕜
obtain :
  ∀ (t : Set 𝕜) (ts : t ⊆ s) (t_count : t.Countable)
    (ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t), IsSeparable (range (derivWithin f s))
⊢ 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

Premises used: TopologicalSpace.IsSeparable.of_separableSpace, TopologicalSpace.IsSeparable.exists_countable_dense_subset
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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 rwa rwa₁ rwa₂ rwa₃ : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)

Tactic:
rwa [inter_eq_self_of_subset_right ts]

Premises used: Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
⊢ s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)

Tactic:
have : s ⊆ closure (s ∩ t) := by rwa [inter_eq_self_of_subset_right ts]
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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)
apply :
  IsSeparable (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F))
⊢ IsSeparable (range (derivWithin f s))

Tactic:
apply IsSeparable.mono _ (range_derivWithin_subset_closure_span_image f this)

Premises used: TopologicalSpace.IsSeparable.mono, range_derivWithin_subset_closure_span_image
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F))

Tactic:
(Countable.image t_count f).isSeparable.span.closure

Premises used: TopologicalSpace.IsSeparable.span, TopologicalSpace.IsSeparable.closure, Set.Countable.image, Set.Countable.isSeparable
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F))

Tactic:
exact (Countable.image t_count f).isSeparable.span.closure

Premises used: TopologicalSpace.IsSeparable.span, TopologicalSpace.IsSeparable.closure, Set.Countable.image, Set.Countable.isSeparable
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
rw : IsSeparable (range (derivWithin f univ))
⊢ IsSeparable (range (deriv f))

Tactic:
rw [← derivWithin_univ]

Premises used: derivWithin_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (derivWithin f univ))

Tactic:
isSeparable_range_derivWithin _ _

Premises used: isSeparable_range_derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (derivWithin f univ))

Tactic:
exact isSeparable_range_derivWithin _ _

Premises used: isSeparable_range_derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
rw : ContinuousAt (Function.update (β := fun (a : 𝕜) ↦ 𝕜) (slope f c) c a) c
⊢ ContinuousAt (Y := 𝕜) (Function.update (β := fun (a : 𝕜) ↦ 𝕜) (fun (x : 𝕜) ↦ (f x - f c) / (x - c)) c a) c

Tactic:
rw [← slope_fun_def_field]

Premises used: slope_fun_def_field
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (β := fun (a : 𝕜) ↦ 𝕜) (slope f c) c a) c

Tactic:
continuousAt_update_same.mpr <| hasDerivAt_iff_tendsto_slope.mp hf

Premises used: Iff.mpr, Iff.mp, hasDerivAt_iff_tendsto_slope, continuousAt_update_same
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (β := fun (a : 𝕜) ↦ 𝕜) (slope f c) c a) c

Tactic:
exact continuousAt_update_same.mpr <| hasDerivAt_iff_tendsto_slope.mp hf

Premises used: Iff.mpr, Iff.mp, hasDerivAt_iff_tendsto_slope, continuousAt_update_same
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
⊢ (𝓝[s \ {x}] x).NeBot

Tactic:
have : (𝓝[s \ {x}] x).NeBot := accPt_principal_iff_nhdsWithin.mp hx
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
⊢ MonotoneOn g (insert x s)

Tactic:
have h'g : MonotoneOn g (insert x s) :=
    hg.insert_of_continuousWithinAt hx.clusterPt hd.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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)
⊢ Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')

Tactic:
have : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g') := hasDerivWithinAt_iff_tendsto_slope.mp hd
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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')
apply : ∀ᶠ (c : 𝕜) in 𝓝[s \ {x}] x, 0 ≤ slope g x c
⊢ 0 ≤ g'

Tactic:
apply ge_of_tendsto this

Premises used: ge_of_tendsto
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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')
h : ∀ (y : 𝕜) (hy : y ∈ s \ {x}), 0 ≤ slope g x y
⊢ ∀ᶠ (c : 𝕜) in 𝓝[s \ {x}] x, 0 ≤ slope g x c

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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}
⊢ y ∈ s ∧ ¬y = x

Tactic:
simp only [mem_diff, mem_singleton_iff] at hy

Premises used: Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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 ∧ ¬y = x
⊢ x ∈ insert x s

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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 ∧ ¬y = x
⊢ y ∈ insert x s

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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 ∧ ¬y = x
⊢ 0 ≤ slope g x y

Tactic:
exact h'g.slope_nonneg (by simp) (by simp [hy])

Premises used: MonotoneOn.slope_nonneg
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
neg : ∀ (hd : ¬DifferentiableWithinAt 𝕜 g s x), 0 ≤ derivWithin g s x
⊢ 0 ≤ derivWithin g s x

Tactic:
by_cases hd : DifferentiableWithinAt 𝕜 g s x

Premises used: DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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

Tactic:
simp [derivWithin_zero_of_not_differentiableWithinAt hd]

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
neg : ∀ (hx : ¬AccPt x (𝓟 s)), 0 ≤ derivWithin g s x
⊢ 0 ≤ derivWithin g s x

Tactic:
by_cases hx : AccPt x (𝓟 s)

Premises used: Filter.principal, AccPt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
hx : ¬AccPt x (𝓟 s)
⊢ 0 ≤ derivWithin g s x

Tactic:
simp [derivWithin_zero_of_not_accPt hx]

Premises used: derivWithin_zero_of_not_accPt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
hx : AccPt x (𝓟 s)
⊢ 0 ≤ derivWithin g s x

Tactic:
hd.hasDerivWithinAt.nonneg_of_monotoneOn hx hg

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.nonneg_of_monotoneOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
hx : AccPt x (𝓟 s)
⊢ 0 ≤ derivWithin g s x

Tactic:
exact hd.hasDerivWithinAt.nonneg_of_monotoneOn hx hg

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.nonneg_of_monotoneOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
⊢ HasDerivWithinAt g g' univ x

Tactic:
rw [← hasDerivWithinAt_univ] at hd

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
hd₁ : HasDerivWithinAt g g' univ x
⊢ Monotone g

Tactic:
rw [← hasDerivWithinAt_univ] at hd

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
apply : AccPt x (𝓟 univ)
⊢ 0 ≤ g'

Tactic:
apply hd.nonneg_of_monotoneOn _ (hg.monotoneOn _)

Premises used: HasDerivWithinAt.nonneg_of_monotoneOn, Monotone.monotoneOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
⊢ AccPt x (𝓟 univ)

Tactic:
PerfectSpace.univ_preperfect _ (mem_univ _)

Premises used: PerfectSpace.univ_preperfect, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
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
⊢ AccPt x (𝓟 univ)

Tactic:
exact PerfectSpace.univ_preperfect _ (mem_univ _)

Premises used: PerfectSpace.univ_preperfect, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Monotone g
rw : 0 ≤ derivWithin g univ x
⊢ 0 ≤ deriv g x

Tactic:
rw [← derivWithin_univ]

Premises used: derivWithin_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Monotone g
⊢ 0 ≤ derivWithin g univ x

Tactic:
(hg.monotoneOn univ).derivWithin_nonneg

Premises used: Set.univ, MonotoneOn.derivWithin_nonneg, Monotone.monotoneOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Monotone g
⊢ 0 ≤ derivWithin g univ x

Tactic:
exact (hg.monotoneOn univ).derivWithin_nonneg

Premises used: Set.univ, MonotoneOn.derivWithin_nonneg, Monotone.monotoneOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x_1 : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx_1 : AccPt x_1 (𝓟 s)
hd : HasDerivWithinAt g g' s x_1
hg : AntitoneOn g s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
hxy : x ≤ y
⊢ (-g) x ≤ (-g) y

Tactic:
simpa using hg hx hy hxy