rw [← mul_le_mul_left (zero_lt_two' ℤ)]
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
⊢ 2 * z * z + 2 * z + 1 ≤ x * x + y * y
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
⊢ 2 * (2 * z * z + 2 * z + 1) ≤ 2 * (x * x + y * y)