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

State before:
c' : ℂ
c : Box
cm : c' ∈ approx c
n : ℕ
r : Floating
⊢ _root_.potential 2 ↑c' ∈ approx (c.potential c n r).1
Tactic:
simp only [_root_.potential, RiemannSphere.fill_coe, mem_approx_potential cm cm]
State after:
no goals