no goals
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x y : OnePoint X
⊢ Inseparable x y ↔ x = ∞ ∧ y = ∞ ∨ ∃ x', x = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
induction x using OnePoint.rec <;> induction y using OnePoint.rec <;>
  simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]