refine ⟨?_, fun h ↦ ⟨_, ⟨a, refl_of_rel r h, rfl⟩, refl_of_rel r h, h⟩⟩
case h.h.a
α : Type u_1
inst✝⁴ : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a✝ b✝ : α
P : Partition s✝
r✝ : α → α → Prop
inst✝³ : IsSymm α r✝
inst✝² : IsTrans α r✝
s : Set α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) ↔ r a b
case h.h.a
α : Type u_1
inst✝⁴ : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a✝ b✝ : α
P : Partition s✝
r✝ : α → α → Prop
inst✝³ : IsSymm α r✝
inst✝² : IsTrans α r✝
s : Set α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) → r a b