case pos
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ (w : ℝ), w ∈ Ioo x y → deriv f w ≠ 0
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a

case neg
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ¬∀ (w : ℝ), w ∈ Ioo x y → deriv f w ≠ 0
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a
by_cases h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
no goals
case pos
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ (w : ℝ), w ∈ Ioo x y → deriv f w ≠ 0
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a
apply StrictMonoOn.exists_slope_lt_deriv_aux hf hxy hf'_mono h
case neg
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∃ w, w ∈ Ioo x y ∧ deriv f w = 0
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a
case neg
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ¬∀ (w : ℝ), w ∈ Ioo x y → deriv f w ≠ 0
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a
push_neg  at h
case neg.intro.intro.intro
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a
case neg
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∃ w, w ∈ Ioo x y ∧ deriv f w = 0
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a
rcases h with ⟨w, ⟨hxw, hwy⟩, hw⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
b : ℝ
hb : (f y - f w) / (y - w) < deriv f b
hwb : w < b
hby : b < y
⊢ (f y - f x) / (y - x) < deriv f b
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
b : ℝ
hb : (f y - f w) / (y - w) < deriv f b
hwb : w < b
hby : b < y
⊢ ∃ a, a ∈ Ioo x y ∧ (f y - f x) / (y - x) < deriv f a
refine' ⟨b, ⟨hxw.trans hwb, hby⟩, _⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ f y - f x < deriv f b * (y - x)
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
b : ℝ
hb : (f y - f w) / (y - w) < deriv f b
hwb : w < b
hby : b < y
⊢ (f y - f x) / (y - x) < deriv f b
simp only [div_lt_iff, hxy, hxw, hwy, sub_pos] at ha hb⊢
no goals
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
this : deriv f a * (w - x) < deriv f b * (w - x)
⊢ f y - f x < deriv f b * (y - x)
linarith
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ContinuousOn (fun w => f w) (Icc x w)

E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ StrictMonoOn (deriv fun w => f w) (Ioo x w)

E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∀ (w_1 : ℝ), w_1 ∈ Ioo x w → deriv (fun w => f w) w_1 ≠ 0
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∃ a, a ∈ Ioo x w ∧ (f w - f x) / (w - x) < deriv f a
apply StrictMonoOn.exists_slope_lt_deriv_aux _ hxw _ _
no goals
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ContinuousOn (fun w => f w) (Icc x w)
exact hf.mono (Icc_subset_Icc le_rfl hwy.le)
no goals
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ StrictMonoOn (deriv fun w => f w) (Ioo x w)
exact hf'_mono.mono (Ioo_subset_Ioo le_rfl hwy.le)
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv (fun w => f w) z ≠ 0
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∀ (w_1 : ℝ), w_1 ∈ Ioo x w → deriv (fun w => f w) w_1 ≠ 0
intro z hz
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv (fun w => f w) z ≠ deriv f w
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv (fun w => f w) z ≠ 0
rw [← hw]
case h
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv (fun w => f w) z < deriv f w
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv (fun w => f w) z ≠ deriv f w
apply ne_of_lt
no goals
case h
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv (fun w => f w) z < deriv f w
exact hf'_mono ⟨hz.1, hz.2.trans hwy⟩ ⟨hxw, hwy⟩ hz.2
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ContinuousOn (fun {y} => f y) (Icc w y)

E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ StrictMonoOn (deriv fun {y} => f y) (Ioo w y)

E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ∀ (w_1 : ℝ), w_1 ∈ Ioo w y → deriv (fun {y} => f y) w_1 ≠ 0
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ∃ b, b ∈ Ioo w y ∧ (f y - f w) / (y - w) < deriv f b
apply StrictMonoOn.exists_slope_lt_deriv_aux _ hwy _ _
no goals
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ContinuousOn (fun {y} => f y) (Icc w y)
refine' hf.mono (Icc_subset_Icc hxw.le le_rfl)
no goals
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ StrictMonoOn (deriv fun {y} => f y) (Ioo w y)
exact hf'_mono.mono (Ioo_subset_Ioo hxw.le le_rfl)
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv (fun {y} => f y) z ≠ 0
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ∀ (w_1 : ℝ), w_1 ∈ Ioo w y → deriv (fun {y} => f y) w_1 ≠ 0
intro z hz
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv (fun {y} => f y) z ≠ deriv f w
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv (fun {y} => f y) z ≠ 0
rw [← hw]
case h
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f w < deriv (fun {y} => f y) z
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv (fun {y} => f y) z ≠ deriv f w
apply ne_of_gt
no goals
case h
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f w < deriv (fun {y} => f y) z
exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f a < deriv f b

E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ 0 ≤ deriv f b
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f a * (w - x) < deriv f b * (w - x)
apply mul_lt_mul _ le_rfl (sub_pos.2 hxw) _
no goals
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f a < deriv f b
exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f w ≤ deriv f b
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ 0 ≤ deriv f b
rw [← hw]
no goals
E : Type ?u.430793
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.430889
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f w ≤ deriv f b
exact (hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hwb, hby⟩ hwb).le