a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
⊢ ∀ ⦃x : ℝ⦄, x ∈ f' '' s → ∀ ⦃y : ℝ⦄, y ∈ f' '' s → Icc x y ⊆ f' '' s
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
⊢ Convex ℝ (f' '' s)
refine' OrdConnected.convex ⟨_⟩
case intro.intro.intro.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a ≤ m
hmb : m ≤ f' b
⊢ m ∈ f' '' s
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
⊢ ∀ ⦃x : ℝ⦄, x ∈ f' '' s → ∀ ⦃y : ℝ⦄, y ∈ f' '' s → Icc x y ⊆ f' '' s
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ m ⟨hma, hmb⟩
case intro.intro.intro.intro.intro.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb : m ≤ f' b
hma : f' a = m
⊢ m ∈ f' '' s

case intro.intro.intro.intro.intro.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb : m ≤ f' b
hma : f' a < m
⊢ m ∈ f' '' s
case intro.intro.intro.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a ≤ m
hmb : m ≤ f' b
⊢ m ∈ f' '' s
cases' eq_or_lt_of_le hma with hma hma
case intro.intro.intro.intro.intro.inr.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m = f' b
⊢ m ∈ f' '' s

case intro.intro.intro.intro.intro.inr.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' s
case intro.intro.intro.intro.intro.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb : m ≤ f' b
hma : f' a < m
⊢ m ∈ f' '' s
cases' eq_or_lt_of_le hmb with hmb hmb
case intro.intro.intro.intro.intro.inr.inr.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
⊢ m ∈ f' '' s

case intro.intro.intro.intro.intro.inr.inr.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
⊢ m ∈ f' '' s
case intro.intro.intro.intro.intro.inr.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' s
cases' le_total a b with hab hab
no goals
case intro.intro.intro.intro.intro.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb : m ≤ f' b
hma : f' a = m
⊢ m ∈ f' '' s
exact hma ▸ mem_image_of_mem f' ha
no goals
case intro.intro.intro.intro.intro.inr.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m = f' b
⊢ m ∈ f' '' s
exact hmb.symm ▸ mem_image_of_mem f' hb
case intro.intro.intro.intro.intro.inr.inr.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
⊢ m ∈ f' '' s
case intro.intro.intro.intro.intro.inr.inr.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
⊢ m ∈ f' '' s
have : Icc a b ⊆ s := hs.ordConnected.out ha hb
case intro.intro.intro.intro.intro.inr.inr.inl.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
c : ℝ
cmem : c ∈ Icc a b
hc : (fun x => f' x) c = m
⊢ m ∈ f' '' s
case intro.intro.intro.intro.intro.inr.inr.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
⊢ m ∈ f' '' s
rcases exists_hasDerivWithinAt_eq_of_gt_of_lt hab
    (fun x hx => (hf x <| this hx).hasDerivWithinAt) hma hmb with
  ⟨c, cmem, hc⟩
no goals
case intro.intro.intro.intro.intro.inr.inr.inl.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
c : ℝ
cmem : c ∈ Icc a b
hc : (fun x => f' x) c = m
⊢ m ∈ f' '' s
exact ⟨c, this cmem, hc⟩
case intro.intro.intro.intro.intro.inr.inr.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
⊢ m ∈ f' '' s
case intro.intro.intro.intro.intro.inr.inr.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
⊢ m ∈ f' '' s
have : Icc b a ⊆ s := hs.ordConnected.out hb ha
case intro.intro.intro.intro.intro.inr.inr.inr.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
c : ℝ
cmem : c ∈ Icc b a
hc : (fun x => f' x) c = m
⊢ m ∈ f' '' s
case intro.intro.intro.intro.intro.inr.inr.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
⊢ m ∈ f' '' s
rcases exists_hasDerivWithinAt_eq_of_lt_of_gt hab
    (fun x hx => (hf x <| this hx).hasDerivWithinAt) hmb hma with
  ⟨c, cmem, hc⟩
no goals
case intro.intro.intro.intro.intro.inr.inr.inr.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivAt f (f' x) x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma✝ : f' a ≤ m
hmb✝ : m ≤ f' b
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
c : ℝ
cmem : c ∈ Icc b a
hc : (fun x => f' x) c = m
⊢ m ∈ f' '' s
exact ⟨c, this cmem, hc⟩