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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ s
⊢ P.partOf x = ∅
Tactic:
rw [← P.sUnion_eq] at hx
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ P.partOf x = ∅

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ P.partOf x = ∅
Tactic:
simp only [partOf, eq_empty_iff_forall_not_mem, mem_sUnion, mem_setOf, not_exists, not_and,
  and_imp]
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ ∀ (x_1 : α), ∀ x_2 ∈ P, x ∈ x_2 → x_1 ∉ x_2

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ ∀ (x_1 : α), ∀ x_2 ∈ P, x ∈ x_2 → x_1 ∉ x_2
Tactic:
exact fun y t ht hxt _ ↦ hx <| mem_sUnion_of_mem hxt ht
State after:
no goals