α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ (⨅ (b : α) (_ : a < b), b) ≤ succ a
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ succ a = ⨅ (b : α) (_ : a < b), b
refine' le_antisymm (le_iInf fun b => le_iInf succ_le_of_lt) _
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ (⨅ (b : α) (_ : ⊤ < b), b) ≤ succ ⊤

case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ (⨅ (b : α) (_ : a < b), b) ≤ succ a
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ (⨅ (b : α) (_ : a < b), b) ≤ succ a
obtain rfl | ha := eq_or_ne a ⊤
no goals
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ (⨅ (b : α) (_ : a < b), b) ≤ succ a
exact iInf₂_le _ (lt_succ_iff_ne_top.2 ha)
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ (⨅ (b : α) (_ : ⊤ < b), b) ≤ ⊤
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ (⨅ (b : α) (_ : ⊤ < b), b) ≤ succ ⊤
rw [succ_top]
no goals
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ (⨅ (b : α) (_ : ⊤ < b), b) ≤ ⊤
exact le_top