case mono_iff
α : Type u_1
β : Type u_2
γ : Type ?u.103518
δ : Type ?u.103521
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
a b : WithTop α
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ ∀ {a b : αᵒᵈ}, (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual) a ≤ (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual) b ↔ a ≤ b
α : Type u_1
β : Type u_2
γ : Type ?u.103518
δ : Type ?u.103521
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
a b : WithTop α
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f a ≤ map f b ↔ a ≤ b
erw [← toDual_le_toDual_iff, toDual_map, toDual_map, WithBot.map_le_iff, toDual_le_toDual_iff]
no goals
case mono_iff
α : Type u_1
β : Type u_2
γ : Type ?u.103518
δ : Type ?u.103521
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
a b : WithTop α
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ ∀ {a b : αᵒᵈ}, (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual) a ≤ (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual) b ↔ a ≤ b
simp [mono_iff]