Theorem: ltTwoMulSqrtTwoMul (FromTheBook/Ch02/Bertrand/Bertrand.lean)

State before:
n : ℝ
h : 81 / 2 < n
⊢ 18 < 2 * Real.sqrt (2 * n)
Tactic:
rw [← div_lt_iff' (by norm_num)]
State after:
n : ℝ
h : 81 / 2 < n
⊢ 18 / 2 < Real.sqrt (2 * n)

State before:
n : ℝ
h : 81 / 2 < n
⊢ 18 / 2 < Real.sqrt (2 * n)
Tactic:
rw [Real.lt_sqrt (by norm_num)]
State after:
n : ℝ
h : 81 / 2 < n
⊢ (18 / 2) ^ 2 < 2 * n

State before:
n : ℝ
h : 81 / 2 < n
⊢ (18 / 2) ^ 2 < 2 * n
Tactic:
norm_num
State after:
n : ℝ
h : 81 / 2 < n
⊢ 81 < 2 * n

State before:
n : ℝ
h : 81 / 2 < n
⊢ 81 < 2 * n
Tactic:
rw [← div_lt_iff' (by norm_num)]
State after:
n : ℝ
h : 81 / 2 < n
⊢ 81 / 2 < n

State before:
n : ℝ
h : 81 / 2 < n
⊢ 81 / 2 < n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
h : 81 / 2 < n
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
h : 81 / 2 < n
⊢ 0 ≤ 18 / 2
Tactic:
norm_num
State after:
no goals