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' '' Icc a b
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' '' Icc a b
have hab' : a < b := by
  refine' lt_of_le_of_ne hab fun hab' => _
  subst b
  exact lt_asymm hma hmb
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' '' Icc a b
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' '' Icc a b
set g : ℝ → ℝ := fun x => f x - m * x
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' '' Icc a b
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' '' Icc a b
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)
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 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' '' Icc a b
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' '' Icc a b
obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Icc a b, IsMinOn g (Icc a b) c
case 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' '' Icc a b
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 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' '' Icc a b
exact
  isCompact_Icc.exists_forall_le (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt
case 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
⊢ f' c = m
case 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' '' Icc a b
use c, cmem
case 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
⊢ f' c - m = 0
case 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
⊢ f' c = m
rw [← sub_eq_zero]
case 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
this : Icc a b ∈ 𝓝 c
⊢ f' c - m = 0
case 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
⊢ f' c - m = 0
have : Icc a b ∈ 𝓝 c := by rwa [← mem_interior_iff_mem_nhds, interior_Icc]
no goals
case 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
this : Icc a b ∈ 𝓝 c
⊢ f' c - m = 0
exact (hc.isLocalMin this).hasDerivAt_eq_zero ((hg c cmem).hasDerivAt this)
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
⊢ False
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
⊢ a < b
refine' lt_of_le_of_ne hab fun hab' => _
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
⊢ False
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
⊢ False
subst b
no goals
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
⊢ False
exact lt_asymm hma hmb
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
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
intro x hx
no goals
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
simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)
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
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a = c
⊢ c ∈ Ioo a b

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
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
cases' eq_or_lt_of_le cmem.1 with hac hac
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
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
hbc : c = b
⊢ c ∈ Ioo a b

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
hbc : c < b
⊢ c ∈ Ioo a b
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
cases' eq_or_lt_of_le cmem.2 with hbc hbc
no goals
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
hbc : c < b
⊢ c ∈ Ioo a b
exact ⟨hac, hbc⟩
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
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
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a = c
⊢ c ∈ Ioo a b
subst c
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)
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
refine'
  absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right _ (sub_pos.2 hab')) (not_le_of_lt hma)
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)
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)
have : b - a ∈ posTangentConeAt (Icc a b) a :=
  mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.refl _)
no goals
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)
simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
  hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
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
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
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
hbc : c = b
⊢ c ∈ Ioo a b
subst c
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)
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
refine' absurd
  (sub_nonpos.1 <| nonpos_of_mul_nonneg_right _ (sub_lt_zero.2 hab')) (not_le_of_lt hmb)
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)
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)
have : a - b ∈ posTangentConeAt (Icc a b) b :=
  mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
no goals
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)
simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
  hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
no goals
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
rw [segment_symm, segment_eq_Icc hab]
no goals
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
rwa [← mem_interior_iff_mem_nhds, interior_Icc]