Theorem: Partition.rel_iff_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 α
P : Partition s
⊢ P.Rel x y ↔ x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
Tactic:
refine ⟨fun h ↦ ⟨h.mem_left, fun _ ↦ h.forall⟩,
  fun ⟨hxs, h⟩ ↦ ⟨P.partOf x, P.partOf_mem hxs, P.mem_partOf hxs, ?_⟩⟩
State after:
α : 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✝ : x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
hxs : x ∈ s
h : ∀ t ∈ P, x ∈ t ↔ y ∈ t
⊢ y ∈ P.partOf x

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✝ : x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
hxs : x ∈ s
h : ∀ t ∈ P, x ∈ t ↔ y ∈ t
⊢ y ∈ P.partOf x
Tactic:
rw [← h _ (P.partOf_mem hxs)]
State after:
α : 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✝ : x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
hxs : x ∈ s
h : ∀ t ∈ P, x ∈ t ↔ y ∈ t
⊢ x ∈ P.partOf x

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✝ : x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
hxs : x ∈ s
h : ∀ t ∈ P, x ∈ t ↔ y ∈ t
⊢ x ∈ P.partOf x
Tactic:
exact P.mem_partOf hxs
State after:
no goals