[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
h : Monotone f
x✝¹ : α
x✝ : x✝¹ ∈ Icc a b
⊢ f x✝¹ ∈ Icc (f a) (f b)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
h : StrictMono f
x✝¹ : α
x✝ : x✝¹ ∈ Ioo a b
⊢ f x✝¹ ∈ Ioo (f a) (f b)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : Monotone f
x✝¹ : α
x✝ : x✝¹ ∈ Ici a
⊢ f x✝¹ ∈ Ici (f a)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : Monotone f
x✝¹ : α
x✝ : x✝¹ ∈ Iic a
⊢ f x✝¹ ∈ Iic (f a)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : StrictMono f
x✝¹ : α
x✝ : x✝¹ ∈ Ioi a
⊢ f x✝¹ ∈ Ioi (f a)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : StrictMono f
x✝¹ : α
x✝ : x✝¹ ∈ Iio a
⊢ f x✝¹ ∈ Iio (f a)
[PROOFSTEP]
aesop
