Theorem: Partition.rel_iff_eqv_class_eq_right (Matroid/ForMathlib/SetPartition.lean)

State before:
α : 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 α
hy : r y y
⊢ r x y ↔ {z | r x z} = {z | r y z}
Tactic:
simp_rw [Set.ext_iff, mem_setOf]
State after:
α : 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 α
hy : r y y
⊢ r x y ↔ ∀ (x_1 : α), r x x_1 ↔ r y x_1

State before:
α : 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 α
hy : r y y
⊢ r x y ↔ ∀ (x_1 : α), r x x_1 ↔ r y x_1
Tactic:
refine' ⟨fun hxy z ↦ ⟨fun hxz ↦ trans_of r (symm_of r hxy) hxz,
  fun hyz ↦ trans_of r hxy hyz⟩, fun h ↦ by rwa [h]⟩
State after:
no goals

State before:
α : 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 α
hy : r y y
h : ∀ (x_1 : α), r x x_1 ↔ r y x_1
⊢ r x y
Tactic:
rwa [h]
State after:
no goals