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
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
⊢ k ≤
      (if z2 = nan then { z := z, n := k, exit := Exit.nan }
        else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n ∧
    (f' 2
              c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).z ∧
      ((if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).exit =
          Exit.large →
        rs' <
          Complex.abs
              ((f' 2
                    c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < z2.val then { z := z, n := k, exit := Exit.large }
                        else iterate' c w rs (k + 1) n).n -
                    k]
                z') ^
            2)
Tactic:
have we : w = z.sqr + c := by rw [←hw, Box.sqr, hzr2, hzi2]
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
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
⊢ k ≤
      (if z2 = nan then { z := z, n := k, exit := Exit.nan }
        else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n ∧
    (f' 2
              c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).z ∧
      ((if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).exit =
          Exit.large →
        rs' <
          Complex.abs
              ((f' 2
                    c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < z2.val then { z := z, n := k, exit := Exit.large }
                        else iterate' c w rs (k + 1) n).n -
                    k]
                z') ^
            2)