[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (Setoid.Rel toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (Setoid.Rel toSetoid✝ x))
x✝ :
  { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ }.toSetoid =
    { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }.toSetoid
⊢ { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
A : Set X
h : IsClopen A
x : X
⊢ IsOpen (setOf (Setoid.Rel { r := fun x y => x ∈ A ↔ y ∈ A, iseqv := (_ : Equivalence fun x y => x ∈ A ↔ y ∈ A) } x))
[PROOFSTEP]
by_cases hx : x ∈ A
[GOAL]
case pos
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
A : Set X
h : IsClopen A
x : X
hx : x ∈ A
⊢ IsOpen (setOf (Setoid.Rel { r := fun x y => x ∈ A ↔ y ∈ A, iseqv := (_ : Equivalence fun x y => x ∈ A ↔ y ∈ A) } x))
[PROOFSTEP]
simp [Setoid.Rel, hx, h.1, h.2, ← compl_setOf]
[GOAL]
case neg
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
A : Set X
h : IsClopen A
x : X
hx : ¬x ∈ A
⊢ IsOpen (setOf (Setoid.Rel { r := fun x y => x ∈ A ↔ y ∈ A, iseqv := (_ : Equivalence fun x y => x ∈ A ↔ y ∈ A) } x))
[PROOFSTEP]
simp [Setoid.Rel, hx, h.1, h.2, ← compl_setOf]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsOpen {proj S x}
[PROOFSTEP]
rw [← S.proj_quotientMap.isOpen_preimage, fiber_eq]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsOpen (setOf (Setoid.Rel S.toSetoid x))
[PROOFSTEP]
exact S.isOpen_setOf_rel _
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsClopen (setOf (Setoid.Rel S.toSetoid x))
[PROOFSTEP]
rw [← fiber_eq]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsClopen (proj S ⁻¹' {proj S x})
[PROOFSTEP]
apply isClopen_preimage
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S a : DiscreteQuotient X
⊢ a ≤ ⊤
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
⊢ ∀ (a b : Quotient ⊤.toSetoid), a = b
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
a✝² : Quotient ⊤.toSetoid
a✝¹ : X
b✝ : Quotient ⊤.toSetoid
a✝ : X
⊢ Quot.mk Setoid.r a✝¹ = Quot.mk Setoid.r a✝
[PROOFSTEP]
exact Quotient.sound trivial
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
g : C(Y, Z)
f : C(X, Y)
A B : DiscreteQuotient Y
h : A ≤ B
⊢ comap f A ≤ comap f B
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
⊢ ofLE (_ : A ≤ A) = id
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ ofLE (_ : A ≤ A) (Quot.mk Setoid.r a✝) = id (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
a : Quotient A.toSetoid
⊢ ofLE (_ : A ≤ A) a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
⊢ ofLE h₂ (ofLE h₁ x) = ofLE (_ : A ≤ C) x
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
a✝ : X
⊢ ofLE h₂ (ofLE h₁ (Quot.mk Setoid.r a✝)) = ofLE (_ : A ≤ C) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x : X
⊢ IsOpen (setOf (Setoid.Rel (connectedComponentSetoid X) x))
[PROOFSTEP]
convert isOpen_connectedComponent (x := x)
[GOAL]
case h.e'_3
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x : X
⊢ setOf (Setoid.Rel (connectedComponentSetoid X) x) = connectedComponent x
[PROOFSTEP]
ext y
[GOAL]
case h.e'_3.h
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x y : X
⊢ y ∈ setOf (Setoid.Rel (connectedComponentSetoid X) x) ↔ y ∈ connectedComponent x
[PROOFSTEP]
simpa only [connectedComponentSetoid, ← connectedComponent_eq_iff_mem] using eq_comm
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : DiscreteTopology X
x y : X
⊢ proj ⊥ x = proj ⊥ y ↔ x = y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
⊢ LEComap g B C → LEComap f A B → LEComap (ContinuousMap.comp g f) A C
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
⊢ map (ContinuousMap.id X) (_ : LEComap (ContinuousMap.id X) A A) = id
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) (_ : LEComap (ContinuousMap.id X) A A) (Quot.mk Setoid.r a✝) = id (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
⊢ map (ContinuousMap.comp g f) (_ : LEComap (ContinuousMap.comp g f) A C) = map g h1 ∘ map f h2
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.comp g f) (_ : LEComap (ContinuousMap.comp g f) A C) (Quot.mk Setoid.r a✝) =
    (map g h1 ∘ map f h2) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
⊢ ofLE h (map f cond a) = map f (_ : LEComap f A B') a
[PROOFSTEP]
rcases a with ⟨⟩
[GOAL]
case mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
a✝ : X
⊢ ofLE h (map f cond (Quot.mk Setoid.r a✝)) = map f (_ : LEComap f A B') (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
⊢ map f cond (ofLE h c) = map f (_ : LEComap f A' B) c
[PROOFSTEP]
rcases c with ⟨⟩
[GOAL]
case mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
a✝ : X
⊢ map f cond (ofLE h (Quot.mk Setoid.r a✝)) = map f (_ : LEComap f A' B) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
S : DiscreteQuotient X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), proj Q x = proj Q y
⊢ x = y
[PROOFSTEP]
rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_clopen, mem_iInter]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
S : DiscreteQuotient X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), proj Q x = proj Q y
⊢ ∀ (i : { Z // IsClopen Z ∧ y ∈ Z }), x ∈ ↑i
[PROOFSTEP]
rintro ⟨U, hU1, hU2⟩
[GOAL]
case mk.intro
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
S : DiscreteQuotient X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), proj Q x = proj Q y
U : Set X
hU1 : IsClopen U
hU2 : y ∈ U
⊢ x ∈ ↑{ val := U, property := (_ : IsClopen U ∧ y ∈ U) }
[PROOFSTEP]
exact (Quotient.exact' (h (ofClopen hU1))).mpr hU2
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : Quotient A.toSetoid
⊢ proj A ⁻¹' {a} ⊆ proj B ⁻¹' {ofLE h a}
[PROOFSTEP]
rcases A.proj_surjective a with ⟨a, rfl⟩
[GOAL]
case intro
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ proj A ⁻¹' {proj A a} ⊆ proj B ⁻¹' {ofLE h (proj A a)}
[PROOFSTEP]
rw [fiber_eq, ofLE_proj, fiber_eq]
[GOAL]
case intro
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ setOf (Setoid.Rel A.toSetoid a) ⊆ setOf (Setoid.Rel B.toSetoid a)
[PROOFSTEP]
exact fun _ h' => h h'
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
[PROOFSTEP]
have H₁ : ∀ Q₁ Q₂, Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂} := fun _ _ h =>
  by
  rw [← compat _ _ h]
  exact fiber_subset_ofLE _ _
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ proj x✝¹ ⁻¹' {Qs x✝¹} ⊆ proj x✝ ⁻¹' {Qs x✝}
[PROOFSTEP]
rw [← compat _ _ h]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ proj x✝¹ ⁻¹' {Qs x✝¹} ⊆ proj x✝ ⁻¹' {ofLE h (Qs x✝¹)}
[PROOFSTEP]
exact fiber_subset_ofLE _ _
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
[PROOFSTEP]
obtain ⟨x, hx⟩ : Set.Nonempty (⋂ Q, proj Q ⁻¹' {Qs Q}) :=
  IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _})
    (directed_of_inf H₁) (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
    (fun Q => (Q.isClosed_preimage {Qs _}).isCompact) fun Q => Q.isClosed_preimage _
[GOAL]
case intro
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂}
x : X
hx : x ∈ ⋂ (Q : DiscreteQuotient X), proj Q ⁻¹' {Qs Q}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
[PROOFSTEP]
exact ⟨x, mem_iInter.1 hx⟩
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
⊢ Finite (Quotient S.toSetoid)
[PROOFSTEP]
have : CompactSpace S := Quotient.compactSpace
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
this : CompactSpace (Quotient S.toSetoid)
⊢ Finite (Quotient S.toSetoid)
[PROOFSTEP]
rwa [← isCompact_univ_iff, isCompact_iff_finite, finite_univ_iff] at this 
