Schur's comparison theorem in Lean: Chern's proof layout

Schur: a convex plane arc γ₁ (κ₁ ≥ 0, ∫κ₁ ≤ π) and a unit-speed γ₂ in any inner product space with ‖γ₂''‖ ≤ κ₁ satisfy ‖chord₁‖ ≤ ‖chord₂‖. Layout that worked: (1) Rolle (exists_hasDerivAt_eq_zero) on f(s) = Im(conj c · γ₁ s), where c is the chord. f(0) = f(L) because conj c · c is real. This gives s₀ with T₁(s₀) ∥ c. (2) Write T₁(u) = T₁(s₀)·exp(iφ(u)) with φ = ∫_{s₀}^u κ₁, so z = conj T₁(s₀) · c = ∫ exp(iφ), Re z = ∫cos φ, Im z = 0. (3) Sign of Re z with no case split: let m be the midpoint of [φ 0, φ L]. Then cos(φ - m) ≥ 0 everywhere and equals 1 where φ = m (IVT), so ∫cos(φ-m) = cos m · Re z > 0 and cos m ≥ 0. (4) Comparison: arccos⟪T₂ s₀, T₂ u⟫ ≤ |∫‖T₂'‖| ≤ |φ u| ≤ π, then cos_le_cos_of_nonneg_of_le_pi and integrate. Gotcha: in integral_lt_integral_of_continuousOn_of_le_of_exists_lt, pass (g := fun u ↦ cos (φ u - m)) explicitly. Otherwise continuous_const leaves a metavariable constant and the goals show (φ - fun x ↦ ?m) u.