ψ_formula₁

lemma ψ_formula₁ {x : ℝ} (hx : 1 / (4 * D) ≤ x ∧ x ≤ 1 / (2 * D)) :    ψ D x = 4 * D * x - 1 := by  have : x ≥ 0 := le_trans (one_div_nonneg.2 (by linarith)) hx.1  have hx1 := (div_le_iff₀' (by linarith)).1 hx.1  have hx2 := (le_div_iff₀' (by linarith)).1 hx.2  have ineq₀ : 4 * D * x - 1 ≤ 2 - 4 * x := by    suffices (2 * D + 2 * D + 4) * x ≤ 3 by linarith    exact le_trans (by gcongr; linarith [D2 hD]) (by linarith: (2 * D + 2 * D + 2 * D) * x ≤ 3)  have ineq₁ : 4 * D * x - 1 ≤ 1 := by linarith  have ineq₂ : 0 ≤ 4 * D * x - 1 := by linarith  rw [ψ, min_eq_left ineq₀, min_eq_right ineq₁, max_eq_right ineq₂]