Theorem: Partition.Rel.forall (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 α
h : P.Rel x y
ht : t ∈ P
⊢ x ∈ t ↔ y ∈ t
Tactic:
obtain ⟨t', ht', hx, hy⟩ := h
State after:
case 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 α
ht : t ∈ P
t' : Set α
ht' : t' ∈ P
hx : x ∈ t'
hy : y ∈ t'
⊢ x ∈ t ↔ y ∈ t

State before:
case 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 α
ht : t ∈ P
t' : Set α
ht' : t' ∈ P
hx : x ∈ t'
hy : y ∈ t'
⊢ x ∈ t ↔ y ∈ t
Tactic:
exact ⟨fun h ↦ by rwa [P.eq_of_mem_of_mem ht ht' h hx],
  fun h ↦ by rwa [P.eq_of_mem_of_mem ht ht' h hy]⟩
State after:
no goals

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 α
ht : t ∈ P
t' : Set α
ht' : t' ∈ P
hx : x ∈ t'
hy : y ∈ t'
h : x ∈ t
⊢ y ∈ t
Tactic:
rwa [P.eq_of_mem_of_mem ht ht' h hx]
State after:
no goals

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 α
ht : t ∈ P
t' : Set α
ht' : t' ∈ P
hx : x ∈ t'
hy : y ∈ t'
h : y ∈ t
⊢ x ∈ t
Tactic:
rwa [P.eq_of_mem_of_mem ht ht' h hy]
State after:
no goals