α : Type u_1
β : Type ?u.89259
γ : Type ?u.89262
δ : Type ?u.89265
inst✝ : LT α
a✝ b✝ : α
a b : WithTop α
⊢ (∃ a_1, ↑WithTop.toDual a = ↑(↑toDual a_1) ∧ ↑WithTop.toDual b < ↑(↑toDual a_1)) ↔ ∃ p, a = ↑p ∧ ↑p < b
α : Type u_1
β : Type ?u.89259
γ : Type ?u.89262
δ : Type ?u.89265
inst✝ : LT α
a✝ b✝ : α
a b : WithTop α
⊢ a < b ↔ ∃ p, a = ↑p ∧ ↑p < b
rw [← toDual_lt_toDual_iff, WithBot.lt_iff_exists_coe, OrderDual.exists]
no goals
α : Type u_1
β : Type ?u.89259
γ : Type ?u.89262
δ : Type ?u.89265
inst✝ : LT α
a✝ b✝ : α
a b : WithTop α
⊢ (∃ a_1, ↑WithTop.toDual a = ↑(↑toDual a_1) ∧ ↑WithTop.toDual b < ↑(↑toDual a_1)) ↔ ∃ p, a = ↑p ∧ ↑p < b
exact exists_congr fun _ => and_congr_left' Iff.rfl