[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a✝ b✝ : 𝕜
s : Set 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
⊢ dslope (↑f ∘ g) a b = ↑f (dslope g a b)
[PROOFSTEP]
rcases eq_or_ne b a with (rfl | hne)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a b✝ : 𝕜
s : Set 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ dslope (↑f ∘ g) b b = ↑f (dslope g b b)
[PROOFSTEP]
simp only [dslope_same]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a b✝ : 𝕜
s : Set 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ deriv (↑f ∘ g) b = ↑f (deriv g b)
[PROOFSTEP]
exact (f.hasFDerivAt.comp_hasDerivAt b (H rfl).hasDerivAt).deriv
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a✝ b✝ : 𝕜
s : Set 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
hne : b ≠ a
⊢ dslope (↑f ∘ g) a b = ↑f (dslope g a b)
[PROOFSTEP]
simpa only [dslope_of_ne _ hne] using f.toLinearMap.slope_comp g a b
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a✝ b✝ : 𝕜
s : Set 𝕜
f : 𝕜 → E
a b : 𝕜
⊢ (b - a) • dslope f a b = f b - f a
[PROOFSTEP]
rcases eq_or_ne b a with (rfl | hne)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a b✝ : 𝕜
s : Set 𝕜
f : 𝕜 → E
b : 𝕜
⊢ (b - b) • dslope f b b = f b - f b
[PROOFSTEP]
simp [dslope_of_ne, *]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a✝ b✝ : 𝕜
s : Set 𝕜
f : 𝕜 → E
a b : 𝕜
hne : b ≠ a
⊢ (b - a) • dslope f a b = f b - f a
[PROOFSTEP]
simp [dslope_of_ne, *]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a b : 𝕜
s : Set 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope (fun x => (x - a) • f x) a b = f b
[PROOFSTEP]
rw [dslope_of_ne _ h, slope_sub_smul _ h.symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
⊢ ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a
[PROOFSTEP]
simp only [dslope, continuousAt_update_same, ← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
⊢ ContinuousWithinAt f s b
[PROOFSTEP]
have : ContinuousWithinAt (fun x => (x - a) • dslope f a x + f a) s b :=
  ((continuousWithinAt_id.sub continuousWithinAt_const).smul h).add continuousWithinAt_const
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
this : ContinuousWithinAt (fun x => (x - a) • dslope f a x + f a) s b
⊢ ContinuousWithinAt f s b
[PROOFSTEP]
simpa only [sub_smul_dslope, sub_add_cancel] using this
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b
[PROOFSTEP]
refine' ⟨ContinuousWithinAt.of_dslope, fun hc => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (dslope f a) s b
[PROOFSTEP]
simp only [dslope, continuousWithinAt_update_of_ne h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (slope f a) s b
[PROOFSTEP]
exact
  ((continuousWithinAt_id.sub continuousWithinAt_const).inv₀ (sub_ne_zero.2 h)).smul (hc.sub continuousWithinAt_const)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ ContinuousAt (dslope f a) b ↔ ContinuousAt f b
[PROOFSTEP]
simp only [← continuousWithinAt_univ, continuousWithinAt_dslope_of_ne h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
⊢ ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a
[PROOFSTEP]
refine' ⟨fun hc => ⟨hc.of_dslope, continuousAt_dslope_same.1 <| hc.continuousAt h⟩, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
⊢ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a → ContinuousOn (dslope f a) s
[PROOFSTEP]
rintro ⟨hc, hd⟩ x hx
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
⊢ ContinuousWithinAt (dslope f a) s x
[PROOFSTEP]
rcases eq_or_ne x a with (rfl | hne)
[GOAL]
case intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
b : 𝕜
s : Set 𝕜
hc : ContinuousOn f s
x : 𝕜
hx : x ∈ s
h : s ∈ 𝓝 x
hd : DifferentiableAt 𝕜 f x
⊢ ContinuousWithinAt (dslope f x) s x
case intro.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
hne : x ≠ a
⊢ ContinuousWithinAt (dslope f a) s x
[PROOFSTEP]
exacts [(continuousAt_dslope_same.2 hd).continuousWithinAt, (continuousWithinAt_dslope_of_ne hne).2 (hc x hx)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 (dslope f a) s b
⊢ DifferentiableWithinAt 𝕜 f s b
[PROOFSTEP]
simpa only [id, sub_smul_dslope f a, sub_add_cancel] using
  ((differentiableWithinAt_id.sub_const a).smul h).add_const (f a)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b
[PROOFSTEP]
refine' ⟨DifferentiableWithinAt.of_dslope, fun hd => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b
[PROOFSTEP]
refine'
  (((differentiableWithinAt_id.sub_const a).inv (sub_ne_zero.2 h)).smul (hd.sub_const (f a))).congr_of_eventuallyEq _
    (dslope_of_ne _ h)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ dslope f a =ᶠ[𝓝[s] b] fun y => (id y - a)⁻¹ • (f y - f a)
[PROOFSTEP]
refine' (eqOn_dslope_slope _ _).eventuallyEq_of_mem _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ {a}ᶜ ∈ 𝓝[s] b
[PROOFSTEP]
exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b
[PROOFSTEP]
simp only [← differentiableWithinAt_univ, differentiableWithinAt_dslope_of_ne h]


[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n ↑f
[PROOFSTEP]
rw [f.decomp]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n (↑(contLinear f) + Function.const V (↑f 0))
[PROOFSTEP]
apply f.contLinear.contDiff.add
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n fun x => Function.const V (↑f 0) x
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n fun x => Function.const V (↑f 0) x
[PROOFSTEP]
exact contDiff_const


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
⊢ ContinuousOn f (closedBall x r)
[PROOFSTEP]
rcases eq_or_ne r 0 with (rfl | hr)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f (closedBall x 0)
[PROOFSTEP]
rw [closedBall_zero]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f {x}
[PROOFSTEP]
exact continuousOn_singleton f x
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closedBall x r)
[PROOFSTEP]
rw [← closure_ball x hr]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure (ball x r))
[PROOFSTEP]
exact h.continuousOn


[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
rcases hab.eq_or_lt with (rfl | hab')
[GOAL]
case inl
a : ℝ
f f' : ℝ → ℝ
m : ℝ
hma : f' a < m
hab : a ≤ a
hf : ∀ (x : ℝ), x ∈ Icc a a → HasDerivWithinAt f (f' x) (Icc a a) x
hmb : m < f' a
⊢ m ∈ f' '' Ioo a a
[PROOFSTEP]
exact (lt_asymm hma hmb).elim
[GOAL]
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
set g : ℝ → ℝ := fun x => f x - m * x
[GOAL]
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
have hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x :=
  by
  intro x hx
  simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
⊢ ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
[PROOFSTEP]
intro x hx
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
x : ℝ
hx : x ∈ Icc a b
⊢ HasDerivWithinAt g (f' x - m) (Icc a b) x
[PROOFSTEP]
simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)
[GOAL]
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Icc a b, IsMinOn g (Icc a b) c
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
⊢ ∃ c, c ∈ Icc a b ∧ IsMinOn g (Icc a b) c
case inr.intro.intro
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
exact isCompact_Icc.exists_forall_le (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt
[GOAL]
case inr.intro.intro
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
have cmem' : c ∈ Ioo a b :=
  by
  rcases cmem.1.eq_or_lt with
    (rfl | hac)
      -- Show that `c` can't be equal to `a`
  · refine' absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right _ (sub_pos.2 hab')) (not_le_of_lt hma)
    have : b - a ∈ posTangentConeAt (Icc a b) a :=
      mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.refl _)
    simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
      hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
  rcases cmem.2.eq_or_gt with
    (rfl | hcb)
      -- Show that `c` can't be equal to `b`
  · refine' absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right _ (sub_lt_zero.2 hab')) (not_le_of_lt hmb)
    have : a - b ∈ posTangentConeAt (Icc a b) b :=
      mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
    simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
      hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
  exact ⟨hac, hcb⟩
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
⊢ c ∈ Ioo a b
[PROOFSTEP]
rcases cmem.1.eq_or_lt with
  (rfl | hac)
    -- Show that `c` can't be equal to `a`
[GOAL]
case inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ a ∈ Ioo a b
[PROOFSTEP]
refine' absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right _ (sub_pos.2 hab')) (not_le_of_lt hma)
[GOAL]
case inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ 0 ≤ (b - a) * (f' a - m)
[PROOFSTEP]
have : b - a ∈ posTangentConeAt (Icc a b) a :=
  mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.refl _)
[GOAL]
case inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
this : b - a ∈ posTangentConeAt (Icc a b) a
⊢ 0 ≤ (b - a) * (f' a - m)
[PROOFSTEP]
simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
  hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
[GOAL]
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
⊢ c ∈ Ioo a b
[PROOFSTEP]
rcases cmem.2.eq_or_gt with
  (rfl | hcb)
    -- Show that `c` can't be equal to `b`
[GOAL]
case inr.inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ b ∈ Ioo a b
[PROOFSTEP]
refine' absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right _ (sub_lt_zero.2 hab')) (not_le_of_lt hmb)
[GOAL]
case inr.inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ 0 ≤ (a - b) * (f' b - m)
[PROOFSTEP]
have : a - b ∈ posTangentConeAt (Icc a b) b :=
  mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ segment ℝ b a ⊆ Icc a b
[PROOFSTEP]
rw [segment_symm, segment_eq_Icc hab]
[GOAL]
case inr.inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
this : a - b ∈ posTangentConeAt (Icc a b) b
⊢ 0 ≤ (a - b) * (f' b - m)
[PROOFSTEP]
simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
  hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
[GOAL]
case inr.inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
hcb : c < b
⊢ c ∈ Ioo a b
[PROOFSTEP]
exact ⟨hac, hcb⟩
[GOAL]
case inr.intro.intro
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ m ∈ f' '' Ioo a b
[PROOFSTEP]
use c, cmem'
[GOAL]
case right
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ f' c = m
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
case right
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ f' c - m = 0
[PROOFSTEP]
have : Icc a b ∈ 𝓝 c := by rwa [← mem_interior_iff_mem_nhds, interior_Icc]
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 c
[PROOFSTEP]
rwa [← mem_interior_iff_mem_nhds, interior_Icc]
[GOAL]
case right
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x => f x - m * x
hg : ∀ (x : ℝ), x ∈ Icc a b → HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
this : Icc a b ∈ 𝓝 c
⊢ f' c - m = 0
[PROOFSTEP]
exact (hc.isLocalMin this).hasDerivAt_eq_zero ((hg c cmem).hasDerivAt this)
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
⊢ OrdConnected (f' '' s)
[PROOFSTEP]
apply ordConnected_of_Ioo
[GOAL]
case hs
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
⊢ ∀ (x : ℝ), x ∈ f' '' s → ∀ (y : ℝ), y ∈ f' '' s → x < y → Ioo x y ⊆ f' '' s
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ - m ⟨hma, hmb⟩
[GOAL]
case hs.intro.intro.intro.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' s
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case hs.intro.intro.intro.intro.intro.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
⊢ m ∈ f' '' s
[PROOFSTEP]
have : Icc a b ⊆ s := hs.out ha hb
[GOAL]
case hs.intro.intro.intro.intro.intro.inl
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
⊢ m ∈ f' '' s
[PROOFSTEP]
rcases exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x <| this hx).mono this) hma hmb with ⟨c, cmem, hc⟩
[GOAL]
case hs.intro.intro.intro.intro.intro.inl.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
c : ℝ
cmem : c ∈ Ioo a b
hc : (fun x => f' x) c = m
⊢ m ∈ f' '' s
[PROOFSTEP]
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
[GOAL]
case hs.intro.intro.intro.intro.intro.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
⊢ m ∈ f' '' s
[PROOFSTEP]
have : Icc b a ⊆ s := hs.out hb ha
[GOAL]
case hs.intro.intro.intro.intro.intro.inr
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
⊢ m ∈ f' '' s
[PROOFSTEP]
rcases exists_hasDerivWithinAt_eq_of_lt_of_gt hab (fun x hx => (hf x <| this hx).mono this) hmb hma with ⟨c, cmem, hc⟩
[GOAL]
case hs.intro.intro.intro.intro.intro.inr.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : OrdConnected s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
c : ℝ
cmem : c ∈ Ioo b a
hc : (fun x => f' x) c = m
⊢ m ∈ f' '' s
[PROOFSTEP]
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : ∀ (x : ℝ), x ∈ s → f' x ≠ m
⊢ (∀ (x : ℝ), x ∈ s → f' x < m) ∨ ∀ (x : ℝ), x ∈ s → m < f' x
[PROOFSTEP]
contrapose! hf'
[GOAL]
a b : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : (∃ x, x ∈ s ∧ m ≤ f' x) ∧ ∃ x, x ∈ s ∧ f' x ≤ m
⊢ ∃ x, x ∈ s ∧ f' x = m
[PROOFSTEP]
rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
a✝ b✝ : ℝ
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x, x ∈ s ∧ f' x = m
[PROOFSTEP]
exact (hs.ordConnected.image_hasDerivWithinAt hf).out (mem_image_of_mem f' ha) (mem_image_of_mem f' hb) ⟨hma, hmb⟩