Theorem: Partition.rel_ofRel_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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
⊢ (ofRel r).Rel = r
Tactic:
ext a b
State after:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (ofRel r).Rel a b ↔ r a b

State before:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (ofRel r).Rel a b ↔ r a b
Tactic:
simp only [Rel, mem_ofRel_iff]
State after:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) ↔ r a b

State before:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) ↔ r a b
Tactic:
refine ⟨?_, fun h ↦ ⟨_, ⟨a, refl_of_rel r h, rfl⟩, refl_of_rel r h, h⟩⟩
State after:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) → r a b

State before:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) → r a b
Tactic:
rintro ⟨_, ⟨x, -, rfl⟩, ha, hb⟩
State after:
case h.h.a.intro.intro.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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b x : α
ha : a ∈ {y | r x y}
hb : b ∈ {y | r x y}
⊢ r a b

State before:
case h.h.a.intro.intro.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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b x : α
ha : a ∈ {y | r x y}
hb : b ∈ {y | r x y}
⊢ r a b
Tactic:
exact trans_of r (symm_of r ha) hb
State after:
no goals