case mp
α : Type u_1
β : Type ?u.22369
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ

case mpr
α : Type u_1
β : Type ?u.22369
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α
α : Type u_1
β : Type ?u.22369
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ
constructor <;> intro i <;> haveI := i
no goals
case mp
α : Type u_1
β : Type ?u.22369
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ
exact
  { exists_pair_ne := @exists_pair_ne α _
    eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }
no goals
case mpr
α : Type u_1
β : Type ?u.22369
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α
exact
  { exists_pair_ne := @exists_pair_ne αᵒᵈ _
    eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }