α : Type u_1
β : Type ?u.76189
γ : Type ?u.76192
δ : Type ?u.76195
a b : α
inst✝ : LE α
h : IsMin a
b✝ : WithTop α
hb : b✝ ≤ ↑a
⊢ ↑a ≤ b✝
α : Type u_1
β : Type ?u.76189
γ : Type ?u.76192
δ : Type ?u.76195
a b : α
inst✝ : LE α
h : IsMin a
⊢ IsMin ↑a
intro _ hb
α : Type u_1
β : Type ?u.76189
γ : Type ?u.76192
δ : Type ?u.76195
a b : α
inst✝ : LE α
h : IsMin a
b✝ : WithTop α
hb : ↑WithTop.toDual ↑a ≤ ↑WithTop.toDual b✝
⊢ ↑a ≤ b✝
α : Type u_1
β : Type ?u.76189
γ : Type ?u.76192
δ : Type ?u.76195
a b : α
inst✝ : LE α
h : IsMin a
b✝ : WithTop α
hb : b✝ ≤ ↑a
⊢ ↑a ≤ b✝
rw [← toDual_le_toDual_iff] at hb
no goals
α : Type u_1
β : Type ?u.76189
γ : Type ?u.76192
δ : Type ?u.76195
a b : α
inst✝ : LE α
h : IsMin a
b✝ : WithTop α
hb : ↑WithTop.toDual ↑a ≤ ↑WithTop.toDual b✝
⊢ ↑a ≤ b✝
simpa [toDual_le_iff] using (IsMax.withBot h : IsMax (toDual a : WithBot αᵒᵈ)) hb