Theorem: Partition.ofRel_rel_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
⊢ ofRel' P.Rel ⋯ = P
Tactic:
ext a
State after:
case hP
α : 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
a : Set α
⊢ a ∈ ofRel' P.Rel ⋯ ↔ a ∈ P

State before:
case hP
α : 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
a : Set α
⊢ a ∈ ofRel' P.Rel ⋯ ↔ a ∈ P
Tactic:
simp only [mem_ofRel'_iff]
State after:
case hP
α : 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
a : Set α
⊢ (∃ x ∈ s, a = {y | P.Rel x y}) ↔ a ∈ P

State before:
case hP
α : 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
a : Set α
⊢ (∃ x ∈ s, a = {y | P.Rel x y}) ↔ a ∈ P
Tactic:
refine ⟨?_, fun h ↦ ?_⟩
State after:
case hP.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
a : Set α
⊢ (∃ x ∈ s, a = {y | P.Rel x y}) → a ∈ P

case hP.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
a : Set α
h : a ∈ P
⊢ ∃ x ∈ s, a = {y | P.Rel x y}

State before:
case hP.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
a : Set α
h : a ∈ P
⊢ ∃ x ∈ s, a = {y | P.Rel x y}
Tactic:
obtain ⟨x, hx⟩ := P.nonempty_of_mem h
State after:
case hP.refine_2.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
a : Set α
h : a ∈ P
x : α
hx : x ∈ a
⊢ ∃ x ∈ s, a = {y | P.Rel x y}

State before:
case hP.refine_2.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
a : Set α
h : a ∈ P
x : α
hx : x ∈ a
⊢ ∃ x ∈ s, a = {y | P.Rel x y}
Tactic:
exact ⟨x, (P.subset_of_mem h) hx, by rwa [setOf_rel_eq _ hx]⟩
State after:
no goals

State before:
case hP.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
a : Set α
⊢ (∃ x ∈ s, a = {y | P.Rel x y}) → a ∈ P
Tactic:
rintro ⟨x,hx, rfl⟩
State after:
case hP.refine_1.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
⊢ {y | P.Rel x y} ∈ P

State before:
case hP.refine_1.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
⊢ {y | P.Rel x y} ∈ P
Tactic:
exact setOf_rel_mem _ 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 α
P : Partition s
a : Set α
h : a ∈ P
x : α
hx : x ∈ a
⊢ a = {y | P.Rel x y}
Tactic:
rwa [setOf_rel_eq _ hx]
State after:
no goals