case intro
α : Type u_1
r : Setoid α
a y : α
ha : a ∈ {x | Rel r x y}
⊢ {x | Rel r x y} = {x | Rel r x a}
α : Type u_1
r : Setoid α
a : α
⊢ ∀ (y : Set α), y ∈ classes r → a ∈ y → y = {x | Rel r x a}
rintro _ ⟨y, rfl⟩ ha
case intro.h
α : Type u_1
r : Setoid α
a y : α
ha : a ∈ {x | Rel r x y}
x : α
⊢ x ∈ {x | Rel r x y} ↔ x ∈ {x | Rel r x a}
case intro
α : Type u_1
r : Setoid α
a y : α
ha : a ∈ {x | Rel r x y}
⊢ {x | Rel r x y} = {x | Rel r x a}
ext x
no goals
case intro.h
α : Type u_1
r : Setoid α
a y : α
ha : a ∈ {x | Rel r x y}
x : α
⊢ x ∈ {x | Rel r x y} ↔ x ∈ {x | Rel r x a}
exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩