Theorem: Partition.setOf_rel_self_eq (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 | P.Rel x x} = s
Tactic:
refine subset_antisymm (fun x hx ↦ ?_) (fun x hx ↦ ?_)
State after:
case refine_1
α : 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 ∈ {x | P.Rel x x}
⊢ x ∈ s

case refine_2
α : 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 ∈ {x | P.Rel x x}

State before:
case refine_2
α : 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 ∈ {x | P.Rel x x}
Tactic:
obtain ⟨t, ⟨ht, hxt⟩, -⟩ := P.exists_unique_of_mem_set hx
State after:
case refine_2.intro.intro.intro
α : 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
t : Set α
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ {x | P.Rel x x}

State before:
case refine_2.intro.intro.intro
α : 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
t : Set α
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ {x | P.Rel x x}
Tactic:
exact ⟨t, ht, hxt, hxt⟩
State after:
no goals

State before:
case refine_1
α : 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 ∈ {x | P.Rel x x}
⊢ x ∈ s
Tactic:
obtain ⟨t, ht, hxP, -⟩ := hx
State after:
case refine_1.intro.intro.intro
α : 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 : α
t : Set α
ht : t ∈ P
hxP : x ∈ t
⊢ x ∈ s

State before:
case refine_1.intro.intro.intro
α : 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 : α
t : Set α
ht : t ∈ P
hxP : x ∈ t
⊢ x ∈ s
Tactic:
exact subset_of_mem ht hxP
State after:
no goals