ode_cos_uniqueness

formal source

 254  have hEt := hE_eq t 0; simp only [hE0] at hEt
 255  nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
 256
 257private theorem ode_cos_uniqueness (f : ℝ → ℝ)
 258    (h_diff : ContDiff ℝ 2 f)
 259    (h_ode : ∀ t, deriv (deriv f) t = -(f t))
 260    (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
 261    ∀ t, f t = Real.cos t := by
 262  let g := fun t => f t - Real.cos t
 263  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
 264  have hDf : Differentiable ℝ f :=
 265    h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 266  have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
 267    intro t
 268    have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
 269      funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
 270    have hDf1 : ContDiff ℝ 1 (deriv f) := by
 271      rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
 272      exact (contDiff_succ_iff_deriv.mp h_diff).2.2
 273    have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
 274      rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
 275    have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
 276      rw [h1]; exact deriv_sub
 277        (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
 278        (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
 279    rw [h2, h_ode t]
 280    have : deriv (deriv Real.cos) t = -(Real.cos t) := by
 281      have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
 282      rw [h_dcos]; exact (Real.hasDerivAt_sin t).neg.deriv
 283    rw [this]; ring
 284  have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]
 285  have hg'0 : deriv g 0 = 0 := by
 286    have : deriv g 0 = deriv f 0 - deriv Real.cos 0 :=
 287      deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt