ZetaAppendix.lemma_approx_monotone_C1

theorem lemma_approx_monotone_C1 {a b : ℝ} (hab : a < b) (g : ℝ → ℝ)    (hg_cont : ContinuousOn g (Set.Icc a b)) (hg_mono : MonotoneOn g (Set.Icc a b)) :    ∀ ε > 0, ∃ g' : ℝ → ℝ, ContDiffOn ℝ 1 g' (Set.Icc a b) ∧ MonotoneOn g' (Set.Icc a b) ∧      ∀ x ∈ Set.Icc a b, |g x - g' x| < ε := by  intro ε hε_pos  set f := fun t : unitInterval ↦ g (a + t.val * (b - a)) with hf_def  obtain ⟨P, hP_cont, hP_mono, hP_approx⟩ : ∃ P : ℝ → ℝ, ContDiffOn ℝ 1 P unitInterval ∧    MonotoneOn P unitInterval ∧ ∀ t : unitInterval, |f t - P t| < ε := by    have hf_cont : ContinuousOn f (Set.univ : Set unitInterval) :=      hg_cont.comp (Continuous.continuousOn (by continuity)) fun x hx ↦        ⟨by nlinarith [x.2.1, x.2.2], by nlinarith [x.2.1, x.2.2]⟩    have hf_mono : Monotone f :=      fun x y hxy ↦ hg_mono ⟨by nlinarith [x.2.1, x.2.2], by nlinarith [x.2.1, x.2.2]⟩ ⟨by nlinarith [y.2.1, y.2.2],        by nlinarith [y.2.1, y.2.2]⟩ (by nlinarith [x.2.1, x.2.2, y.2.1, y.2.2, show (x : ℝ) ≤ y from hxy])    have := @lemma_approx_monotone_C1_I    exact this ⟨f, by simpa using hf_cont⟩ hf_mono ε hε_pos  refine ⟨fun x ↦ P ((x - a) / (b - a)), ?_, ?_, ?_⟩  · simp_all only [MonotoneOn, Set.mem_Icc, and_imp, gt_iff_lt, Subtype.forall]    refine hP_cont.comp (ContDiffOn.div_const (contDiffOn_id.sub contDiffOn_const) _)      fun x hx ↦ ⟨?_, ?_⟩ <;> nlinarith [hx.1, hx.2, mul_div_cancel₀ (x - a) (sub_ne_zero_of_ne hab.ne')]  · simp_all only [MonotoneOn, Set.mem_Icc, and_imp, gt_iff_lt, Subtype.forall]    exact fun x hx₁ hx₂ y hy₁ hy₂ hxy ↦ hP_mono (div_nonneg (by linarith) (by linarith))      (div_le_one_of_le₀ (by linarith) (by linarith)) (div_nonneg (by linarith) (by linarith))        (div_le_one_of_le₀ (by linarith) (by linarith)) (div_le_div_of_nonneg_right (by linarith) (by linarith))  · simp_all only [MonotoneOn, Set.mem_Icc, and_imp, gt_iff_lt, Subtype.forall]    intro x hx₁ hx₂    convert hP_approx ((x - a) / (b - a)) (div_nonneg (by linarith) (by linarith))      (div_le_one_of_le₀ (by linarith) (by linarith)) using 1    congr 1    rw [div_mul_cancel₀ _ (by linarith)]    ring_nf