Theorem: Imo1998P2.norm_bound_of_odd_sum (Compfiles/Imo1998P2.lean)

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ 2 * z * z + 2 * z + 1 ≤ x * x + y * y
Tactic:
suffices 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y by
  rw [← mul_le_mul_left (zero_lt_two' ℤ)]; ring_nf at this ⊢; exact this
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
Tactic:
have h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1 := by rw [h]; ring
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
Tactic:
rw [← add_sq_add_sq_sub, h', add_le_add_iff_left]
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 1 ≤ (x - y) * (x - y)

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 1 ≤ (x - y) * (x - y)
Tactic:
suffices 0 < (x - y) * (x - y) by apply Int.add_one_le_of_lt this
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 0 < (x - y) * (x - y)

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 0 < (x - y) * (x - y)
Tactic:
rw [mul_self_pos, sub_ne_zero]
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ x ≠ y

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ x ≠ y
Tactic:
apply Int.ne_of_odd_add ⟨z, h⟩
State after:
no goals

State before:
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
Tactic:
rw [← mul_le_mul_left (zero_lt_two' ℤ)]
State after:
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)

State before:
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)
Tactic:
ring_nf at this ⊢
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2
⊢ 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2
⊢ 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2
Tactic:
exact this
State after:
no goals

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ (x + y) * (x + y) = 4 * z * z + 4 * z + 1
Tactic:
rw [h]
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ (2 * z + 1) * (2 * z + 1) = 4 * z * z + 4 * z + 1

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ (2 * z + 1) * (2 * z + 1) = 4 * z * z + 4 * z + 1
Tactic:
ring
State after:
no goals

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
this : 0 < (x - y) * (x - y)
⊢ 1 ≤ (x - y) * (x - y)
Tactic:
apply Int.add_one_le_of_lt this
State after:
no goals