[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
rcases hab.eq_or_lt with (rfl | hab')
[GOAL]
case inl
a : ℝ
f f' : ℝ → ℝ
m : ℝ
hma : f' a < m
hab : a ≤ a
hf : ∀ (x : ℝ), x ∈ Icc a a → HasDerivWithinAt f (f' x) (Icc a a) x
hmb : m < f' a
⊢ m ∈ f' '' Ioo a a
[PROOFSTEP]
exact (lt_asymm hma hmb).elim
[GOAL]
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
set g : ℝ → ℝ := fun x => f x - m * x
[GOAL]
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
have hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x :=
  by
  intro x hx
  simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
⊢ ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
[PROOFSTEP]
intro x hx
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
x : ℝ
hx : x ∈ Icc a b
⊢ HasDerivWithinAt g (f' x - m) (Icc a b) x
[PROOFSTEP]
simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)
[GOAL]
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Icc a b, IsMinOn g (Icc a b) c
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
⊢ ∃ c, c ∈ Icc a b ∧ IsMinOn g (Icc a b) c
case inr.intro.intro
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
exact isCompact_Icc.exists_forall_le (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt
[GOAL]
case inr.intro.intro
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
have cmem' : c ∈ Ioo a b :=
  by
  rcases cmem.1.eq_or_lt with
    (rfl | hac)
      -- Show that `c` can't be equal to `a`
  · refine' absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right _ (sub_pos.2 hab')) (not_le_of_lt hma)
    have : b - a ∈ posTangentConeAt (Icc a b) a :=
      mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.refl _)
    simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
      hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
  rcases cmem.2.eq_or_gt with
    (rfl | hcb)
      -- Show that `c` can't be equal to `b`
  · refine' absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right _ (sub_lt_zero.2 hab')) (not_le_of_lt hmb)
    have : a - b ∈ posTangentConeAt (Icc a b) b :=
      mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
    simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
      hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
  exact ⟨hac, hcb⟩
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
⊢ c ∈ Ioo a b
[PROOFSTEP]
rcases cmem.1.eq_or_lt with
  (rfl | hac)
    -- Show that `c` can't be equal to `a`
[GOAL]
case inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ a ∈ Ioo a b
[PROOFSTEP]
refine' absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right _ (sub_pos.2 hab')) (not_le_of_lt hma)
[GOAL]
case inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ 0 ≤ (b - a) * (f' a - m)
[PROOFSTEP]
have : b - a ∈ posTangentConeAt (Icc a b) a :=
  mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.refl _)
[GOAL]
case inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
this : b - a ∈ posTangentConeAt (Icc a b) a
⊢ 0 ≤ (b - a) * (f' a - m)
[PROOFSTEP]
simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
  hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
[GOAL]
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
⊢ c ∈ Ioo a b
[PROOFSTEP]
rcases cmem.2.eq_or_gt with
  (rfl | hcb)
    -- Show that `c` can't be equal to `b`
[GOAL]
case inr.inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ b ∈ Ioo a b
[PROOFSTEP]
refine' absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right _ (sub_lt_zero.2 hab')) (not_le_of_lt hmb)
[GOAL]
case inr.inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ 0 ≤ (a - b) * (f' b - m)
[PROOFSTEP]
have : a - b ∈ posTangentConeAt (Icc a b) b :=
  mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ segment ℝ b a ⊆ Icc a b
[PROOFSTEP]
rw [segment_symm, segment_eq_Icc hab]
[GOAL]
case inr.inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
this : a - b ∈ posTangentConeAt (Icc a b) b
⊢ 0 ≤ (a - b) * (f' b - m)
[PROOFSTEP]
simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
  hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
[GOAL]
case inr.inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
hcb : c < b
⊢ c ∈ Ioo a b
[PROOFSTEP]
exact ⟨hac, hcb⟩
[GOAL]
case inr.intro.intro
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
use c, cmem'
[GOAL]
case right
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ f' c = m
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
case right
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ f' c - m = 0
[PROOFSTEP]
have : Icc a b ∈ 𝓝 c := by rwa [← mem_interior_iff_mem_nhds, interior_Icc]
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 c
[PROOFSTEP]
rwa [← mem_interior_iff_mem_nhds, interior_Icc]
[GOAL]
case right
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
this : Icc a b ∈ 𝓝 c
⊢ f' c - m = 0
[PROOFSTEP]
exact (hc.isLocalMin this).hasDerivAt_eq_zero ((hg c cmem).hasDerivAt this)
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
⊢ OrdConnected (f' '' s)
[PROOFSTEP]
apply ordConnected_of_Ioo
[GOAL]
case hs
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
⊢ ∀ (x : ℝ), x ∈ f' '' s → ∀ (y : ℝ), y ∈ f' '' s → x < y → Ioo x y ⊆ f' '' s
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ - m ⟨hma, hmb⟩
[GOAL]
case hs.intro.intro.intro.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' s
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case hs.intro.intro.intro.intro.intro.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
⊢ m ∈ f' '' s
[PROOFSTEP]
have : Icc a b ⊆ s := hs.out ha hb
[GOAL]
case hs.intro.intro.intro.intro.intro.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
⊢ m ∈ f' '' s
[PROOFSTEP]
rcases exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x <| this hx).mono this) hma hmb with ⟨c, cmem, hc⟩
[GOAL]
case hs.intro.intro.intro.intro.intro.inl.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
c : ℝ
cmem : c ∈ Ioo a b
hc : (fun x => f' x) c = m
⊢ m ∈ f' '' s
[PROOFSTEP]
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
[GOAL]
case hs.intro.intro.intro.intro.intro.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
⊢ m ∈ f' '' s
[PROOFSTEP]
have : Icc b a ⊆ s := hs.out hb ha
[GOAL]
case hs.intro.intro.intro.intro.intro.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
⊢ m ∈ f' '' s
[PROOFSTEP]
rcases exists_hasDerivWithinAt_eq_of_lt_of_gt hab (fun x hx => (hf x <| this hx).mono this) hmb hma with ⟨c, cmem, hc⟩
[GOAL]
case hs.intro.intro.intro.intro.intro.inr.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
c : ℝ
cmem : c ∈ Ioo b a
hc : (fun x => f' x) c = m
⊢ m ∈ f' '' s
[PROOFSTEP]
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : ∀ (x : ℝ), x ∈ s → f' x ≠ m
⊢ (∀ (x : ℝ), x ∈ s → f' x < m) ∨ ∀ (x : ℝ), x ∈ s → m < f' x
[PROOFSTEP]
contrapose! hf'
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : (∃ x, x ∈ s ∧ m ≤ f' x) ∧ ∃ x, x ∈ s ∧ f' x ≤ m
⊢ ∃ x, x ∈ s ∧ f' x = m
[PROOFSTEP]
rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x, x ∈ s ∧ f' x = m
[PROOFSTEP]
exact (hs.ordConnected.image_hasDerivWithinAt hf).out (mem_image_of_mem f' ha) (mem_image_of_mem f' hb) ⟨hma, hmb⟩
