Theorem: Partition.exists_unique_of_mem_set (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
⊢ ∃! t, t ∈ P ∧ x ∈ t
Tactic:
rw [← P.sUnion_eq, mem_sUnion] 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 : ∃ t ∈ ↑P, x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : ∃ t ∈ ↑P, x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
Tactic:
obtain ⟨t, hxt⟩ := hx
State after:
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
t : Set α
hxt : t ∈ ↑P ∧ x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t

State before:
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
t : Set α
hxt : t ∈ ↑P ∧ x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
Tactic:
exact ⟨t, hxt, fun u ⟨huP, hxu⟩ ↦ eq_of_mem_inter huP hxt.1 ⟨hxu, hxt.2⟩⟩
State after:
no goals