-- Mathlib/Analysis/Calculus/Darboux.lean
theorem Set.OrdConnected.image_hasDerivWithinAt {s : Set ℝ} (hs : OrdConnected s)
    (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) : OrdConnected (f' '' s)

Proof state:
case hs.intro.intro.intro.intro.intro.inl.intro.intro
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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 : f' c = m
⊢ m ∈ f' '' s

Tactic:
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩

Result:
no goals

Proof state:
case hs.intro.intro.intro.intro.intro.inl
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Tactic:
rcases exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x <| this hx).mono this) hma
    hmb with
  ⟨c, cmem, hc⟩

Result:
case hs.intro.intro.intro.intro.intro.inl.intro.intro
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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 : f' c = m
⊢ m ∈ f' '' s

Proof state:
case hs.intro.intro.intro.intro.intro.inl
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Tactic:
have : Icc a b ⊆ s := hs.out ha hb

Result:
case hs.intro.intro.intro.intro.intro.inl
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Proof state:
case hs.intro.intro.intro.intro.intro
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Tactic:
rcases le_total a b with hab | hab

Result:
case hs.intro.intro.intro.intro.intro.inl
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

case hs.intro.intro.intro.intro.intro.inr
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Proof state:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ (f' '' s).OrdConnected

Tactic:
apply ordConnected_of_Ioo

Result:
case hs
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ ∀ x ∈ f' '' s, ∀ y ∈ f' '' s, x < y → Ioo x y ⊆ f' '' s

Proof state:
case hs.intro.intro.intro.intro.intro.inr
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Tactic:
rcases exists_hasDerivWithinAt_eq_of_lt_of_gt hab (fun x hx => (hf x <| this hx).mono this) hmb
    hma with
  ⟨c, cmem, hc⟩

Result:
case hs.intro.intro.intro.intro.intro.inr.intro.intro
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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 : f' c = m
⊢ m ∈ f' '' s

Proof state:
case hs.intro.intro.intro.intro.intro.inr
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Tactic:
have : Icc b a ⊆ s := hs.out hb ha

Result:
case hs.intro.intro.intro.intro.intro.inr
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Proof state:
case hs
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ ∀ x ∈ f' '' s, ∀ y ∈ f' '' s, x < y → Ioo x y ⊆ f' '' s

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ - m ⟨hma, hmb⟩

Result:
case hs.intro.intro.intro.intro.intro
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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

Proof state:
case hs.intro.intro.intro.intro.intro.inr.intro.intro
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ 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 : f' c = m
⊢ m ∈ f' '' s

Tactic:
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩

Result:
no goals