awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
refine_1 : DifferentiableOn ℝ f' (interior D)
⊢ DifferentiableOn ℝ (deriv f) (interior D)

Tactic:
rw [differentiableOn_congr this]

Premises used: differentiableOn_congr
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
⊢ DifferentiableOn ℝ f' (interior D)

Tactic:
fun x hx ↦ (hf'' _ hx).differentiableWithinAt

Premises used: HasDerivWithinAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
⊢ DifferentiableOn ℝ f' (interior D)

Tactic:
exact fun x hx ↦ (hf'' _ hx).differentiableWithinAt

Premises used: HasDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ f'' x

Tactic:
hf''₀ _ hx
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
h : deriv^[2] f x = f'' x
⊢ 0 ≤ deriv^[2] f x

Tactic:
convert! hf''₀ _ hx using 1
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
rw : ∀ (y : ℝ) (hy : y ∈ interior D), HasDerivWithinAt (deriv f) (f'' y) (interior D) y
⊢ deriv (deriv f) x = f'' x

Tactic:
rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]

Premises used: isOpen_interior, deriv_eqOn
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
rw rw₁ : f' y = f' y
⊢ deriv f y = f' y

Tactic:
rw [this hy]
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ HasDerivWithinAt (deriv f) (f'' y) (interior D) y

Tactic:
exact (hf'' _ hy).congr this <| by rw [this hy]

Premises used: HasDerivWithinAt.congr
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
⊢ EqOn (deriv f) f' (interior D)

Tactic:
have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
⊢ ConcaveOn ℝ D f

Tactic:
concaveOn_of_deriv2_nonpos hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_

Premises used: HasDerivWithinAt.differentiableWithinAt, concaveOn_of_deriv2_nonpos
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
refine_1 : DifferentiableOn ℝ (deriv f) (interior D)
refine_2 : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ ConcaveOn ℝ D f

Tactic:
refine concaveOn_of_deriv2_nonpos hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_

Premises used: HasDerivWithinAt.differentiableWithinAt, concaveOn_of_deriv2_nonpos
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
refine_1 : DifferentiableOn ℝ f' (interior D)
⊢ DifferentiableOn ℝ (deriv f) (interior D)

Tactic:
rw [differentiableOn_congr this]

Premises used: differentiableOn_congr
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
⊢ DifferentiableOn ℝ f' (interior D)

Tactic:
fun x hx ↦ (hf'' _ hx).differentiableWithinAt

Premises used: HasDerivWithinAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
⊢ DifferentiableOn ℝ f' (interior D)

Tactic:
exact fun x hx ↦ (hf'' _ hx).differentiableWithinAt

Premises used: HasDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
⊢ f'' x ≤ 0

Tactic:
hf''₀ _ hx
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
h : deriv^[2] f x = f'' x
⊢ deriv^[2] f x ≤ 0

Tactic:
convert! hf''₀ _ hx using 1
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
rw : ∀ (y : ℝ) (hy : y ∈ interior D), HasDerivWithinAt (deriv f) (f'' y) (interior D) y
⊢ deriv (deriv f) x = f'' x

Tactic:
rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]

Premises used: isOpen_interior, deriv_eqOn
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
rw rw₁ : f' y = f' y
⊢ deriv f y = f' y

Tactic:
rw [this hy]
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ HasDerivWithinAt (deriv f) (f'' y) (interior D) y

Tactic:
exact (hf'' _ hy).congr this <| by rw [this hy]

Premises used: HasDerivWithinAt.congr
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, 0 < deriv^[2] f x
rwa rwa₁ rwa₂ rwa₃ : ∀ x ∈ interior D, 0 < deriv (deriv f) x
⊢ ∀ x ∈ interior (interior D), 0 < deriv (deriv f) x

Tactic:
rwa [interior_interior]

Premises used: interior_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0
rwa rwa₁ rwa₂ rwa₃ : ∀ x ∈ interior D, deriv (deriv f) x < 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x < 0

Tactic:
rwa [interior_interior]

Premises used: interior_interior
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf' : DifferentiableOn ℝ f D
hf'' : DifferentiableOn ℝ (deriv f) D
hf''_nonneg : ∀ x ∈ D, 0 ≤ deriv^[2] f x
⊢ ConvexOn ℝ D f

Tactic:
convexOn_of_deriv2_nonneg hD hf'.continuousOn (hf'.mono interior_subset)
    (hf''.mono interior_subset) fun x hx => hf''_nonneg x (interior_subset hx)

Premises used: interior_subset, DifferentiableOn.continuousOn, convexOn_of_deriv2_nonneg, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf' : DifferentiableOn ℝ f D
hf'' : DifferentiableOn ℝ (deriv f) D
hf''_nonpos : ∀ x ∈ D, deriv^[2] f x ≤ 0
⊢ ConcaveOn ℝ D f

Tactic:
concaveOn_of_deriv2_nonpos hD hf'.continuousOn (hf'.mono interior_subset)
    (hf''.mono interior_subset) fun x hx => hf''_nonpos x (interior_subset hx)

Premises used: interior_subset, DifferentiableOn.continuousOn, concaveOn_of_deriv2_nonpos, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ D, 0 < deriv^[2] f x
⊢ StrictConvexOn ℝ D f

Tactic:
strictConvexOn_of_deriv2_pos hD hf fun x hx => hf'' x (interior_subset hx)

Premises used: interior_subset, strictConvexOn_of_deriv2_pos
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ D, deriv^[2] f x < 0
⊢ StrictConcaveOn ℝ D f

Tactic:
strictConcaveOn_of_deriv2_neg hD hf fun x hx => hf'' x (interior_subset hx)

Premises used: interior_subset, strictConcaveOn_of_deriv2_neg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
f : ℝ → ℝ
hf' : Differentiable ℝ f
hf'' : Differentiable ℝ (deriv f)
hf''_nonneg : ∀ (x : ℝ), 0 ≤ deriv^[2] f x
⊢ ConvexOn ℝ univ f

Tactic:
convexOn_of_deriv2_nonneg' convex_univ hf'.differentiableOn hf''.differentiableOn fun x _ =>
    hf''_nonneg x

Premises used: convexOn_of_deriv2_nonneg', convex_univ, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
f : ℝ → ℝ
hf' : Differentiable ℝ f
hf'' : Differentiable ℝ (deriv f)
hf''_nonpos : ∀ (x : ℝ), deriv^[2] f x ≤ 0
⊢ ConcaveOn ℝ univ f

Tactic:
concaveOn_of_deriv2_nonpos' convex_univ hf'.differentiableOn hf''.differentiableOn fun x _ =>
    hf''_nonpos x

Premises used: concaveOn_of_deriv2_nonpos', convex_univ, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
f : ℝ → ℝ
hf : Continuous f
hf'' : ∀ (x : ℝ), 0 < deriv^[2] f x
⊢ StrictConvexOn ℝ univ f

Tactic:
strictConvexOn_of_deriv2_pos' convex_univ hf.continuousOn fun x _ => hf'' x

Premises used: Continuous.continuousOn, convex_univ, strictConvexOn_of_deriv2_pos'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
f : ℝ → ℝ
hf : Continuous f
hf'' : ∀ (x : ℝ), deriv^[2] f x < 0
⊢ StrictConcaveOn ℝ univ f

Tactic:
strictConcaveOn_of_deriv2_neg' convex_univ hf.continuousOn fun x _ => hf'' x

Premises used: Continuous.continuousOn, convex_univ, strictConcaveOn_of_deriv2_neg'
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConvexOn 𝕜 s f
hx : x ∈ s
⊢ MonotoneOn (slope f x) (s \ {x})

Tactic:
(slope_fun_def_field f _).symm ▸ fun _ hy _ hz hz' ↦ hfc.secant_mono hx (mem_of_mem_diff hy)
    (mem_of_mem_diff hz) (notMem_of_mem_diff hy :) (notMem_of_mem_diff hz :) hz'

Premises used: Eq.rec, Set.mem_of_mem_diff, ConvexOn.secant_mono, Set.notMem_of_mem_diff, slope_fun_def_field, Eq.symm
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ s
⊢ MonotoneOn (slope f x) {y : 𝕜 | y ∈ s ∧ x < y}

Tactic:
(hfc.slope_mono hxs).mono fun _ ⟨h1, h2⟩ ↦ ⟨h1, h2.ne'⟩

Premises used: _private.0.ConvexOn.monotoneOn_slope_gt.match_1, Membership.mem, ConvexOn.slope_mono, LT.lt.ne', SDiff.sdiff, And.intro, Singleton.singleton, MonotoneOn.mono
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ s
⊢ MonotoneOn (slope f x) {y : 𝕜 | y ∈ s ∧ y < x}

Tactic:
(hfc.slope_mono hxs).mono fun _ ⟨h1, h2⟩ ↦ ⟨h1, h2.ne⟩

Premises used: _private.0.ConvexOn.monotoneOn_slope_lt.match_1, Membership.mem, ConvexOn.slope_mono, SDiff.sdiff, And.intro, Singleton.singleton, LT.lt.ne, MonotoneOn.mono
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hx : x ∈ s
rw : AntitoneOn ((-slope (-f)) x) (s \ {x})
⊢ AntitoneOn (slope f x) (s \ {x})

Tactic:
rw [← neg_neg f, slope_neg_fun]

Premises used: slope_neg_fun, neg_neg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hx : x ∈ s
⊢ AntitoneOn ((-slope (-f)) x) (s \ {x})

Tactic:
(ConvexOn.slope_mono hfc.neg hx).neg

Premises used: MonotoneOn.neg, ConvexOn.slope_mono, ConcaveOn.neg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hx : x ∈ s
⊢ AntitoneOn ((-slope (-f)) x) (s \ {x})

Tactic:
exact (ConvexOn.slope_mono hfc.neg hx).neg

Premises used: MonotoneOn.neg, ConvexOn.slope_mono, ConcaveOn.neg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hxs : x ∈ s
⊢ AntitoneOn (slope f x) {y : 𝕜 | y ∈ s ∧ x < y}

Tactic:
(hfc.slope_anti hxs).mono fun _ ⟨h1, h2⟩ ↦ ⟨h1, h2.ne'⟩

Premises used: _private.0.ConvexOn.monotoneOn_slope_gt.match_1, Membership.mem, ConcaveOn.slope_anti, AntitoneOn.mono, LT.lt.ne', SDiff.sdiff, And.intro, Singleton.singleton
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hxs : x ∈ s
⊢ AntitoneOn (slope f x) {y : 𝕜 | y ∈ s ∧ y < x}

Tactic:
(hfc.slope_anti hxs).mono fun _ ⟨h1, h2⟩ ↦ ⟨h1, h2.ne⟩

Premises used: _private.0.ConvexOn.monotoneOn_slope_lt.match_1, Membership.mem, ConcaveOn.slope_anti, AntitoneOn.mono, SDiff.sdiff, And.intro, Singleton.singleton, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
⊢ ∃ y < x, y ∈ s

Tactic:
Eventually.exists_lt (mem_interior_iff_mem_nhds.mp hxs)

Premises used: mem_interior_iff_mem_nhds, Iff.mp, Filter.Eventually.exists_lt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
obtain : ∀ (y : 𝕜) (hyx : y < x) (hys : y ∈ s), BddBelow (slope f x '' {y : 𝕜 | y ∈ s ∧ x < y})
⊢ BddBelow (slope f x '' {y : 𝕜 | y ∈ s ∧ x < y})

Tactic:
obtain ⟨y, hyx, hys⟩ : ∃ y, y < x ∧ y ∈ s :=
    Eventually.exists_lt (mem_interior_iff_mem_nhds.mp hxs)

Premises used: mem_interior_iff_mem_nhds, Iff.mp, Filter.Eventually.exists_lt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
⊢ BddBelow (slope f x '' {y : 𝕜 | y ∈ s ∧ x < y})

Tactic:
bddBelow_iff_subset_Ici.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩

Premises used: Iff.mpr, Set.Ici, Membership.mem, slope, _private.0.bddBelow_slope_lt_of_mem_interior.match_1, bddBelow_iff_subset_Ici, Exists.intro
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
refine :
  ∀ y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y},
    ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z) (hz' : slope f x z = y'),
      y' ∈ Ici (slope f x y)
⊢ BddBelow (slope f x '' {y : 𝕜 | y ∈ s ∧ x < y})

Tactic:
refine bddBelow_iff_subset_Ici.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z
hz' : slope f x z = y'
simp_rw : slope f x y ≤ slope f x z
⊢ y' ∈ Ici (slope f x y)

Tactic:
simp_rw [mem_Ici, ← hz']

Premises used: Set.mem_Ici
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z
hz' : slope f x z = y'
⊢ slope f x y ≤ slope f x z

Tactic:
hfc.slope_mono (interior_subset hxs) ?_ ?_ (hyx.trans hz.2).le

Premises used: interior_subset, LT.lt.le, ConvexOn.slope_mono, And.right, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z
hz' : slope f x z = y'
refine_1 : y ∈ s \ {x}
refine_2 : z ∈ s \ {x}
⊢ slope f x y ≤ slope f x z

Tactic:
refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hyx.trans hz.2).le

Premises used: interior_subset, LT.lt.le, ConvexOn.slope_mono, And.right, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z
hz' : slope f x z = y'
⊢ y ∈ s \ {x}

Tactic:
simp [hys, hyx.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : y < x
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ x < y}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ x < y} z
hz' : slope f x z = y'
⊢ z ∈ s \ {x}

Tactic:
simp [hz.2.ne', hz.1]

Premises used: LT.lt.ne', And.right, And.left
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
⊢ ∃ (y : 𝕜), x < y ∧ y ∈ s

Tactic:
Eventually.exists_gt (mem_interior_iff_mem_nhds.mp hxs)

Premises used: mem_interior_iff_mem_nhds, Iff.mp, Filter.Eventually.exists_gt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
obtain : ∀ (y : 𝕜) (hyx : x < y) (hys : y ∈ s), BddAbove (slope f x '' {y : 𝕜 | y ∈ s ∧ y < x})
⊢ BddAbove (slope f x '' {y : 𝕜 | y ∈ s ∧ y < x})

Tactic:
obtain ⟨y, hyx, hys⟩ : ∃ y, x < y ∧ y ∈ s :=
    Eventually.exists_gt (mem_interior_iff_mem_nhds.mp hxs)

Premises used: mem_interior_iff_mem_nhds, Iff.mp, Filter.Eventually.exists_gt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
⊢ BddAbove (slope f x '' {y : 𝕜 | y ∈ s ∧ y < x})

Tactic:
bddAbove_iff_subset_Iic.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩

Premises used: Iff.mpr, _private.0.bddAbove_slope_gt_of_mem_interior.match_1, Membership.mem, bddAbove_iff_subset_Iic, slope, Exists.intro, Set.Iic
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
refine :
  ∀ y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ y < x},
    ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ y < x} z) (hz' : slope f x z = y'),
      y' ∈ Iic (slope f x y)
⊢ BddAbove (slope f x '' {y : 𝕜 | y ∈ s ∧ y < x})

Tactic:
refine bddAbove_iff_subset_Iic.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ y < x}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ y < x} z
hz' : slope f x z = y'
simp_rw : slope f x z ≤ slope f x y
⊢ y' ∈ Iic (slope f x y)

Tactic:
simp_rw [mem_Iic, ← hz']

Premises used: Set.mem_Iic
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
h : y' ∈ slope f x '' {y : 𝕜 | y ∈ s ∧ y < x}
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {y : 𝕜 | y ∈ s ∧ y < x} z
hz' : slope f x z = y'
⊢ slope f x z ≤ slope f x y

Tactic:
hfc.slope_mono (interior_subset hxs) ?_ ?_ (hz.2.trans hyx).le

Premises used: interior_subset, LT.lt.le, ConvexOn.slope_mono, And.right, LT.lt.trans