Is Total Time Derivative explicit

lemma isTotalTimeDerivative_explicit {δL : Time → X → X → ℝ} :    IsTotalTimeDerivative δL ↔  (∃ (F : Time → X → ℝ) (_ : ContDiff ℝ ∞ ↿F),    ∀ t q v, δL t q v = fderiv ℝ ↿F (t, q) ((1 : Time), v)) := by  -- Preliminary construction: properties of the function t => (t, q t)  let tq := fun (q : Time → X) t => (t, q t)  have h_tq_contDiff : ∀ (q : Time → X), ContDiff ℝ ∞ q -> ContDiff ℝ ∞ (tq q) := by    fun_prop  have h_tq_der :  ∀ (q : Time → X) t, ContDiff ℝ ∞ q -> ∂ₜ (tq q) t = (1, ∂ₜ q t) := by    intro q t h_ContDiff_q    ext    change (∂ₜ (tq q) t).1.val = (1 : Time).val    congr    apply Eq.symm    calc      (1 : Time) = fderiv ℝ (fun (t' : Time) => t') t 1 := by simp only [fderiv_fun_id,        ContinuousLinearMap.coe_id', id_eq]      _ = fderiv ℝ (fun (t' : Time) => (tq q t').1) t 1 := by rfl      _ = (∂ₜ (tq q) t).1 := by        rw [fderiv.fst]        · simp          rfl        · apply ContDiffAt.differentiableAt          · apply ContDiff.contDiffAt            exact h_tq_contDiff q h_ContDiff_q          · by_contra            rcases this    apply Eq.symm    calc       (1, ∂ₜ q t).2 = fderiv ℝ (fun t' => (tq q t').2) t 1 := by rfl       _ = (∂ₜ (tq q) t).2 := by        rw [fderiv.snd]        · simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.coe_snd']          rfl        · apply ContDiffAt.differentiableAt          · apply ContDiff.contDiffAt            exact h_tq_contDiff q h_ContDiff_q          · by_contra            rcases this  have h_F_tq_der : ∀ (q : Time → X) (F : Time → X → ℝ) t, (ContDiff ℝ ∞ ↿F) → (ContDiff ℝ ∞ q)  →      ∂ₜ (fun t' => ↿F (t', q t')) t = fderiv ℝ ↿F (t, q t) ((1 : Time), ∂ₜ q t) := by    intro q F t hF hq    change  fderiv ℝ ((↿F) ∘ (tq q)) t 1 = fderiv ℝ ↿F (t, q t) ((1 : Time), ∂ₜ q t)    rw [fderiv_comp]    · simp only [ContinuousLinearMap.comp_apply]      rw [← Time.deriv_eq,h_tq_der]      exact hq    · apply ContDiffAt.differentiableAt      · apply ContDiff.contDiffAt        exact hF      · by_contra        rcases this    · apply ContDiffAt.differentiableAt      · apply ContDiff.contDiffAt        exact h_tq_contDiff q hq      · by_contra        rcases this  -- beginning of the proof  constructor  -- From total the total derivative to the explicit form  · intro h    rcases h with ⟨F, hF⟩    rcases hF with ⟨hFdif, hFder⟩    use F    use hFdif    intro t q₀ v    let qv := fun (t' : Time) => (q₀ - t.val • v) + t'.val • v    have h_qv_contDiff : ContDiff ℝ ∞ qv := by      change ContDiff ℝ ∞ (((fun (tR : ℝ) => (q₀ - t.val • v) + tR • v)) ∘ Time.toRealCLE)      fun_prop    have h_qv_t : qv t = q₀ := by      calc        qv t = (q₀ - t.val • v) + t.val • v := by rfl        _ = q₀ := by module    have h_qv_der : ∂ₜ qv t = v := by      calc        ∂ₜ qv t = fderiv ℝ (fun t' => (q₀ - t.val • v) + t'.val • v) t 1 := by rfl        _ = v := by          rw [fderiv_const_add,fderiv_smul_const]          · simp only [ContinuousLinearMap.smulRight_apply, fderiv_val, one_smul]          · fun_prop    rw [← h_qv_t, ← h_qv_der, hFder, ← h_F_tq_der]    · rfl    · exact hFdif    · exact h_qv_contDiff    · exact h_qv_contDiff  -- From the explicit form to the total derivative  · intro h    rcases h with ⟨F, hF⟩    rcases hF with ⟨hFdif, hFder⟩    use F    use hFdif    intro t q hq_ContDiff    rw [hFder, ← h_F_tq_der]    · rfl    · exact hFdif    · exact hq_ContDiff