Theorem: RiemannSphere.invCoePartialHomeomorph_target (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
⊢ invCoePartialHomeomorph.target = {0}ᶜ
Tactic:
ext z
State after:
case h
z : 𝕊
⊢ z ∈ invCoePartialHomeomorph.target ↔ z ∈ {0}ᶜ

State before:
case h
z : 𝕊
⊢ z ∈ invCoePartialHomeomorph.target ↔ z ∈ {0}ᶜ
Tactic:
simp only [invCoePartialHomeomorph, PartialHomeomorph.trans_toPartialEquiv,
PartialEquiv.trans_target, Homeomorph.toPartialHomeomorph_target, PartialHomeomorph.coe_coe_symm,
Homeomorph.toPartialHomeomorph_symm_apply, invHomeomorph_symm, coePartialHomeomorph_target,
preimage_compl, univ_inter, mem_compl_iff, mem_preimage, invHomeomorph_apply, mem_singleton_iff,
inv_eq_inf]
State after:
no goals