Theorem: Partition.mem_ofRel'_iff (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 t : Set α
hs : s = {x | r x x}
⊢ t ∈ ofRel' r hs ↔ ∃ x ∈ s, t = {y | r x y}
Tactic:
subst hs
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
t : Set α
⊢ t ∈ ofRel' r ⋯ ↔ ∃ x ∈ {x | r x x}, t = {y | r x y}

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
t : Set α
⊢ t ∈ ofRel' r ⋯ ↔ ∃ x ∈ {x | r x x}, t = {y | r x y}
Tactic:
simp [ofRel', mem_congr_iff, mem_ofRel_iff]
State after:
no goals