E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ C * (y - x) ≤ f y - f x
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
⊢ ∀ (x : ℝ), x ∈ D → ∀ (y : ℝ), y ∈ D → x ≤ y → C * (y - x) ≤ f y - f x
intro x hx y hy hxy
case inl
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x = y
⊢ C * (y - x) ≤ f y - f x

case inr
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
⊢ C * (y - x) ≤ f y - f x
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ C * (y - x) ≤ f y - f x
cases' eq_or_lt_of_le hxy with hxy' hxy'
case inr
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
⊢ C * (y - x) ≤ f y - f x
case inr
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
⊢ C * (y - x) ≤ f y - f x
have hxyD : Icc x y ⊆ D := hD.ordConnected.out hx hy
case inr
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ C * (y - x) ≤ f y - f x
case inr
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
⊢ C * (y - x) ≤ f y - f x
have hxyD' : Ioo x y ⊆ interior D :=
  subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a = (f y - f x) / (y - x)

case inr.intro.intro
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x
case inr
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ C * (y - x) ≤ f y - f x
obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x)
case inr.intro.intro
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ ∃ a, a ∈ Ioo x y ∧ deriv f a = (f y - f x) / (y - x)

case inr.intro.intro
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x
exact exists_deriv_eq_slope f hxy' (hf.mono hxyD) (hf'.mono hxyD')
case inr.intro.intro
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
this : C ≤ (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x
case inr.intro.intro
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x
have : C ≤ (f y - f x) / (y - x) := ha ▸ hf'_ge _ (hxyD' a_mem)
no goals
case inr.intro.intro
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x < y
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
a : ℝ
a_mem : a ∈ Ioo x y
ha : deriv f a = (f y - f x) / (y - x)
this : C ≤ (f y - f x) / (y - x)
⊢ C * (y - x) ≤ f y - f x
exact (le_div_iff (sub_pos.2 hxy')).1 this
no goals
case inl
E : Type ?u.400429
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.400525
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
hf'_ge : ∀ (x : ℝ), x ∈ interior D → C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x = y
⊢ C * (y - x) ≤ f y - f x
rw [hxy', sub_self, sub_self, mul_zero]