α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c, c ∈ classes r ∧ x ∈ c ∧ y ∈ c
z : α
hx : x ∈ {x | Rel r x z}
hy : y ∈ {x | Rel r x z}
⊢ Rel r x y
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c, c ∈ classes r ∧ x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x | Rel r x z}
hx : x ∈ c
hy : y ∈ c
⊢ Rel r x y
subst c
no goals
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c, c ∈ classes r ∧ x ∈ c ∧ y ∈ c
z : α
hx : x ∈ {x | Rel r x z}
hy : y ∈ {x | Rel r x z}
⊢ Rel r x y
exact r.trans' hx (r.symm' hy)