α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
a : α
⊢ pred a ≤ ⨆ (b : α) (_ : b < a), b
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
a : α
⊢ pred a = ⨆ (b : α) (_ : b < a), b
refine' le_antisymm _ (iSup_le fun b => iSup_le le_pred_of_lt)
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
⊢ pred ⊥ ≤ ⨆ (b : α) (_ : b < ⊥), b

case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
a : α
ha : a ≠ ⊥
⊢ pred a ≤ ⨆ (b : α) (_ : b < a), b
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
a : α
⊢ pred a ≤ ⨆ (b : α) (_ : b < a), b
obtain rfl | ha := eq_or_ne a ⊥
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
⊢ ⊥ ≤ ⨆ (b : α) (_ : b < ⊥), b
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
⊢ pred ⊥ ≤ ⨆ (b : α) (_ : b < ⊥), b
rw [pred_bot]
no goals
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
⊢ ⊥ ≤ ⨆ (b : α) (_ : b < ⊥), b
exact bot_le
no goals
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : PredOrder α
a : α
ha : a ≠ ⊥
⊢ pred a ≤ ⨆ (b : α) (_ : b < a), b
exact @le_iSup₂ _ _ (fun b => b < a) _ (fun a _ => a) (pred a) (pred_lt_iff_ne_bot.2 ha)