awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Ioc a b)
⊢ IsMinOn f (Ioc a c) b
have refine_2 : MonotoneOn f (Icc b c)
Tactic: refine isMinOn_Ioc_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ AntitoneOn f (Ioc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
⊢ AntitoneOn f (Ioc a b)
have refine_1₁ : ∀ x ∈ interior (Ioc a b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ MonotoneOn f (Icc b c)
have refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
⊢ MonotoneOn f (Icc b c)
have refine_2₁ : ∀ x ∈ interior (Icc b c), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ IsMinOn f (Ico a c) b
have refine_1 : AntitoneOn f (Icc a b)
Tactic: refine isMinOn_Ico_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Icc a b)
⊢ IsMinOn f (Ico a c) b
have refine_2 : MonotoneOn f (Ico b c)
Tactic: refine isMinOn_Ico_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ AntitoneOn f (Icc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
⊢ AntitoneOn f (Icc a b)
have refine_1₁ : ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ MonotoneOn f (Ico b c)
have refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
⊢ MonotoneOn f (Ico b c)
have refine_2₁ : ∀ x ∈ interior (Ico b c), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ IsMinOn f (Icc a c) b
have refine_1 : AntitoneOn f (Icc a b)
Tactic: refine isMinOn_Icc_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Icc a b)
⊢ IsMinOn f (Icc a c) b
have refine_2 : MonotoneOn f (Icc b c)
Tactic: refine isMinOn_Icc_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ AntitoneOn f (Icc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
⊢ AntitoneOn f (Icc a b)
have refine_1₁ : ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ MonotoneOn f (Icc b c)
have refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
⊢ MonotoneOn f (Icc b c)
have refine_2₁ : ∀ x ∈ interior (Icc b c), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ IsMinOn f (Ioi a) b
have refine_1 : AntitoneOn f (Ioc a b)
Tactic: refine isMinOn_Ioi_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Ioc a b)
⊢ IsMinOn f (Ioi a) b
have refine_2 : MonotoneOn f (Ici b)
Tactic: refine isMinOn_Ioi_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ AntitoneOn f (Ioc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
⊢ AntitoneOn f (Ioc a b)
have refine_1₁ : ∀ x ∈ interior (Ioc a b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ MonotoneOn f (Ici b)
have refine_2 : DifferentiableOn ℝ f (interior (Ici b))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
⊢ MonotoneOn f (Ici b)
have refine_2₁ : ∀ x ∈ interior (Ici b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)
-- 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)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ IsMinOn f (Ici a) b
have refine_1 : AntitoneOn f (Icc a b)
Tactic: refine isMinOn_Ici_of_anti_mono ?_ ?_
-- 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)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Icc a b)
⊢ IsMinOn f (Ici a) b
have refine_2 : MonotoneOn f (Ici b)
Tactic: refine isMinOn_Ici_of_anti_mono ?_ ?_
-- 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)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ AntitoneOn f (Icc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)
-- 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)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
⊢ AntitoneOn f (Icc a b)
have refine_1₁ : ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)
-- 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)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ MonotoneOn f (Ici b)
have refine_2 : DifferentiableOn ℝ f (interior (Ici b))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)
-- 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)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
⊢ MonotoneOn f (Ici b)
have refine_2₁ : ∀ x ∈ interior (Ici b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ IsMinOn f (Iio c) b
have refine_1 : AntitoneOn f (Iic b)
Tactic: refine isMinOn_Iio_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Iic b)
⊢ IsMinOn f (Iio c) b
have refine_2 : MonotoneOn f (Ico b c)
Tactic: refine isMinOn_Iio_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ AntitoneOn f (Iic b)
have refine_1 : DifferentiableOn ℝ f (interior (Iic b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
⊢ AntitoneOn f (Iic b)
have refine_1₁ : ∀ x ∈ interior (Iic b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ MonotoneOn f (Ico b c)
have refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
⊢ MonotoneOn f (Ico b c)
have refine_2₁ : ∀ x ∈ interior (Ico b c), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ IsMinOn f (Iic c) b
have refine_1 : AntitoneOn f (Iic b)
Tactic: refine isMinOn_Iic_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Iic b)
⊢ IsMinOn f (Iic c) b
have refine_2 : MonotoneOn f (Icc b c)
Tactic: refine isMinOn_Iic_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ AntitoneOn f (Iic b)
have refine_1 : DifferentiableOn ℝ f (interior (Iic b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
⊢ AntitoneOn f (Iic b)
have refine_1₁ : ∀ x ∈ interior (Iic b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ MonotoneOn f (Icc b c)
have refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
⊢ MonotoneOn f (Icc b c)
have refine_2₁ : ∀ x ∈ interior (Icc b c), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ IsMinOn f univ b
have refine_1 : AntitoneOn f (Iic b)
Tactic: refine isMinOn_univ_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Iic b)
⊢ IsMinOn f univ b
have refine_2 : MonotoneOn f (Ici b)
Tactic: refine isMinOn_univ_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ AntitoneOn f (Iic b)
have refine_1 : DifferentiableOn ℝ f (interior (Iic b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
⊢ AntitoneOn f (Iic b)
have refine_1₁ : ∀ x ∈ interior (Iic b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ MonotoneOn f (Ici b)
have refine_2 : DifferentiableOn ℝ f (interior (Ici b))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
⊢ MonotoneOn f (Ici b)
have refine_2₁ : ∀ x ∈ interior (Ici b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
⊢ IsLocalMax f b
have obtain : ∀ (a : ℝ) (ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x), IsLocalMax f b
Tactic: obtain ⟨a, ha⟩ := (nhdsLT_basis b).eventually_iff.mp <| hd₀.and h₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x
⊢ IsLocalMax f b
have obtain : ∀ (c : ℝ) (hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0), IsLocalMax f b
Tactic: obtain ⟨c, hc⟩ := (nhdsGT_basis b).eventually_iff.mp <| hd₁.and h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
⊢ IsLocalMin f b
have obtain : ∀ (a : ℝ) (ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0), IsLocalMin f b
Tactic: obtain ⟨a, ha⟩ := (nhdsLT_basis b).eventually_iff.mp <| hd₀.and h₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
⊢ IsLocalMin f b
have obtain : ∀ (c : ℝ) (hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≥ 0), IsLocalMin f b
Tactic: obtain ⟨c, hc⟩ := (nhdsGT_basis b).eventually_iff.mp <| hd₁.and h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
⊢ ∀ᶠ (x : ℝ) in 𝓝 x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have rw : (∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)) ∧
  ∀ᶠ (x : ℝ) in pure x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
Tactic: rw [← nhdsNE_sup_pure x₀, eventually_sup]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
⊢ (∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)) ∧
    ∀ᶠ (x : ℝ) in pure x₀,
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have refine : ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
Tactic: refine ⟨?_, by simpa⟩