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

State before:
c z : Box
n : ℕ
⊢ (iterate c z nan n).exit = Exit.nan
Tactic:
rw [iterate]
State after:
c z : Box
n : ℕ
⊢ (if nan = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z nan 0 n).exit = Exit.nan

State before:
c z : Box
n : ℕ
⊢ (if nan = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z nan 0 n).exit = Exit.nan
Tactic:
simp only [ite_true, Function.iterate_zero]
State after:
no goals