Theorem: Partition.setOf_rel_eq_partOf (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 α
P : Partition s
x : α
⊢ {y | P.Rel x y} = P.partOf x
Tactic:
by_cases hx : x ∈ s
State after:
case pos
α : 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 α
P : Partition s
x : α
hx : x ∈ s
⊢ {y | P.Rel x y} = P.partOf x

case neg
α : 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 α
P : Partition s
x : α
hx : x ∉ s
⊢ {y | P.Rel x y} = P.partOf x

State before:
case neg
α : 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 α
P : Partition s
x : α
hx : x ∉ s
⊢ {y | P.Rel x y} = P.partOf x
Tactic:
rw [partOf_eq_empty _ hx, eq_empty_iff_forall_not_mem]
State after:
case neg
α : 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 α
P : Partition s
x : α
hx : x ∉ s
⊢ ∀ (x_1 : α), x_1 ∉ {y | P.Rel x y}

State before:
case neg
α : 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 α
P : Partition s
x : α
hx : x ∉ s
⊢ ∀ (x_1 : α), x_1 ∉ {y | P.Rel x y}
Tactic:
exact fun y hxy ↦ hx <| Rel.mem_left hxy
State after:
no goals

State before:
case pos
α : 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 α
P : Partition s
x : α
hx : x ∈ s
⊢ {y | P.Rel x y} = P.partOf x
Tactic:
rw [setOf_rel_eq (P.partOf_mem hx) (P.mem_partOf hx)]
State after:
no goals