-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem LineDifferentiableAt.congr_of_eventuallyEq
    (h : LineDifferentiableAt 𝕜 f x v) (hL : f₁ =ᶠ[𝓝 x] f) :
    LineDifferentiableAt 𝕜 f₁ x 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✝
x v : E
h : LineDifferentiableAt 𝕜 f x v
F : 𝕜 → E := fun t => x + t • v
hL : f₁ =ᶠ[𝓝 (F 0)] f
⊢ (fun t => f₁ (x + t • v)) =ᶠ[𝓝 0] fun t => f (x + t • v)

Tactic:
exact (Continuous.continuousAt (by fun_prop)).preimage_mem_nhds hL

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
x v : E
h : LineDifferentiableAt 𝕜 f x v
hL : f₁ =ᶠ[𝓝 x] f
⊢ LineDifferentiableAt 𝕜 f₁ x v

Tactic:
apply DifferentiableAt.congr_of_eventuallyEq h

Result:
𝕜 : 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
x v : E
h : LineDifferentiableAt 𝕜 f x v
hL : f₁ =ᶠ[𝓝 x] 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
x v : E
h : LineDifferentiableAt 𝕜 f x v
hL : 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:
𝕜 : 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✝
x v : E
h : LineDifferentiableAt 𝕜 f x v
hL : f₁ =ᶠ[𝓝 x] f
F : 𝕜 → E := fun t => x + t • v
⊢ (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✝
x v : E
h : LineDifferentiableAt 𝕜 f x v
hL : f₁ =ᶠ[𝓝 x] f
F : 𝕜 → E := fun t => x + t • v
⊢ x = F 0

Tactic:
simp [F]

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✝
x v : E
h : LineDifferentiableAt 𝕜 f x v
F : 𝕜 → E := fun t => x + t • v
hL : f₁ =ᶠ[𝓝 (F 0)] f
⊢ Continuous F

Tactic:
fun_prop

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✝
x v : E
h : LineDifferentiableAt 𝕜 f x v
hL : f₁ =ᶠ[𝓝 x] f
F : 𝕜 → E := fun t => x + t • v
⊢ (fun t => f₁ (x + t • v)) =ᶠ[𝓝 0] fun t => f (x + t • v)

Tactic:
rw [show x = F 0 by simp [F]] at hL

Result:
𝕜 : 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✝
x v : E
h : LineDifferentiableAt 𝕜 f x v
F : 𝕜 → E := fun t => x + t • v
hL : f₁ =ᶠ[𝓝 (F 0)] f
⊢ (fun t => f₁ (x + t • v)) =ᶠ[𝓝 0] fun t => f (x + t • v)