α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : α
hxy : Inseparable x y
⊢ x = y
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
⊢ T0Space α
refine' ⟨fun x y hxy => _⟩
case intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : α
hxy : Inseparable x y
s : Set α
hxs : x ∈ s
hys : y ∈ s
hs : T0Space ↑s
⊢ x = y
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : α
hxy : Inseparable x y
⊢ x = y
rcases h x y hxy with ⟨s, hxs, hys, hs⟩
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
y : α
s : Set α
hys : y ∈ s
hs : T0Space ↑s
x : { x // x ∈ s }
hxy : Inseparable (↑x) y
⊢ ↑x = y
case intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
x y : α
hxy : Inseparable x y
s : Set α
hxs : x ∈ s
hys : y ∈ s
hs : T0Space ↑s
⊢ x = y
lift x to s using hxs
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set α
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
y : α
s : Set α
hys : y ∈ s
hs : T0Space ↑s
x : { x // x ∈ s }
hxy : Inseparable (↑x) y
⊢ ↑x = y
lift y to s using hys
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set α
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable x y
⊢ ↑x = ↑y
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set α
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y
rw [← subtype_inseparable_iff] at hxy
no goals
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set α
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable x y
⊢ ↑x = ↑y
exact congr_arg Subtype.val hxy.eq