Theorem: Usa2018P1.am_gm (Compfiles/Usa2018P1.lean)

State before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 2 * (a * b) ^ (1 / 2) ≤ a + b
Tactic:
have hw : (0 : ℝ) ≤ 1/2 := by norm_num
State after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 2 * (a * b) ^ (1 / 2) ≤ a + b

State before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 2 * (a * b) ^ (1 / 2) ≤ a + b
Tactic:
rw [Real.mul_rpow ha hb]
State after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 2 * (a ^ (1 / 2) * b ^ (1 / 2)) ≤ a + b

State before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 2 * (a ^ (1 / 2) * b ^ (1 / 2)) ≤ a + b
Tactic:
have := Real.geom_mean_le_arith_mean2_weighted hw hw ha hb (by norm_num)
State after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
this : a ^ (1 / 2) * b ^ (1 / 2) ≤ 1 / 2 * a + 1 / 2 * b
⊢ 2 * (a ^ (1 / 2) * b ^ (1 / 2)) ≤ a + b

State before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
this : a ^ (1 / 2) * b ^ (1 / 2) ≤ 1 / 2 * a + 1 / 2 * b
⊢ 2 * (a ^ (1 / 2) * b ^ (1 / 2)) ≤ a + b
Tactic:
linarith
State after:
no goals

State before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hw : 0 ≤ 1 / 2
⊢ 1 / 2 + 1 / 2 = 1
Tactic:
norm_num
State after:
no goals