simpa using hP x
case mk.mk.h
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition s
parts✝¹ : Set α
setIndependent✝¹ : CompleteLattice.SetIndependent parts✝¹
bot_not_mem✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
setIndependent✝ : CompleteLattice.SetIndependent parts✝
bot_not_mem✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
hP :
  ∀ (x : α),
    x ∈ { parts := parts✝¹, setIndependent := setIndependent✝¹, bot_not_mem := bot_not_mem✝¹, sSup_eq' := sSup_eq'✝¹ } ↔
      x ∈ { parts := parts✝, setIndependent := setIndependent✝, bot_not_mem := bot_not_mem✝, sSup_eq' := sSup_eq'✝ }
x : α
⊢ x ∈ parts✝¹ ↔ x ∈ parts✝
no goals