E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a < (f y - f x) / (y - x)
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 ∧ deriv f a < (f y - f x) / (y - x)
have A : DifferentiableOn ℝ f (Ioo x y) := fun w wmem =>
  (differentiableAt_of_deriv_ne_zero (h w wmem)).differentiableWithinAt
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a = (f y - f x) / (y - x)

case intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a < (f y - f x) / (y - x)
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a < (f y - f x) / (y - x)
obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x)
case intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a < (f y - f x) / (y - x)
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a = (f y - f x) / (y - x)

case intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a < (f y - f x) / (y - x)
exact exists_deriv_eq_slope f hxy hf A
case intro.intro.intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a < (f y - f x) / (y - x)
case intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a < (f y - f x) / (y - x)
rcases nonempty_Ioo.2 hxa with ⟨b, ⟨hxb, hba⟩⟩
case intro.intro.intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ deriv f b < (f y - f x) / (y - x)
case intro.intro.intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a < (f y - f x) / (y - x)
refine' ⟨b, ⟨hxb, hba.trans hay⟩, _⟩
case intro.intro.intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ deriv f b < deriv f a
case intro.intro.intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ deriv f b < (f y - f x) / (y - x)
rw [← ha]
no goals
case intro.intro.intro.intro.intro
E : Type ?u.437432
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.437528
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 : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ deriv f b < deriv f a
exact hf'_mono ⟨hxb, hba.trans hay⟩ ⟨hxa, hay⟩ hba