Theorem: Partition.eq_of_rel_iff_rel (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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ P = P'
Tactic:
rw [← ofRel_rel_eq P, ← ofRel_rel_eq P']
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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ ofRel' P.Rel ⋯ = ofRel' P'.Rel ⋯

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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ ofRel' P.Rel ⋯ = ofRel' P'.Rel ⋯
Tactic:
congr
State after:
case e_r
α : 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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ P.Rel = P'.Rel

State before:
case e_r
α : 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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ P.Rel = P'.Rel
Tactic:
ext
State after:
case e_r.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 α
P P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
x✝¹ x✝ : α
⊢ P.Rel x✝¹ x✝ ↔ P'.Rel x✝¹ x✝

State before:
case e_r.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 α
P P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
x✝¹ x✝ : α
⊢ P.Rel x✝¹ x✝ ↔ P'.Rel x✝¹ x✝
Tactic:
exact h _ _
State after:
no goals