Theorem: iterate'_correct (Ray/Render/Iterate.lean)

State before:
c z : Box
rs : Floating
c' z' : ℂ
rs' : ℝ
cm : c' ∈ approx c
zm : z' ∈ approx z
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
k n : ℕ
⊢ 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)
Tactic:
induction' n with n h generalizing k z z'
State after:
case zero
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
⊢ let i := iterate' c z rs k 0;
  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)

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 : ℕ
⊢ let i := iterate' c z rs k (n + 1);
  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)

State before:
case zero
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
⊢ let i := iterate' c z rs k 0;
  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)
Tactic:
simpa only [iterate', le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero, id_eq,
  IsEmpty.forall_iff, and_true, true_and]
State after:
no goals

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 : ℕ
⊢ let i := iterate' c z rs k (n + 1);
  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)
Tactic:
simp only [iterate', Floating.val_lt_val]
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 : ℕ
⊢ k ≤
      (if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
        else
          if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
          else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n ∧
    (f' 2
              c')^[(if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
                else
                  if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
                  else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).z ∧
      ((if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := z.re.sqr - 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 z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
                        else
                          iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
                    k]
                z') ^
            2)

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 : ℕ
⊢ k ≤
      (if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
        else
          if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
          else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n ∧
    (f' 2
              c')^[(if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
                else
                  if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
                  else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).z ∧
      ((if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := z.re.sqr - 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 z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
                        else
                          iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
                    k]
                z') ^
            2)
Tactic:
generalize hzr2 : z.re.sqr = zr2
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
⊢ 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)

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
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)

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
⊢ 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)
Tactic:
generalize hz2 : zr2.lo.add zi2.lo false = z2
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
⊢ 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 ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) 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 ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) 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 ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) 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 ({ 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 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 ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
                    k]
                z') ^
            2)

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
⊢ 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 ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) 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 ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) 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 ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) 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 ({ 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 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 ({ re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
                    k]
                z') ^
            2)
Tactic:
generalize hw : (⟨zr2 - zi2, (z.re * z.im).scaleB 1⟩ : Box) + c = w
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
⊢ 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)

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]
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)

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
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)
Tactic:
have wa : f' 2 c' z' ∈ approx w := by rw [we, f']; mono
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
wa : f' 2 c' z' ∈ approx 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)

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
we : w = z.sqr + c
wa : f' 2 c' z' ∈ approx 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:
generalize hw' : f' 2 c' z' = w' at wa
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx 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)

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
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx 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:
by_cases z2n : z2 = nan
State after:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : z2 = nan
⊢ 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)

case neg
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
⊢ 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)

State before:
case neg
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
⊢ 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:
by_cases rz : rs.val < z2.val
State after:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ 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)

case neg
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
⊢ 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)

State before:
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
⊢ w = z.sqr + c
Tactic:
rw [←hw, Box.sqr, hzr2, hzi2]
State after:
no goals

State before:
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
⊢ f' 2 c' z' ∈ approx w
Tactic:
rw [we, f']
State after:
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
⊢ z' ^ 2 + c' ∈ approx (z.sqr + c)

State before:
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
⊢ z' ^ 2 + c' ∈ approx (z.sqr + c)
Tactic:
mono
State after:
no goals

State before:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : z2 = nan
⊢ 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:
simpa only [z2n, ite_true, le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero,
  id_eq, IsEmpty.forall_iff, and_true, true_and]
State after:
no goals

State before:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ 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:
simp only [z2n, rz, ite_true, le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero,
  id_eq, zm, forall_true_left, true_and, Complex.abs_def,
  Real.sq_sqrt (Complex.normSq_nonneg _), if_false]
State after:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ rs' < Complex.normSq z'

State before:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ rs' < Complex.normSq z'
Tactic:
refine lt_of_le_of_lt rsm (lt_of_lt_of_le rz ?_)
State after:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ z2.val ≤ Complex.normSq z'

State before:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ z2.val ≤ Complex.normSq z'
Tactic:
simp only [Complex.normSq_apply, ←sq, ←hz2, ←hzr2, ←hzi2] at z2n ⊢
State after:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2

State before:
case pos
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Tactic:
rcases Floating.ne_nan_of_add z2n with ⟨nr, ni⟩
State after:
case pos.intro
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : z.re.sqr.lo ≠ nan
ni : z.im.sqr.lo ≠ nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2

State before:
case pos.intro
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : z.re.sqr.lo ≠ nan
ni : z.im.sqr.lo ≠ nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Tactic:
simp only [ne_eq, Interval.lo_eq_nan] at nr ni
State after:
case pos.intro
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2

State before:
case pos.intro
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ (z.re.sqr.lo.add z.im.sqr.lo false).val ≤ z'.re ^ 2 + z'.im ^ 2
Tactic:
refine le_trans (Floating.add_le z2n) (add_le_add ?_ ?_)
State after:
case pos.intro.refine_1
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z.re.sqr.lo.val ≤ z'.re ^ 2

case pos.intro.refine_2
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z.im.sqr.lo.val ≤ z'.im ^ 2

State before:
case pos.intro.refine_1
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z.re.sqr.lo.val ≤ z'.re ^ 2
Tactic:
apply Interval.lo_le nr
State after:
case pos.intro.refine_1
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z'.re ^ 2 ∈ approx z.re.sqr

State before:
case pos.intro.refine_1
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z'.re ^ 2 ∈ approx z.re.sqr
Tactic:
mono
State after:
no goals

State before:
case pos.intro.refine_2
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z.im.sqr.lo.val ≤ z'.im ^ 2
Tactic:
apply Interval.lo_le ni
State after:
case pos.intro.refine_2
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z'.im ^ 2 ∈ approx z.im.sqr

State before:
case pos.intro.refine_2
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
rz : rs.val < z2.val
z2n : ¬z.re.sqr.lo.add z.im.sqr.lo false = nan
nr : ¬z.re.sqr = nan
ni : ¬z.im.sqr = nan
⊢ z'.im ^ 2 ∈ approx z.im.sqr
Tactic:
mono
State after:
no goals

State before:
case neg
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
⊢ 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:
simp only [rz, ite_false, z2n]
State after:
case neg
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
⊢ k ≤ (iterate' c w rs (k + 1) n).n ∧
    (f' 2 c')^[(iterate' c w rs (k + 1) n).n - k] z' ∈ approx (iterate' c w rs (k + 1) n).z ∧
      ((iterate' c w rs (k + 1) n).exit = Exit.large →
        rs' < Complex.abs ((f' 2 c')^[(iterate' c w rs (k + 1) n).n - k] z') ^ 2)

State before:
case neg
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
⊢ k ≤ (iterate' c w rs (k + 1) n).n ∧
    (f' 2 c')^[(iterate' c w rs (k + 1) n).n - k] z' ∈ approx (iterate' c w rs (k + 1) n).z ∧
      ((iterate' c w rs (k + 1) n).exit = Exit.large →
        rs' < Complex.abs ((f' 2 c')^[(iterate' c w rs (k + 1) n).n - k] z') ^ 2)
Tactic:
generalize hi : iterate' c w rs (k + 1) n = i
State after:
case neg
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)

State before:
case neg
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
specialize h wa (k+1)
State after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  let i := iterate' c w rs (k + 1) n;
  let w' := (f' 2 c')^[i.n - (k + 1)] w';
  k + 1 ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)

State before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  let i := iterate' c w rs (k + 1) n;
  let w' := (f' 2 c')^[i.n - (k + 1)] w';
  k + 1 ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
simp only [hi] at h
State after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)

State before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ k ≤ i.n ∧ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
refine ⟨by omega, ?_⟩
State after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)

State before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
have ie : i.n - k = (i.n - (k + 1)) + 1 := by omega
State after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
ie : i.n - k = i.n - (k + 1) + 1
⊢ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)

State before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
ie : i.n - k = i.n - (k + 1) + 1
⊢ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
rw [ie, Function.iterate_succ_apply, hw']
State after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
ie : i.n - k = i.n - (k + 1) + 1
⊢ (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
    (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)

State before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
ie : i.n - k = i.n - (k + 1) + 1
⊢ (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
    (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
Tactic:
exact h.2
State after:
no goals

State before:
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ k ≤ i.n
Tactic:
omega
State after:
no goals

State before:
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
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
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ i.n - k = i.n - (k + 1) + 1
Tactic:
omega
State after:
no goals