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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Ioc a c) b
have refine_1 : MonotoneOn f (Ioc a b)
Tactic: refine isMaxOn_Ioc_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Ioc a b)
⊢ IsMaxOn f (Ioc a c) b
have refine_2 : AntitoneOn f (Icc b c)
Tactic: refine isMaxOn_Ioc_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ MonotoneOn f (Ioc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
⊢ MonotoneOn f (Ioc a b)
have refine_1₁ : ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ AntitoneOn f (Icc b c)
have refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
⊢ AntitoneOn f (Icc b c)
have refine_2₁ : ∀ x ∈ interior (Icc b c), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Ico a c) b
have refine_1 : MonotoneOn f (Icc a b)
Tactic: refine isMaxOn_Ico_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Icc a b)
⊢ IsMaxOn f (Ico a c) b
have refine_2 : AntitoneOn f (Ico b c)
Tactic: refine isMaxOn_Ico_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ MonotoneOn f (Icc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
⊢ MonotoneOn f (Icc a b)
have refine_1₁ : ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ AntitoneOn f (Ico b c)
have refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
⊢ AntitoneOn f (Ico b c)
have refine_2₁ : ∀ x ∈ interior (Ico b c), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Icc a c) b
have refine_1 : MonotoneOn f (Icc a b)
Tactic: refine isMaxOn_Icc_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Icc a b)
⊢ IsMaxOn f (Icc a c) b
have refine_2 : AntitoneOn f (Icc b c)
Tactic: refine isMaxOn_Icc_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ MonotoneOn f (Icc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
⊢ MonotoneOn f (Icc a b)
have refine_1₁ : ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ AntitoneOn f (Icc b c)
have refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
⊢ AntitoneOn f (Icc b c)
have refine_2₁ : ∀ x ∈ interior (Icc b c), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ IsMaxOn f (Ioi a) b
have refine_1 : MonotoneOn f (Ioc a b)
Tactic: refine isMaxOn_Ioi_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : MonotoneOn f (Ioc a b)
⊢ IsMaxOn f (Ioi a) b
have refine_2 : AntitoneOn f (Ici b)
Tactic: refine isMaxOn_Ioi_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ MonotoneOn f (Ioc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
⊢ MonotoneOn f (Ioc a b)
have refine_1₁ : ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ AntitoneOn f (Ici b)
have refine_2 : DifferentiableOn ℝ f (interior (Ici b))
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
⊢ AntitoneOn f (Ici b)
have refine_2₁ : ∀ x ∈ interior (Ici b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ IsMaxOn f (Ici a) b
have refine_1 : MonotoneOn f (Icc a b)
Tactic: refine isMaxOn_Ici_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : MonotoneOn f (Icc a b)
⊢ IsMaxOn f (Ici a) b
have refine_2 : AntitoneOn f (Ici b)
Tactic: refine isMaxOn_Ici_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ MonotoneOn f (Icc a b)
have refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
⊢ MonotoneOn f (Icc a b)
have refine_1₁ : ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ AntitoneOn f (Ici b)
have refine_2 : DifferentiableOn ℝ f (interior (Ici b))
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
⊢ AntitoneOn f (Ici b)
have refine_2₁ : ∀ x ∈ interior (Ici b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Iio c) b
have refine_1 : MonotoneOn f (Iic b)
Tactic: refine isMaxOn_Iio_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Iic b)
⊢ IsMaxOn f (Iio c) b
have refine_2 : AntitoneOn f (Ico b c)
Tactic: refine isMaxOn_Iio_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ MonotoneOn f (Iic b)
have refine_1 : DifferentiableOn ℝ f (interior (Iic b))
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
⊢ MonotoneOn f (Iic b)
have refine_1₁ : ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ AntitoneOn f (Ico b c)
have refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
⊢ AntitoneOn f (Ico b c)
have refine_2₁ : ∀ x ∈ interior (Ico b c), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Iic c) b
have refine_1 : MonotoneOn f (Iic b)
Tactic: refine isMaxOn_Iic_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Iic b)
⊢ IsMaxOn f (Iic c) b
have refine_2 : AntitoneOn f (Icc b c)
Tactic: refine isMaxOn_Iic_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ MonotoneOn f (Iic b)
have refine_1 : DifferentiableOn ℝ f (interior (Iic b))
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
⊢ MonotoneOn f (Iic b)
have refine_1₁ : ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ AntitoneOn f (Icc b c)
have refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
⊢ AntitoneOn f (Icc b c)
have refine_2₁ : ∀ x ∈ interior (Icc b c), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ IsMaxOn f univ b
have refine_1 : MonotoneOn f (Iic b)
Tactic: refine isMaxOn_univ_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : MonotoneOn f (Iic b)
⊢ IsMaxOn f univ b
have refine_2 : AntitoneOn f (Ici b)
Tactic: refine isMaxOn_univ_of_mono_anti ?_ ?_
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ MonotoneOn f (Iic b)
have refine_1 : DifferentiableOn ℝ f (interior (Iic b))
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
⊢ MonotoneOn f (Iic b)
have refine_1₁ : ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
Tactic: apply monotoneOn_of_deriv_nonneg (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ AntitoneOn f (Ici b)
have refine_2 : DifferentiableOn ℝ f (interior (Ici b))
Tactic: apply antitoneOn_of_deriv_nonpos (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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
⊢ AntitoneOn f (Ici b)
have refine_2₁ : ∀ x ∈ interior (Ici b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ IsMinOn f (Ioo a c) b
have refine_1 : AntitoneOn f (Ioc a b)
Tactic: refine isMinOn_Ioo_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
refine_1 : AntitoneOn f (Ioc a b)
⊢ IsMinOn f (Ioo a c) b
have refine_2 : MonotoneOn f (Ico b c)
Tactic: refine isMinOn_Ioo_of_anti_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 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 h hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 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 h hd₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 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 h hd₁)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 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 h 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
⊢ IsMinOn f (Ioc a c) b
have refine_1 : AntitoneOn f (Ioc a b)
Tactic: refine isMinOn_Ioc_of_anti_mono ?_ ?_