case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b

case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b
by_cases ha : IsMin a
no goals
case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b
rw [ha.pred_eq, or_iff_right_of_imp ge_of_eq]
no goals
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b
rw [← pred_lt_iff_of_not_isMin ha, le_iff_eq_or_lt, eq_comm]