Theorem: Partition.eq_partOf_of_mem (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
ht : t ∈ P
hxt : x ∈ t
⊢ t = P.partOf x
Tactic:
have hx : x ∈ s := by
  rw [← P.sUnion_eq]
  exact mem_sUnion_of_mem hxt ht
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
⊢ t = 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
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
⊢ t = P.partOf x
Tactic:
obtain ⟨t', ⟨-, h⟩⟩ := P.exists_unique_of_mem_set hx
State after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
t' : Set α
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t = P.partOf x

State before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
t' : Set α
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t = P.partOf x
Tactic:
rw [h t ⟨ht, hxt⟩, h (P.partOf x) ⟨P.partOf_mem hx, P.mem_partOf hx⟩]
State after:
no goals

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ s
Tactic:
rw [← P.sUnion_eq]
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ ⋃₀ ↑P

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ ⋃₀ ↑P
Tactic:
exact mem_sUnion_of_mem hxt ht
State after:
no goals