Theorem: Box.mem_approx_potential (Ray/Render/Potential.lean)

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
⊢ ⋯.potential c' ↑z' ∈ approx (c.potential z n r).1
Tactic:
set s := superF 2
State after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ s.potential c' ↑z' ∈ approx (c.potential z n r).1

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ s.potential c' ↑z' ∈ approx (c.potential z n r).1
Tactic:
rw [Box.potential]
State after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := c.normSq.hi;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := c.normSq.hi;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
generalize hcs : (normSq c).hi = cs
State after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
generalize hi : iterate c z (cs.max 9) n = i
State after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
by_cases csn : cs = nan
State after:
case pos
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [hi, Interval.hi_eq_nan, Floating.val_lt_val]
State after:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
generalize hie : i.exit = ie
State after:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
ie : Exit
hie : i.exit = ie
⊢ s.potential c' ↑z' ∈
    approx
      (match ie with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
ie : Exit
hie : i.exit = ie
⊢ s.potential c' ↑z' ∈
    approx
      (match ie with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
induction ie
State after:
case neg.count
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

case neg.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

case neg.nan
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.nan
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.nan with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
case pos
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [csn, Floating.nan_max, iterate_nan, Interval.approx_nan, mem_univ]
State after:
no goals

State before:
case neg.count
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
generalize hzs : (normSq i.z) = zs
State after:
case neg.count
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
case neg.count
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
by_cases bad : zs = nan ∨ (16 : Floating).val < zs.hi.val ∨ (16 : Floating).val < cs.val
State after:
case pos
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
bad : zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬(zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val)
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
case pos
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
bad : zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [Floating.val_lt_val, bad, ↓reduceIte, Interval.approx_nan, mem_univ]
State after:
no goals

State before:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬(zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val)
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [bad, ↓reduceIte]
State after:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬(zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val)
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)

State before:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬(zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val)
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
simp only [not_or, not_lt, ←hzs] at bad
State after:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬i.z.normSq = nan ∧ i.z.normSq.hi.val ≤ 16.val ∧ cs.val ≤ 16.val
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)

State before:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬i.z.normSq = nan ∧ i.z.normSq.hi.val ≤ 16.val ∧ cs.val ≤ 16.val
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
rcases bad with ⟨zsn, z4, c4⟩
State after:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16.val
c4 : cs.val ≤ 16.val
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)

State before:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16.val
c4 : cs.val ≤ 16.val
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
rw [Floating.val_ofNat] at c4 z4
State after:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ ↑16
c4 : cs.val ≤ ↑16
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)

State before:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ ↑16
c4 : cs.val ≤ ↑16
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
simp only [← hcs, Nat.cast_ofNat, Interval.hi_eq_nan] at c4 z4 csn zsn
State after:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)

State before:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
apply Interval.mem_approx_iter_sqrt' s.potential_nonneg
State after:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
⊢ s.potential c' ↑z' ^ 2 ^ i.n ∈ approx potential_small

State before:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
⊢ s.potential c' ↑z' ^ 2 ^ i.n ∈ approx potential_small
Tactic:
simp only [←s.potential_eqn_iter, f_f'_iter]
State after:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
⊢ s.potential c' ↑((f' 2 c')^[i.n] z') ∈ approx potential_small

State before:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
⊢ s.potential c' ↑((f' 2 c')^[i.n] z') ∈ approx potential_small
Tactic:
generalize hw' : (f' 2 c')^[i.n] z' = w'
State after:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
⊢ s.potential c' ↑w' ∈ approx potential_small

State before:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
⊢ s.potential c' ↑w' ∈ approx potential_small
Tactic:
have le4 : Real.sqrt 16 ≤ 4 := by rw [Real.sqrt_le_iff]; norm_num
State after:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ s.potential c' ↑w' ∈ approx potential_small

State before:
case neg.intro.intro
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ s.potential c' ↑w' ∈ approx potential_small
Tactic:
apply approx_potential_small
State after:
case neg.intro.intro.c4
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ Complex.abs c' ≤ 4

case neg.intro.intro.z4
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ Complex.abs w' ≤ 4

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
⊢ √16 ≤ 4
Tactic:
rw [Real.sqrt_le_iff]
State after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
⊢ 0 ≤ 4 ∧ 16 ≤ 4 ^ 2

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
⊢ 0 ≤ 4 ∧ 16 ≤ 4 ^ 2
Tactic:
norm_num
State after:
no goals

State before:
case neg.intro.intro.c4
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ Complex.abs c' ≤ 4
Tactic:
exact le_trans (Box.abs_le_sqrt_normSq cm csn) (le_trans (Real.sqrt_le_sqrt c4) le4)
State after:
no goals

State before:
case neg.intro.intro.z4
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ Complex.abs w' ≤ 4
Tactic:
refine le_trans (Box.abs_le_sqrt_normSq ?_ zsn) (le_trans (Real.sqrt_le_sqrt z4) le4)
State after:
case neg.intro.intro.z4
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ w' ∈ approx i.z

State before:
case neg.intro.intro.z4
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ w' ∈ approx i.z
Tactic:
rw [←hw', ←hi]
State after:
case neg.intro.intro.z4
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ (f' 2 c')^[(iterate c z (cs.max 9) n).n] z' ∈ approx (iterate c z (cs.max 9) n).z

State before:
case neg.intro.intro.z4
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
hie : i.exit = Exit.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ (f' 2 c')^[(iterate c z (cs.max 9) n).n] z' ∈ approx (iterate c z (cs.max 9) n).z
Tactic:
exact mem_approx_iterate cm zm _
State after:
no goals

State before:
case neg.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
generalize hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
State after:
case neg.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

State before:
case neg.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [hj]
State after:
case neg.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
⊢ s.potential c' ↑z' ∈
    approx
      (match j.exit with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1

State before:
case neg.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
⊢ s.potential c' ↑z' ∈
    approx
      (match j.exit with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
generalize hje : j.exit = je
State after:
case neg.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
je : Exit
hje : j.exit = je
⊢ s.potential c' ↑z' ∈
    approx
      (match je with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1

State before:
case neg.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
je : Exit
hje : j.exit = je
⊢ s.potential c' ↑z' ∈
    approx
      (match je with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
induction je
State after:
case neg.large.count
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.count
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1

case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.large
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1

case neg.large.nan
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.nan
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.nan with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1

State before:
case neg.large.count
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.count
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
simp only [Interval.approx_nan, mem_univ]
State after:
no goals

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.large
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
simp only
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.large
⊢ s.potential c' ↑z' ∈ approx (j.z.potential_large.iter_sqrt (i.n + j.n))

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.large
⊢ s.potential c' ↑z' ∈ approx (j.z.potential_large.iter_sqrt (i.n + j.n))
Tactic:
generalize hn : i.n + j.n = n
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.large
n : ℕ
hn : i.n + j.n = n
⊢ s.potential c' ↑z' ∈ approx (j.z.potential_large.iter_sqrt n)

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.large
n : ℕ
hn : i.n + j.n = n
⊢ s.potential c' ↑z' ∈ approx (j.z.potential_large.iter_sqrt n)
Tactic:
apply Interval.mem_approx_iter_sqrt' s.potential_nonneg
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.large
n : ℕ
hn : i.n + j.n = n
⊢ s.potential c' ↑z' ^ 2 ^ n ∈ approx j.z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.large
n : ℕ
hn : i.n + j.n = n
⊢ s.potential c' ↑z' ^ 2 ^ n ∈ approx j.z.potential_large
Tactic:
simp only [←s.potential_eqn_iter, f_f'_iter, ←hj] at hje ⊢
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
⊢ s.potential c' ↑((f' 2 c')^[n] z') ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
⊢ s.potential c' ↑((f' 2 c')^[n] z') ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
generalize hw' : (f' 2 c')^[n] z' = w'
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
have izm : (f' 2 c')^[i.n] z' ∈ approx i.z := by rw [←hi]; exact mem_approx_iterate cm zm _
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
have jl := iterate_large cm izm hje
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl :
  ((r.mul r true).max (cs.max 36)).val <
    Complex.abs ((f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z')) ^ 2
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl :
  ((r.mul r true).max (cs.max 36)).val <
    Complex.abs ((f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z')) ^ 2
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
have jrn := ne_nan_of_iterate (hje.trans_ne (by decide))
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl :
  ((r.mul r true).max (cs.max 36)).val <
    Complex.abs ((f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z')) ^ 2
jrn : (r.mul r true).max (cs.max 36) ≠ nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl :
  ((r.mul r true).max (cs.max 36)).val <
    Complex.abs ((f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z')) ^ 2
jrn : (r.mul r true).max (cs.max 36) ≠ nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
simp only [hj, ← Function.iterate_add_apply, add_comm _ i.n, hn, hw'] at jl
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jrn : (r.mul r true).max (cs.max 36) ≠ nan
jl : ((r.mul r true).max (cs.max 36)).val < Complex.abs w' ^ 2
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jrn : (r.mul r true).max (cs.max 36) ≠ nan
jl : ((r.mul r true).max (cs.max 36)).val < Complex.abs w' ^ 2
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
simp only [ne_eq, Floating.max_eq_nan, not_or] at jrn
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : ((r.mul r true).max (cs.max 36)).val < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : ((r.mul r true).max (cs.max 36)).val < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
rw [Floating.val_max jrn.1 (Floating.max_ne_nan.mpr jrn.2),
  Floating.val_max jrn.2.1 jrn.2.2, max_lt_iff, max_lt_iff, Floating.val_ofNat,
  Nat.cast_eq_ofNat] at jl
State after:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large

State before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
apply approx_potential_large
State after:
case neg.large.large.cz
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ Complex.abs c' ≤ Complex.abs w'

case neg.large.large.z6
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 6 ≤ Complex.abs w'

case neg.large.large.zm
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
⊢ (f' 2 c')^[i.n] z' ∈ approx i.z
Tactic:
rw [←hi]
State after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
⊢ (f' 2 c')^[(iterate c z (cs.max 9) n✝).n] z' ∈ approx (iterate c z (cs.max 9) n✝).z

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
⊢ (f' 2 c')^[(iterate c z (cs.max 9) n✝).n] z' ∈ approx (iterate c z (cs.max 9) n✝).z
Tactic:
exact mem_approx_iterate cm zm _
State after:
no goals

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl :
  ((r.mul r true).max (cs.max 36)).val <
    Complex.abs ((f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z')) ^ 2
⊢ Exit.large ≠ Exit.nan
Tactic:
decide
State after:
no goals

State before:
case neg.large.large.cz
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ Complex.abs c' ≤ Complex.abs w'
Tactic:
refine le_trans ?_ (le_trans (Real.sqrt_le_sqrt jl.2.1.le) ?_)
State after:
case neg.large.large.cz.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ Complex.abs c' ≤ cs.val.sqrt

case neg.large.large.cz.refine_2
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (Complex.abs w' ^ 2).sqrt ≤ Complex.abs w'

State before:
case neg.large.large.cz.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ Complex.abs c' ≤ cs.val.sqrt
Tactic:
simp only [← hcs, Interval.hi_eq_nan] at csn ⊢
State after:
case neg.large.large.cz.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
csn : ¬c.normSq = nan
⊢ Complex.abs c' ≤ c.normSq.hi.val.sqrt

State before:
case neg.large.large.cz.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
csn : ¬c.normSq = nan
⊢ Complex.abs c' ≤ c.normSq.hi.val.sqrt
Tactic:
exact abs_le_sqrt_normSq cm csn
State after:
no goals

State before:
case neg.large.large.cz.refine_2
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (Complex.abs w' ^ 2).sqrt ≤ Complex.abs w'
Tactic:
simp only [apply_nonneg, Real.sqrt_sq, le_refl]
State after:
no goals

State before:
case neg.large.large.z6
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 6 ≤ Complex.abs w'
Tactic:
refine le_trans ?_ (le_trans (Real.sqrt_le_sqrt jl.2.2.le) ?_)
State after:
case neg.large.large.z6.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 6 ≤ √36

case neg.large.large.z6.refine_2
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (Complex.abs w' ^ 2).sqrt ≤ Complex.abs w'

State before:
case neg.large.large.z6.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 6 ≤ √36
Tactic:
have e : (36 : ℝ) = 6 ^ 2 := by norm_num
State after:
case neg.large.large.z6.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
e : 36 = 6 ^ 2
⊢ 6 ≤ √36

State before:
case neg.large.large.z6.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
e : 36 = 6 ^ 2
⊢ 6 ≤ √36
Tactic:
rw [e, Real.sqrt_sq (by norm_num)]
State after:
no goals

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 36 = 6 ^ 2
Tactic:
norm_num
State after:
no goals

State before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
e : 36 = 6 ^ 2
⊢ 0 ≤ 6
Tactic:
norm_num
State after:
no goals

State before:
case neg.large.large.z6.refine_2
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (Complex.abs w' ^ 2).sqrt ≤ Complex.abs w'
Tactic:
simp only [apply_nonneg, Real.sqrt_sq, le_refl]
State after:
no goals

State before:
case neg.large.large.zm
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z
Tactic:
rw [←hw', ←hn, add_comm _ j.n, Function.iterate_add_apply, ←hj]
State after:
case neg.large.large.zm
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z') ∈
    approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z

State before:
case neg.large.large.zm
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z') ∈
    approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z
Tactic:
exact mem_approx_iterate cm izm _
State after:
no goals

State before:
case neg.large.nan
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.nan
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.nan with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
simp only [Interval.approx_nan, mem_univ]
State after:
no goals

State before:
case neg.nan
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.nan
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.nan with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [Interval.approx_nan, mem_univ]
State after:
no goals