decide_lt_zero_foldPlusOneStep

proof body

Tactic-mode proof.

 168  classical
 169  set x : ℝ := u i
 170  have hx1 : (1 : Int) ≤ coeffMag x + 1 := by
 171    have hx0 : (0 : Int) ≤ coeffMag x := (Int.floor_nonneg (a := |x|)).2 (abs_nonneg x)
 172    linarith
 173  have hmpos : 0 < clampI32 (coeffMag x + 1) :=
 174    clampI32_pos_of_ge_one (x := coeffMag x + 1) hx1
 175  by_cases hx : x < 0
 176  ·
 177    have hzInt : (coeffSign x) * clampI32 (coeffMag x + 1) < 0 := by
 178      have hneg : -(clampI32 (coeffMag x + 1)) < 0 := neg_neg_of_pos hmpos
 179      calc
 180        (coeffSign x) * clampI32 (coeffMag x + 1)
 181            = (-1) * clampI32 (coeffMag x + 1) := by simp [coeffSign, hx]
 182        _ = -(clampI32 (coeffMag x + 1)) := by ring
 183        _ < 0 := hneg
 184    have hzReal :
 185        (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) < 0 :=
 186      (cast_lt_zero_iff (z := (coeffSign x) * clampI32 (coeffMag x + 1))).2 hzInt
 187    have hy : (foldPlusOneStep u) i < 0 := by
 188      simpa [foldPlusOneStep, x] using hzReal
 189    simp [x, hx, hy]
 190  ·
 191    have hzInt : (0 : Int) ≤ (coeffSign x) * clampI32 (coeffMag x + 1) := by
 192      have hm0 : (0 : Int) ≤ clampI32 (coeffMag x + 1) := le_of_lt hmpos
 193      simpa [coeffSign, hx] using hm0
 194    have hzReal :
 195        (0 : ℝ) ≤ (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) := by
 196      exact_mod_cast hzInt
 197    have hy : ¬ (foldPlusOneStep u) i < 0 := by
 198      have hy0 : (0 : ℝ) ≤ (foldPlusOneStep u) i := by
 199        simpa [foldPlusOneStep, x] using hzReal
 200      exact not_lt_of_ge hy0
 201    simp [x, hx, hy]
 202