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

State before:
c z : Box
rs : Floating
n : ℕ
e : (iterate c z rs n).exit ≠ Exit.nan
⊢ rs ≠ nan
Tactic:
contrapose e
State after:
c z : Box
rs : Floating
n : ℕ
e : ¬rs ≠ nan
⊢ ¬(iterate c z rs n).exit ≠ Exit.nan

State before:
c z : Box
rs : Floating
n : ℕ
e : ¬rs ≠ nan
⊢ ¬(iterate c z rs n).exit ≠ Exit.nan
Tactic:
simp only [ne_eq, not_not] at e
State after:
c z : Box
rs : Floating
n : ℕ
e : rs = nan
⊢ ¬(iterate c z rs n).exit ≠ Exit.nan

State before:
c z : Box
rs : Floating
n : ℕ
e : rs = nan
⊢ ¬(iterate c z rs n).exit ≠ Exit.nan
Tactic:
simp only [e, iterate_nan, ne_eq, not_true_eq_false, not_false_eq_true]
State after:
no goals