Theorem: iterate_large (Ray/Render/Iterate.lean)

State before:
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (iterate c z rs n).exit = Exit.large
⊢ rs.val < Complex.abs ((f' 2 c')^[(iterate c z rs n).n] z') ^ 2
Tactic:
rw [iterate] at l ⊢
State after:
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2

State before:
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2
Tactic:
by_cases rsn : rs = nan
State after:
case pos
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
rsn : rs = nan
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2

case neg
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
rsn : ¬rs = nan
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2

State before:
case pos
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
rsn : rs = nan
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2
Tactic:
simp only [rsn, ↓reduceIte] at l
State after:
no goals

State before:
case neg
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
rsn : ¬rs = nan
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2
Tactic:
simp only [rsn, ite_false] at l ⊢
State after:
case neg
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
rsn : ¬rs = nan
l : (iterate' c z rs 0 n).exit = Exit.large
⊢ rs.val < Complex.abs ((f' 2 c')^[(iterate' c z rs 0 n).n] z') ^ 2

State before:
case neg
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
rsn : ¬rs = nan
l : (iterate' c z rs 0 n).exit = Exit.large
⊢ rs.val < Complex.abs ((f' 2 c')^[(iterate' c z rs 0 n).n] z') ^ 2
Tactic:
simpa only [not_lt, Nat.sub_zero] using (iterate'_correct cm zm rsn (le_refl _) 0 n).2.2 l
State after:
no goals