no goals
α : Type ?u.13387
X : Type u_1
Y : Type ?u.13393
Z : Type ?u.13396
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
a : Quotient A.toSetoid
⊢ ofLE (_ : A ≤ A) a = a
simp