Theorem: sqrtTwoMulLeSelf (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
n : ℕ
hn : 2 ≤ n
⊢ Nat.sqrt (2 * n) ≤ n
Tactic:
conv => rhs; rw [← Nat.sqrt_eq n]
State after:
n : ℕ
hn : 2 ≤ n
⊢ Nat.sqrt (2 * n) ≤ Nat.sqrt (n * n)

State before:
n : ℕ
hn : 2 ≤ n
⊢ Nat.sqrt (2 * n) ≤ Nat.sqrt (n * n)
Tactic:
apply Nat.sqrt_le_sqrt
State after:
case h
n : ℕ
hn : 2 ≤ n
⊢ 2 * n ≤ n * n

State before:
case h
n : ℕ
hn : 2 ≤ n
⊢ 2 * n ≤ n * n
Tactic:
exact Nat.mul_le_mul_right _ hn
State after:
no goals