awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Icc b c), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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

Tactic:
isMinOn_Ico_of_anti_mono ?_ ?_

Premises used: isMinOn_Ico_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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)
refine_2 : MonotoneOn f (Ico b c)
⊢ IsMinOn f (Ico a c) b

Tactic:
refine isMinOn_Ico_of_anti_mono ?_ ?_

Premises used: isMinOn_Ico_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_1₁ : ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
⊢ AntitoneOn f (Icc a b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)

Premises used: _private.0.continuousOn_Icc, convex_Icc, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Icc a b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Icc a b), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_2₁ : ∀ x ∈ interior (Ico b c), 0 ≤ deriv f x
⊢ MonotoneOn f (Ico b c)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico hb hd₁)

Premises used: convex_Ico, monotoneOn_of_deriv_nonneg, _private.0.continuousOn_Ico
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Ico b c))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Ico b c), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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

Tactic:
isMinOn_Icc_of_anti_mono ?_ ?_

Premises used: isMinOn_Icc_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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)
refine_2 : MonotoneOn f (Icc b c)
⊢ IsMinOn f (Icc a c) b

Tactic:
refine isMinOn_Icc_of_anti_mono ?_ ?_

Premises used: isMinOn_Icc_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_1₁ : ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
⊢ AntitoneOn f (Icc a b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)

Premises used: _private.0.continuousOn_Icc, convex_Icc, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Icc a b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Icc a b), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_2₁ : ∀ x ∈ interior (Icc b c), 0 ≤ deriv f x
⊢ MonotoneOn f (Icc b c)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁)

Premises used: _private.0.continuousOn_Icc, monotoneOn_of_deriv_nonneg, convex_Icc
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Icc b c))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Icc b c), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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

Tactic:
isMinOn_Ioi_of_anti_mono ?_ ?_

Premises used: isMinOn_Ioi_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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)
refine_2 : MonotoneOn f (Ici b)
⊢ IsMinOn f (Ioi a) b

Tactic:
refine isMinOn_Ioi_of_anti_mono ?_ ?_

Premises used: isMinOn_Ioi_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_1₁ : ∀ x ∈ interior (Ioc a b), deriv f x ≤ 0
⊢ AntitoneOn f (Ioc a b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀)

Premises used: convex_Ioc, _private.0.continuousOn_Ioc, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Ioc a b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Ioc a b), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_2₁ : ∀ x ∈ interior (Ici b), 0 ≤ deriv f x
⊢ MonotoneOn f (Ici b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)

Premises used: monotoneOn_of_deriv_nonneg, convex_Ici, _private.0.continuousOn_Ici
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Ici b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Ici b), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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

Tactic:
isMinOn_Ici_of_anti_mono ?_ ?_

Premises used: isMinOn_Ici_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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)
refine_2 : MonotoneOn f (Ici b)
⊢ IsMinOn f (Ici a) b

Tactic:
refine isMinOn_Ici_of_anti_mono ?_ ?_

Premises used: isMinOn_Ici_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_1₁ : ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
⊢ AntitoneOn f (Icc a b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀)

Premises used: _private.0.continuousOn_Icc, convex_Icc, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Icc a b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Icc a b), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_2₁ : ∀ x ∈ interior (Ici b), 0 ≤ deriv f x
⊢ MonotoneOn f (Ici b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)

Premises used: monotoneOn_of_deriv_nonneg, convex_Ici, _private.0.continuousOn_Ici
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Ici b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Ici b), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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

Tactic:
isMinOn_Iio_of_anti_mono ?_ ?_

Premises used: isMinOn_Iio_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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)
refine_2 : MonotoneOn f (Ico b c)
⊢ IsMinOn f (Iio c) b

Tactic:
refine isMinOn_Iio_of_anti_mono ?_ ?_

Premises used: isMinOn_Iio_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_1₁ : ∀ x ∈ interior (Iic b), deriv f x ≤ 0
⊢ AntitoneOn f (Iic b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)

Premises used: convex_Iic, _private.0.continuousOn_Iic, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Iic b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Iic b), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_2₁ : ∀ x ∈ interior (Ico b c), 0 ≤ deriv f x
⊢ MonotoneOn f (Ico b c)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico hb hd₁)

Premises used: convex_Ico, monotoneOn_of_deriv_nonneg, _private.0.continuousOn_Ico
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Ico b c))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Ico b c), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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

Tactic:
isMinOn_Iic_of_anti_mono ?_ ?_

Premises used: isMinOn_Iic_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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)
refine_2 : MonotoneOn f (Icc b c)
⊢ IsMinOn f (Iic c) b

Tactic:
refine isMinOn_Iic_of_anti_mono ?_ ?_

Premises used: isMinOn_Iic_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_1₁ : ∀ x ∈ interior (Iic b), deriv f x ≤ 0
⊢ AntitoneOn f (Iic b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)

Premises used: convex_Iic, _private.0.continuousOn_Iic, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Iic b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Iic b), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_2₁ : ∀ x ∈ interior (Icc b c), 0 ≤ deriv f x
⊢ MonotoneOn f (Icc b c)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁)

Premises used: _private.0.continuousOn_Icc, monotoneOn_of_deriv_nonneg, convex_Icc
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Icc b c))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Icc b c), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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

Tactic:
isMinOn_univ_of_anti_mono ?_ ?_

Premises used: isMinOn_univ_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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)
refine_2 : MonotoneOn f (Ici b)
⊢ IsMinOn f univ b

Tactic:
refine isMinOn_univ_of_anti_mono ?_ ?_

Premises used: isMinOn_univ_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_1₁ : ∀ x ∈ interior (Iic b), deriv f x ≤ 0
⊢ AntitoneOn f (Iic b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀)

Premises used: convex_Iic, _private.0.continuousOn_Iic, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Iic b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Iic b), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
refine_2₁ : ∀ x ∈ interior (Ici b), 0 ≤ deriv f x
⊢ MonotoneOn f (Ici b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁)

Premises used: monotoneOn_of_deriv_nonneg, convex_Ici, _private.0.continuousOn_Ici
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ DifferentiableOn ℝ f (interior (Ici b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
⊢ ∀ x ∈ interior (Ici b), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : 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
⊢ IsLocalMin f b

Tactic:
(isMinOn_Ioo_of_deriv h hd₀ hd₁ h₀ h₁).isLocalMin (Ioo_mem_nhds g₀ g₁)

Premises used: isMinOn_Ioo_of_deriv, IsMinOn.isLocalMin, Ioo_mem_nhds
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
obtain : ∀ (a : ℝ) (ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x), IsLocalMax f b
⊢ IsLocalMax f b

Tactic:
obtain ⟨a, ha⟩ := (nhdsLT_basis b).eventually_iff.mp <| hd₀.and h₀

Premises used: Filter.Eventually.and, nhdsLT_basis, Iff.mp, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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
obtain : ∀ (c : ℝ) (hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0), IsLocalMax f b
⊢ IsLocalMax f b

Tactic:
obtain ⟨c, hc⟩ := (nhdsGT_basis b).eventually_iff.mp <| hd₁.and h₁

Premises used: nhdsGT_basis, Filter.Eventually.and, Iff.mp, Filter.HasBasis.eventually_iff