𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, (a ∈ s ∧ IsOpen s) ∧ ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)
𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, a ∈ s ∧ IsOpen s ∧ ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)
simp only [← and_assoc]
case refine'_1
𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      ApproximatesLinearOn f (↑f') t (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2) →
        ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)

case refine'_2
𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)
𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, (a ∈ s ∧ IsOpen s) ∧ ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)
refine' ((nhds_basis_opens a).exists_iff _).1 _
case refine'_2
𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)
case refine'_1
𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      ApproximatesLinearOn f (↑f') t (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2) →
        ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)

case refine'_2
𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)
exact fun s t => ApproximatesLinearOn.mono_set
no goals
case refine'_2
𝕜 : 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.526060
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.526163
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, s ∈ 𝓝 a ∧ ApproximatesLinearOn f (↑f') s (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ / 2)
exact
  hf.approximates_deriv_on_nhds <|
    f'.subsingleton_or_nnnorm_symm_pos.imp id fun hf' => half_pos <| inv_pos.2 hf'