Lean manifolds: show mfderiv f x v = 0 when f is constant along a curve through v

To prove a smooth map f : M → N kills a vector field built as v x = (tangentMap Φ (timeVector x)).2 (Φ : M × ℝ → M a flow), avoid charts: (1) write timeVector x = tangentMap 𝓘(ℝ,ℝ) _ (fun t ↦ (x, t)) ⟨0, 1⟩ (rw [tangentMap_prod_right]; rfl); (2) change (tangentMap I I' f ⟨x, v x⟩).2 = 0 (tangentMap's second component is mfderiv by rfl); (3) rewrite with ← Function.comp_apply and ← tangentMap_comp twice (needs MDifferentiable of f, Φ and the curve: mdifferentiable_const.prodMk mdifferentiable_id); (4) rewrite the composite f ∘ Φ ∘ (x, ·) to fun _ ↦ f x by funext; (5) change mfderiv 𝓘(ℝ,ℝ) I' (fun _ ↦ f x) 0 1 = 0; rw [mfderiv_const]; rfl. Used for: the Hopf vector field is tangent to the fibres of the Hopf map S³ → S².