α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ sup P.parts id = ⊥
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥
simp_rw [← P.supParts]
case refine'_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ sup P.parts id = ⊥

case refine'_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : sup P.parts id = ⊥
b : α
hb : b ∈ P.parts
⊢ ⊥ ∈ P.parts
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ sup P.parts id = ⊥
refine' ⟨fun h ↦ _, fun h ↦ eq_empty_iff_forall_not_mem.2 fun b hb ↦ P.not_bot_mem _⟩
case refine'_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ sup ∅ id = ⊥
case refine'_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ sup P.parts id = ⊥
rw [h]
no goals
case refine'_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ sup ∅ id = ⊥
exact Finset.sup_empty
no goals
case refine'_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : sup P.parts id = ⊥
b : α
hb : b ∈ P.parts
⊢ ⊥ ∈ P.parts
rwa [← le_bot_iff.1 ((le_sup hb).trans h.le)]