x y : ℕ∞
⊢ ↑withTopEquiv (↑withTopEquiv.symm x) ≤ ↑withTopEquiv (↑withTopEquiv.symm y) ↔ x ≤ y
x y : ℕ∞
⊢ ↑withTopEquiv.symm x ≤ ↑withTopEquiv.symm y ↔ x ≤ y
rw [← withTopEquiv_le]
no goals
x y : ℕ∞
⊢ ↑withTopEquiv (↑withTopEquiv.symm x) ≤ ↑withTopEquiv (↑withTopEquiv.symm y) ↔ x ≤ y
simp