-- Mathlib/Topology/Separation/Basic.lean
theorem SeparationQuotient.t1Space_iff : T1Space (SeparationQuotient X) ↔ R0Space X

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) → Symmetric Specializes

Tactic:
intro h x y xspecy

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
x y : X
xspecy : x ⤳ y
⊢ y ⤳ x

Proof state:
case mpr.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Symmetric Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ x ⤳ y ∧ y ⤳ x

Tactic:
exact ⟨xspecy, yspecx⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ T1Space (SeparationQuotient X) ↔ R0Space X

Tactic:
rw [r0Space_iff, ((t1Space_TFAE (SeparationQuotient X)).out 0 9 :)]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Symmetric Specializes

Proof state:
case mpr.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Symmetric Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
⊢ Quot.mk (⇑(inseparableSetoid X)) x = Quot.mk (⇑(inseparableSetoid X)) y

Tactic:
have yspecx : y ⤳ x := h xspecy

Result:
case mpr.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Symmetric Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ Quot.mk (⇑(inseparableSetoid X)) x = Quot.mk (⇑(inseparableSetoid X)) y

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Symmetric Specializes

Tactic:
constructor

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) → Symmetric Specializes

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Symmetric Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
x y : X
xspecy : x ⤳ y
⊢ y ⤳ x

Tactic:
rw [← IsInducing.specializes_iff isInducing_mk, h xspecy] at *

Result:
no goals

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Symmetric Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y

Tactic:
rintro h ⟨x⟩ ⟨y⟩ sxspecsy

Result:
case mpr.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Symmetric Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
⊢ Quot.mk (⇑(inseparableSetoid X)) x = Quot.mk (⇑(inseparableSetoid X)) y

Proof state:
case mpr.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Symmetric Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
⊢ Quot.mk (⇑(inseparableSetoid X)) x = Quot.mk (⇑(inseparableSetoid X)) y

Tactic:
have xspecy : x ⤳ y := isInducing_mk.specializes_iff.mp sxspecsy

Result:
case mpr.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Symmetric Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
⊢ Quot.mk (⇑(inseparableSetoid X)) x = Quot.mk (⇑(inseparableSetoid X)) y

Proof state:
case mpr.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Symmetric Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ Quot.mk (⇑(inseparableSetoid X)) x = Quot.mk (⇑(inseparableSetoid X)) y

Tactic:
erw [mk_eq_mk, inseparable_iff_specializes_and]

Result:
case mpr.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Symmetric Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ x ⤳ y ∧ y ⤳ x