Theorem: iterate'_correct
Proof state before:
case succ
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
⊢ k ≤
      (if zr2.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
        else
          if rs.val < (zr2.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
          else iterate' c ({ re := zr2 - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n ∧
    (f' 2
              c')^[(if zr2.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
                else
                  if rs.val < (zr2.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
                  else iterate' c ({ re := zr2 - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if zr2.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (zr2.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := zr2 - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).z ∧
      ((if zr2.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (zr2.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := zr2 - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).exit =
          Exit.large →
        rs' <
          Complex.abs
              ((f' 2
                    c')^[(if zr2.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < (zr2.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
                        else iterate' c ({ re := zr2 - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
                    k]
                z') ^
            2)
Tactic:
generalize hzi2 : z.im.sqr = zi2
Proof state after:
case succ
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
⊢ k ≤
      (if zr2.lo.add zi2.lo false = nan then { z := z, n := k, exit := Exit.nan }
        else
          if rs.val < (zr2.lo.add zi2.lo false).val then { z := z, n := k, exit := Exit.large }
          else iterate' c ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n ∧
    (f' 2
              c')^[(if zr2.lo.add zi2.lo false = nan then { z := z, n := k, exit := Exit.nan }
                else
                  if rs.val < (zr2.lo.add zi2.lo false).val then { z := z, n := k, exit := Exit.large }
                  else iterate' c ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if zr2.lo.add zi2.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (zr2.lo.add zi2.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).z ∧
      ((if zr2.lo.add zi2.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (zr2.lo.add zi2.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).exit =
          Exit.large →
        rs' <
          Complex.abs
              ((f' 2
                    c')^[(if zr2.lo.add zi2.lo false = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < (zr2.lo.add zi2.lo false).val then { z := z, n := k, exit := Exit.large }
                        else iterate' c ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
                    k]
                z') ^
            2)