Theorem: Partition.iSup_eq (Matroid/ForMathlib/SetPartition.lean)

State before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P : Partition s
⊢ ⨆ x ∈ P, x = s
Tactic:
simp_rw [← P.sSup_eq', sSup_eq_iSup]
State after:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P : Partition s
⊢ ⨆ x ∈ P, x = ⨆ a ∈ P.parts, a

State before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P : Partition s
⊢ ⨆ x ∈ P, x = ⨆ a ∈ P.parts, a
Tactic:
rfl
State after:
no goals