𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.467335
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.467430
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), ↑f₀' y = ↑f₁' y
⊢ ∀ (x : E × E),
    f₀ x.fst = f₁ x.fst ∧ f₀ x.snd = f₁ x.snd →
      (fun p => f₀ p.fst - f₀ p.snd - ↑f₀' (p.fst - p.snd)) x = (fun p => f₁ p.fst - f₁ p.snd - ↑f₁' (p.fst - p.snd)) x
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.467335
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.467430
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), ↑f₀' y = ↑f₁' y
⊢ HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x
refine' isLittleO_congr ((h.prod_mk_nhds h).mono _) (eventually_of_forall fun _ => _root_.rfl)
case intro
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.467335
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.467430
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), ↑f₀' y = ↑f₁' y
p : E × E
hp₁ : f₀ p.fst = f₁ p.fst
hp₂ : f₀ p.snd = f₁ p.snd
⊢ (fun p => f₀ p.fst - f₀ p.snd - ↑f₀' (p.fst - p.snd)) p = (fun p => f₁ p.fst - f₁ p.snd - ↑f₁' (p.fst - p.snd)) p
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.467335
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.467430
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), ↑f₀' y = ↑f₁' y
⊢ ∀ (x : E × E),
    f₀ x.fst = f₁ x.fst ∧ f₀ x.snd = f₁ x.snd →
      (fun p => f₀ p.fst - f₀ p.snd - ↑f₀' (p.fst - p.snd)) x = (fun p => f₁ p.fst - f₁ p.snd - ↑f₁' (p.fst - p.snd)) x
rintro p ⟨hp₁, hp₂⟩
no goals
case intro
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.467335
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.467430
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), ↑f₀' y = ↑f₁' y
p : E × E
hp₁ : f₀ p.fst = f₁ p.fst
hp₂ : f₀ p.snd = f₁ p.snd
⊢ (fun p => f₀ p.fst - f₀ p.snd - ↑f₀' (p.fst - p.snd)) p = (fun p => f₁ p.fst - f₁ p.snd - ↑f₁' (p.fst - p.snd)) p
simp only [*]