E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
Hr : ∀ (x : ℝ), x ∈ Icc a b → ∀ (r : ℝ), r > 0 → f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ B x
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
Hr : ∀ (x : ℝ), x ∈ Icc a b → ∀ (r : ℝ), r > 0 → f x ≤ B x + r * (x - a)
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → f x ≤ B x
intro x hx
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
Hr : ∀ (x : ℝ), x ∈ Icc a b → ∀ (r : ℝ), r > 0 → f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0
⊢ f x ≤ B x
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
Hr : ∀ (x : ℝ), x ∈ Icc a b → ∀ (r : ℝ), r > 0 → f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ B x
have : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0 :=
  continuousWithinAt_const.add (continuousWithinAt_id.mul continuousWithinAt_const)
no goals
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
Hr : ∀ (x : ℝ), x ∈ Icc a b → ∀ (r : ℝ), r > 0 → f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0
⊢ f x ≤ B x
convert continuousWithinAt_const.closure_le _ this (Hr x hx) using 1 <;> simp
case ha
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ f a ≤ B a + r * (a - a)

case hB
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ContinuousOn (fun x => B x + r * (x - a)) (Icc a b)

case hB'
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt (fun x => B x + r * (x - a)) (?m.13270 x) (Ici x) x

case bound
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ∀ (x : ℝ), x ∈ Ico a b → f x = B x + r * (x - a) → B' x < ?m.13270 x

case a
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ x ∈ Icc a b

E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ℝ → ℝ
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ f x ≤ B x + r * (x - a)
apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound
no goals
case a
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ x ∈ Icc a b
exact hx
no goals
case ha
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ f a ≤ B a + r * (a - a)
rwa [sub_self, mul_zero, add_zero]
no goals
case hB
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ContinuousOn (fun x => B x + r * (x - a)) (Icc a b)
exact hB.add (continuousOn_const.mul (continuousOn_id.sub continuousOn_const))
case hB'
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun x => B x + r * (x - a)) (?m.13270 x) (Ici x) x
case hB'
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt (fun x => B x + r * (x - a)) (?m.13270 x) (Ici x) x
intro x hx
no goals
case hB'
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt (fun x => B x + r * (x - a)) (?m.13270 x) (Ici x) x
exact (hB' x hx).add (((hasDerivWithinAt_id x (Ici x)).sub_const a).const_mul r)
case bound
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x✝ : ℝ
hx : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
a✝¹ : x ∈ Ico a b
a✝ : f x = B x + r * (x - a)
⊢ B' x < B' x + r * 1
case bound
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ∀ (x : ℝ), x ∈ Ico a b → f x = B x + r * (x - a) → B' x < B' x + r * 1
intro x _ _
case bound
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x✝ : ℝ
hx : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
a✝¹ : x ∈ Ico a b
a✝ : f x = B x + r * (x - a)
⊢ B' x < B' x + r
case bound
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x✝ : ℝ
hx : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
a✝¹ : x ∈ Ico a b
a✝ : f x = B x + r * (x - a)
⊢ B' x < B' x + r * 1
rw [mul_one]
no goals
case bound
E : Type ?u.11278
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.11374
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
x✝ : ℝ
hx : x✝ ∈ Icc a b
r : ℝ
hr : r > 0
x : ℝ
a✝¹ : x ∈ Ico a b
a✝ : f x = B x + r * (x - a)
⊢ B' x < B' x + r
exact (lt_add_iff_pos_right _).2 hr