F : Type ?u.108900
α : Type u_1
β : Type u_2
γ : Type ?u.108909
δ : Type ?u.108912
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ ↑(toOrderEmbedding f) x ⊓ ↑(toOrderEmbedding f) y ≤ ↑(toOrderEmbedding f) (x ⊓ y)
F : Type ?u.108900
α : Type u_1
β : Type u_2
γ : Type ?u.108909
δ : Type ?u.108912
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ ↑f (x ⊓ y) = ↑f x ⊓ ↑f y
refine' (f.toOrderEmbedding.map_inf_le x y).antisymm _
F : Type ?u.108900
α : Type u_1
β : Type u_2
γ : Type ?u.108909
δ : Type ?u.108912
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ ↑(symm f) (↑(toOrderEmbedding f) x ⊓ ↑(toOrderEmbedding f) y) ≤ ↑(symm f) (↑(toOrderEmbedding f) (x ⊓ y))
F : Type ?u.108900
α : Type u_1
β : Type u_2
γ : Type ?u.108909
δ : Type ?u.108912
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ ↑(toOrderEmbedding f) x ⊓ ↑(toOrderEmbedding f) y ≤ ↑(toOrderEmbedding f) (x ⊓ y)
apply f.symm.le_iff_le.1
no goals
F : Type ?u.108900
α : Type u_1
β : Type u_2
γ : Type ?u.108909
δ : Type ?u.108912
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ ↑(symm f) (↑(toOrderEmbedding f) x ⊓ ↑(toOrderEmbedding f) y) ≤ ↑(symm f) (↑(toOrderEmbedding f) (x ⊓ y))
simpa using f.symm.toOrderEmbedding.map_inf_le (f x) (f y)