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

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

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

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

State before:
case pos
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
rsn : rs = nan
⊢ (f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z' ∈
    approx (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).z
Tactic:
simpa only [rsn, ite_true, Function.iterate_zero, id_eq]
State after:
no goals

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

State before:
case neg
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
rsn : ¬rs = nan
⊢ (f' 2 c')^[(iterate' c z rs 0 n).n] z' ∈ approx (iterate' c z rs 0 n).z
Tactic:
exact (iterate'_correct cm zm rsn (le_refl _) 0 n).2.1
State after:
no goals