-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem Filter.EventuallyEq.hasLineDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) :
    HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v

Proof state:
case h.e'_3.h.e'_3
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
B : ContinuousAt F 0
⊢ F 0 = x

Tactic:
simp [F]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
B : ContinuousAt F 0
this : f₀ =ᶠ[𝓝 (F 0)] f₁
⊢ (fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)

Tactic:
exact B.preimage_mem_nhds this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
⊢ HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v

Tactic:
apply hasDerivAt_iff

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
⊢ (fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
⊢ (fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)

Tactic:
have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
B : ContinuousAt F 0
⊢ (fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
⊢ ContinuousAt F 0

Tactic:
apply Continuous.continuousAt

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
⊢ Continuous F

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
B : ContinuousAt F 0
⊢ (fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)

Tactic:
have : f₀ =ᶠ[𝓝 (F 0)] f₁ := by convert h; simp [F]

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
B : ContinuousAt F 0
this : f₀ =ᶠ[𝓝 (F 0)] f₁
⊢ (fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
B : ContinuousAt F 0
⊢ f₀ =ᶠ[𝓝 (F 0)] f₁

Tactic:
convert h

Result:
case h.e'_3.h.e'_3
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
B : ContinuousAt F 0
⊢ F 0 = x

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
⊢ Continuous F

Tactic:
fun_prop

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
⊢ (fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)

Tactic:
let F := fun (t : 𝕜) ↦ x + t • v

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace 𝕜 F✝
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F✝
f' : F✝
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : 𝕜 → E := fun t => x + t • v
⊢ (fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)