case inl
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hE : Subsingleton E
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c

case inr
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : Subsingleton E ∨ 0 < c
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
cases' hc with hE hc
case inr
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
this : ∀ᶠ (x : E × E) in 𝓝 (a, a), ‖f x.fst - f x.snd - ↑f' (x.fst - x.snd)‖ ≤ (fun a => ↑a) c * ‖x.fst - x.snd‖
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
case inr
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
have := hf.def hc
case inr
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
this : ∃ t, t ∈ 𝓝 a ∧ t ×ˢ t ⊆ {x | ‖f x.fst - f x.snd - ↑f' (x.fst - x.snd)‖ ≤ (fun a => ↑a) c * ‖x.fst - x.snd‖}
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
case inr
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
this : ∀ᶠ (x : E × E) in 𝓝 (a, a), ‖f x.fst - f x.snd - ↑f' (x.fst - x.snd)‖ ≤ (fun a => ↑a) c * ‖x.fst - x.snd‖
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
rw [nhds_prod_eq, Filter.Eventually, mem_prod_same_iff] at this
case inr.intro.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
s : Set E
has : s ∈ 𝓝 a
hs : s ×ˢ s ⊆ {x | ‖f x.fst - f x.snd - ↑f' (x.fst - x.snd)‖ ≤ (fun a => ↑a) c * ‖x.fst - x.snd‖}
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
case inr
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
this : ∃ t, t ∈ 𝓝 a ∧ t ×ˢ t ⊆ {x | ‖f x.fst - f x.snd - ↑f' (x.fst - x.snd)‖ ≤ (fun a => ↑a) c * ‖x.fst - x.snd‖}
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
rcases this with ⟨s, has, hs⟩
no goals
case inr.intro.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
s : Set E
has : s ∈ 𝓝 a
hs : s ×ˢ s ⊆ {x | ‖f x.fst - f x.snd - ↑f' (x.fst - x.snd)‖ ≤ (fun a => ↑a) c * ‖x.fst - x.snd‖}
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
exact ⟨s, has, fun x hx y hy => hs (mk_mem_prod hx hy)⟩
case inl
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hE : Subsingleton E
x : E
x✝¹ : x ∈ univ
y : E
x✝ : y ∈ univ
⊢ ‖f x - f y - ↑f' (x - y)‖ ≤ ↑c * ‖x - y‖
case inl
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hE : Subsingleton E
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f f' s c
refine' ⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => _⟩
no goals
case inl
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.502454
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.502557
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
ε : ℝ
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hE : Subsingleton E
x : E
x✝¹ : x ∈ univ
y : E
x✝ : y ∈ univ
⊢ ‖f x - f y - ↑f' (x - y)‖ ≤ ↑c * ‖x - y‖
simp [@Subsingleton.elim E hE x y]