-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem Filter.EventuallyEq.hasStrictFDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) (h' : ∀ y, f₀' y = f₁' y) :
    HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x

Proof state:
𝕜 : 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
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), f₀' y = f₁' y
⊢ ∀ (x : E × E),
    f₀ x.1 = f₁ x.1 ∧ f₀ x.2 = f₁ x.2 →
      (fun p => f₀ p.1 - f₀ p.2 - f₀' (p.1 - p.2)) x = (fun p => f₁ p.1 - f₁ p.2 - f₁' (p.1 - p.2)) x

Tactic:
rintro p ⟨hp₁, hp₂⟩

Result:
case 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
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), f₀' y = f₁' y
p : E × E
hp₁ : f₀ p.1 = f₁ p.1
hp₂ : f₀ p.2 = f₁ p.2
⊢ (fun p => f₀ p.1 - f₀ p.2 - f₀' (p.1 - p.2)) p = (fun p => f₁ p.1 - f₁ p.2 - f₁' (p.1 - p.2)) p

Proof state:
case 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
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), f₀' y = f₁' y
p : E × E
hp₁ : f₀ p.1 = f₁ p.1
hp₂ : f₀ p.2 = f₁ p.2
⊢ (fun p => f₀ p.1 - f₀ p.2 - f₀' (p.1 - p.2)) p = (fun p => f₁ p.1 - f₁ p.2 - f₁' (p.1 - p.2)) p

Tactic:
simp only [*]

Result:
no goals

Proof state:
𝕜 : 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
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), f₀' y = f₁' y
⊢ ((fun p => f₀ p.1 - f₀ p.2 - f₀' (p.1 - p.2)) =o[𝕜;𝓝 (x, x)] fun p => p.1 - p.2) ↔
    (fun p => f₁ p.1 - f₁ p.2 - f₁' (p.1 - p.2)) =o[𝕜;𝓝 (x, x)] fun p => p.1 - p.2

Tactic:
refine isLittleOTVS_congr ((h.prod_mk_nhds h).mono ?_) .rfl

Result:
𝕜 : 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
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), f₀' y = f₁' y
⊢ ∀ (x : E × E),
    f₀ x.1 = f₁ x.1 ∧ f₀ x.2 = f₁ x.2 →
      (fun p => f₀ p.1 - f₀ p.2 - f₀' (p.1 - p.2)) x = (fun p => f₁ p.1 - f₁ p.2 - f₁' (p.1 - p.2)) x

Proof state:
𝕜 : 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
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), f₀' y = f₁' y
⊢ HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x

Tactic:
rw [hasStrictFDerivAt_iff_isLittleOTVS, hasStrictFDerivAt_iff_isLittleOTVS]

Result:
𝕜 : 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
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), f₀' y = f₁' y
⊢ ((fun p => f₀ p.1 - f₀ p.2 - f₀' (p.1 - p.2)) =o[𝕜;𝓝 (x, x)] fun p => p.1 - p.2) ↔
    (fun p => f₁ p.1 - f₁ p.2 - f₁' (p.1 - p.2)) =o[𝕜;𝓝 (x, x)] fun p => p.1 - p.2