case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x y : α
⊢ y ∈ proj hs ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (↑(equivQuotient hs).symm (Quotient.mk'' x))
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x : α
⊢ proj hs ⁻¹' {Quotient.mk'' x} = s (↑(equivQuotient hs).symm (Quotient.mk'' x))
ext y
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x y : α
⊢ proj hs y = Quotient.mk'' x ↔ index hs y = ↑(equivQuotient hs).symm (Quotient.mk'' x)
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x y : α
⊢ y ∈ proj hs ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (↑(equivQuotient hs).symm (Quotient.mk'' x))
simp only [Set.mem_preimage, Set.mem_singleton_iff, hs.mem_iff_index_eq]
no goals
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x y : α
⊢ proj hs y = Quotient.mk'' x ↔ index hs y = ↑(equivQuotient hs).symm (Quotient.mk'' x)
exact Quotient.eq''