a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
m : ℝ
hf' : (∃ x, x ∈ s ∧ m ≤ f' x) ∧ ∃ x, x ∈ s ∧ f' x ≤ m
⊢ ∃ x, x ∈ s ∧ f' x = m
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
m : ℝ
hf' : ∀ (x : ℝ), x ∈ s → f' x ≠ m
⊢ (∀ (x : ℝ), x ∈ s → f' x < m) ∨ ∀ (x : ℝ), x ∈ s → m < f' x
contrapose! hf'
case intro.intro.intro.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x, x ∈ s ∧ f' x = m
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
m : ℝ
hf' : (∃ x, x ∈ s ∧ m ≤ f' x) ∧ ∃ x, x ∈ s ∧ f' x ≤ m
⊢ ∃ x, x ∈ s ∧ f' x = m
rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩
no goals
case intro.intro.intro.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x, x ∈ s ∧ f' x = m
exact (convex_image_hasDerivAt hs hf).ordConnected.out
  (mem_image_of_mem f' ha) (mem_image_of_mem f' hb) ⟨hma, hmb⟩