case refine'_1

⊢ ↑⊥.cells ⊆ ∅

case refine'_2

⊢ ∅ ⊆ ↑⊥.cells
⊢ ↑⊥.cells = ∅
refine' Set.eq_of_subset_of_subset _ _
case refine'_1
x : ℕ × ℕ
h : x ∈ ↑⊥.cells
⊢ x ∈ ∅

case refine'_2

⊢ ∅ ⊆ ↑⊥.cells
case refine'_1

⊢ ↑⊥.cells ⊆ ∅

case refine'_2

⊢ ∅ ⊆ ↑⊥.cells
intros x h
case refine'_2

⊢ ∅ ⊆ ↑⊥.cells
case refine'_1
x : ℕ × ℕ
h : x ∈ ↑⊥.cells
⊢ x ∈ ∅

case refine'_2

⊢ ∅ ⊆ ↑⊥.cells
simp [mem_mk, Finset.coe_empty, Set.mem_empty_iff_false] at h
no goals
case refine'_2

⊢ ∅ ⊆ ↑⊥.cells
simp only [cells_bot, Finset.coe_empty, Set.empty_subset]