awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
refine_1₁ : ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x
⊢ MonotoneOn f (Icc a b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Icc a b) (continuousOn_Icc ha hb 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Icc a b), 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
refine_2₁ : ∀ x ∈ interior (Icc b c), deriv f x ≤ 0
⊢ AntitoneOn f (Icc b c)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Icc b c) (continuousOn_Icc hb hc 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Icc b c), 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ IsMaxOn f (Ioi a) b

Tactic:
isMaxOn_Ioi_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ioi_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : MonotoneOn f (Ioc a b)
refine_2 : AntitoneOn f (Ici b)
⊢ IsMaxOn f (Ioi a) b

Tactic:
refine isMaxOn_Ioi_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ioi_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
refine_1₁ : ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x
⊢ MonotoneOn f (Ioc a b)

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

Premises used: monotoneOn_of_deriv_nonneg, convex_Ioc, _private.0.continuousOn_Ioc
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ioc a b), 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
refine_2₁ : ∀ x ∈ interior (Ici b), deriv f x ≤ 0
⊢ AntitoneOn f (Ici b)

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

Premises used: convex_Ici, _private.0.continuousOn_Ici, 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ici 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ IsMaxOn f (Ici a) b

Tactic:
isMaxOn_Ici_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ici_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : MonotoneOn f (Icc a b)
refine_2 : AntitoneOn f (Ici b)
⊢ IsMaxOn f (Ici a) b

Tactic:
refine isMaxOn_Ici_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ici_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
refine_1₁ : ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x
⊢ MonotoneOn f (Icc a b)

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

Premises used: _private.0.continuousOn_Icc, monotoneOn_of_deriv_nonneg, convex_Icc
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Icc a 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
refine_2₁ : ∀ x ∈ interior (Ici b), deriv f x ≤ 0
⊢ AntitoneOn f (Ici b)

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

Premises used: convex_Ici, _private.0.continuousOn_Ici, 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ici 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Iio c) b

Tactic:
isMaxOn_Iio_of_mono_anti ?_ ?_

Premises used: isMaxOn_Iio_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Iic b)
refine_2 : AntitoneOn f (Ico b c)
⊢ IsMaxOn f (Iio c) b

Tactic:
refine isMaxOn_Iio_of_mono_anti ?_ ?_

Premises used: isMaxOn_Iio_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
refine_1₁ : ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
⊢ MonotoneOn f (Iic b)

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

Premises used: convex_Iic, _private.0.continuousOn_Iic, monotoneOn_of_deriv_nonneg
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Iic 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
refine_2₁ : ∀ x ∈ interior (Ico b c), deriv f x ≤ 0
⊢ AntitoneOn f (Ico b c)

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

Premises used: convex_Ico, _private.0.continuousOn_Ico, 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ico b c), 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Iic c) b

Tactic:
isMaxOn_Iic_of_mono_anti ?_ ?_

Premises used: isMaxOn_Iic_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Iic b)
refine_2 : AntitoneOn f (Icc b c)
⊢ IsMaxOn f (Iic c) b

Tactic:
refine isMaxOn_Iic_of_mono_anti ?_ ?_

Premises used: isMaxOn_Iic_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
refine_1₁ : ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
⊢ MonotoneOn f (Iic b)

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

Premises used: convex_Iic, _private.0.continuousOn_Iic, monotoneOn_of_deriv_nonneg
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Iic b), 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
refine_2₁ : ∀ x ∈ interior (Icc b c), deriv f x ≤ 0
⊢ AntitoneOn f (Icc b c)

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

Premises used: _private.0.continuousOn_Icc, convex_Icc, 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Icc b c), 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ IsMaxOn f univ b

Tactic:
isMaxOn_univ_of_mono_anti ?_ ?_

Premises used: isMaxOn_univ_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : MonotoneOn f (Iic b)
refine_2 : AntitoneOn f (Ici b)
⊢ IsMaxOn f univ b

Tactic:
refine isMaxOn_univ_of_mono_anti ?_ ?_

Premises used: isMaxOn_univ_of_mono_anti
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Iic b))
refine_1₁ : ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
⊢ MonotoneOn f (Iic b)

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

Premises used: convex_Iic, _private.0.continuousOn_Iic, monotoneOn_of_deriv_nonneg
-- 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Iic b), 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ici b))
refine_2₁ : ∀ x ∈ interior (Ici b), deriv f x ≤ 0
⊢ AntitoneOn f (Ici b)

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

Premises used: convex_Ici, _private.0.continuousOn_Ici, 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ 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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ici b), deriv f x ≤ 0

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, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsLocalMax f b

Tactic:
(isMaxOn_Ioo_of_deriv h hd₀ hd₁ h₀ h₁).isLocalMax (Ioo_mem_nhds g₀ g₁)

Premises used: IsMaxOn.isLocalMax, Ioo_mem_nhds, isMaxOn_Ioo_of_deriv
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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

Tactic:
isMinOn_Ioo_of_anti_mono ?_ ?_

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

Tactic:
refine isMinOn_Ioo_of_anti_mono ?_ ?_

Premises used: isMinOn_Ioo_of_anti_mono
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
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))
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 h hd₀)

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

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

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

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

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

Tactic:
simp_all
-- 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
⊢ IsMinOn f (Ioc a c) b

Tactic:
isMinOn_Ioc_of_anti_mono ?_ ?_

Premises used: isMinOn_Ioc_of_anti_mono
-- 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
refine_1 : AntitoneOn f (Ioc a b)
refine_2 : MonotoneOn f (Icc b c)
⊢ IsMinOn f (Ioc a c) b

Tactic:
refine isMinOn_Ioc_of_anti_mono ?_ ?_

Premises used: isMinOn_Ioc_of_anti_mono
-- 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
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 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
⊢ DifferentiableOn ℝ f (interior (Ioc a b))

Tactic:
simp_all
-- 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 (Ioc a b), deriv f x ≤ 0

Tactic:
simp_all
-- 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
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 : ℝ
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