a : ℕ
a1 : 1 < a
this : a * 1 ≤ a * a
⊢ a ≤ a * a
a : ℕ
a1 : 1 < a
⊢ a ≤ a * a
have := @Nat.mul_le_mul_left 1 a a (le_of_lt a1)
no goals
a : ℕ
a1 : 1 < a
this : a * 1 ≤ a * a
⊢ a ≤ a * a
rwa [mul_one] at this