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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P : Partition s
x : α
ht : t ∈ P
hu : u ∈ P
hx : x ∈ t ∩ u
hdj : Disjoint t u
⊢ False
Tactic:
simp [hdj.inter_eq] at hx
State after:
no goals