E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
⊢ Icc a b ⊆ {x | f x ≤ B x}
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
⊢ ∀ ⦃x : ℝ⦄, x ∈ Icc a b → f x ≤ B x
change Icc a b ⊆ { x | f x ≤ B x }
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
⊢ Icc a b ⊆ {x | f x ≤ B x}
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
⊢ Icc a b ⊆ {x | f x ≤ B x}
set s := { x | f x ≤ B x } ∩ Icc a b
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
⊢ Icc a b ⊆ {x | f x ≤ B x}
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
⊢ Icc a b ⊆ {x | f x ≤ B x}
have A : ContinuousOn (fun x => (f x, B x)) (Icc a b) := hf.prod hB
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
⊢ Icc a b ⊆ {x | f x ≤ B x}
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
⊢ Icc a b ⊆ {x | f x ≤ B x}
have : IsClosed s := by
  simp only [inter_comm]
  exact A.preimage_closed_of_closed isClosed_Icc OrderClosedTopology.isClosed_le'
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
⊢ ∀ (x : ℝ), x ∈ {x | f x ≤ B x} ∩ Ico a b → ∀ (y : ℝ), y ∈ Ioi x → Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
⊢ Icc a b ⊆ {x | f x ≤ B x}
apply this.Icc_subset_of_forall_exists_gt ha
case intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
⊢ ∀ (x : ℝ), x ∈ {x | f x ≤ B x} ∩ Ico a b → ∀ (y : ℝ), y ∈ Ioi x → Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
rintro x ⟨hxB : f x ≤ B x, xab⟩ y hy
case intro.inl
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)

case intro.inr
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
case intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
cases' hxB.lt_or_eq with hxB hxB
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {x | f x ≤ B x})
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
⊢ IsClosed s
simp only [inter_comm]
no goals
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {x | f x ≤ B x})
exact A.preimage_closed_of_closed isClosed_Icc OrderClosedTopology.isClosed_le'
case intro.inl
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
⊢ {x | f x ≤ B x} ∈ 𝓝[Ioi x] x
case intro.inl
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
refine' nonempty_of_mem (inter_mem _ (Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, hy⟩))
case intro.inl
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this✝ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
this : ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x
⊢ {x | f x ≤ B x} ∈ 𝓝[Ioi x] x
case intro.inl
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
⊢ {x | f x ≤ B x} ∈ 𝓝[Ioi x] x
have : ∀ᶠ x in 𝓝[Icc a b] x, f x < B x :=
  A x (Ico_subset_Icc_self xab) (IsOpen.mem_nhds (isOpen_lt continuous_fst continuous_snd) hxB)
case intro.inl
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this✝¹ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
this✝ : ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x
this : ∀ᶠ (x : ℝ) in 𝓝[Ioi x] x, f x < B x
⊢ {x | f x ≤ B x} ∈ 𝓝[Ioi x] x
case intro.inl
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this✝ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
this : ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x
⊢ {x | f x ≤ B x} ∈ 𝓝[Ioi x] x
have : ∀ᶠ x in 𝓝[>] x, f x < B x := nhdsWithin_le_of_mem (Icc_mem_nhdsWithin_Ioi xab) this
no goals
case intro.inl
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this✝¹ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
this✝ : ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x
this : ∀ᶠ (x : ℝ) in 𝓝[Ioi x] x, f x < B x
⊢ {x | f x ≤ B x} ∈ 𝓝[Ioi x] x
exact this.mono fun y => le_of_lt
case intro.inr.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
case intro.inr
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
rcases exists_between (bound x xab hxB) with ⟨r, hfr, hrB⟩
case intro.inr.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
case intro.inr.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
specialize hf' x xab r hfr
case intro.inr.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
case intro.inr.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
have HB : ∀ᶠ z in 𝓝[>] x, r < slope B x z :=
  (hasDerivWithinAt_iff_tendsto_slope' <| lt_irrefl x).1 (hB' x xab).Ioi_of_Ici
    (Ioi_mem_nhds hrB)
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
⊢ ∃ z, slope f x z < r ∧ r < slope B x z ∧ z ∈ Ioc x y

case intro.inr.intro.intro.intro.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
case intro.inr.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
obtain ⟨z, hfz, hzB, hz⟩ : ∃ z, slope f x z < r ∧ r < slope B x z ∧ z ∈ Ioc x y
case intro.inr.intro.intro.intro.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
⊢ ∃ z, slope f x z < r ∧ r < slope B x z ∧ z ∈ Ioc x y

case intro.inr.intro.intro.intro.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
exact (hf'.and_eventually (HB.and (Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, hy⟩))).exists
case intro.inr.intro.intro.intro.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ z ∈ {x | f x ≤ B x}
case intro.inr.intro.intro.intro.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ Set.Nonempty ({x | f x ≤ B x} ∩ Ioc x y)
refine' ⟨z, _, hz⟩
case intro.inr.intro.intro.intro.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this✝ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : slope f x z ≤ slope B x z
⊢ z ∈ {x | f x ≤ B x}
case intro.inr.intro.intro.intro.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
⊢ z ∈ {x | f x ≤ B x}
have := (hfz.trans hzB).le
no goals
case intro.inr.intro.intro.intro.intro.intro
E : Type ?u.193
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.289
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
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 → f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x => (f x, B x)) (Icc a b)
this✝ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hfr : f' x < r
hrB : r < B' x
hf' : ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, slope f x z < r
HB : ∀ᶠ (z : ℝ) in 𝓝[Ioi x] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : slope f x z ≤ slope B x z
⊢ z ∈ {x | f x ≤ B x}
rwa [slope_def_field, slope_def_field, div_le_div_right (sub_pos.2 hz.1), hxB,
  sub_le_sub_iff_right] at this