-- Mathlib/Algebra/Order/Ring/Cast.lean
lemma nneg_mul_add_sq_of_abs_le_one (n : ℤ) (hx : |x| ≤ 1) : (0 : R) ≤ n * x + n * n

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n * x + ↑n * ↑n

Tactic:
rw [← mul_add, mul_nonneg_iff]

Result:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
this : x + ↑n ≤ 1 + -1
⊢ x + ↑n ≤ 0

Tactic:
rwa [add_neg_cancel] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
⊢ 0 ≤ ↑n * x + ↑n * ↑n

Tactic:
have hnx' : n < 0 → x + n ≤ 0 := fun hn => by
  have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
  rwa [add_neg_cancel] at this

Result:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n * x + ↑n * ↑n

Proof state:
case inr.inl
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
hx : |x| ≤ 1
hnx : 0 < 0 → 0 ≤ x + ↑0
hnx' : 0 < 0 → x + ↑0 ≤ 0
⊢ 0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0

Tactic:
simp [le_total 0 x]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
⊢ x + ↑n ≤ 0

Tactic:
have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)

Result:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
this : x + ↑n ≤ 1 + -1
⊢ x + ↑n ≤ 0

Proof state:
case inr.inr
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Tactic:
exact Or.inl ⟨mod_cast h.le, hnx h⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
this : -1 + 1 ≤ x + ↑n
⊢ 0 ≤ x + ↑n

Tactic:
rwa [neg_add_cancel] at this

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Tactic:
exact Or.inr ⟨mod_cast h.le, hnx' h⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Tactic:
rcases lt_trichotomy n 0 with (h | rfl | h)

Result:
case inl
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

case inr.inl
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
hx : |x| ≤ 1
hnx : 0 < 0 → 0 ≤ x + ↑0
hnx' : 0 < 0 → x + ↑0 ≤ 0
⊢ 0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0

case inr.inr
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
⊢ 0 ≤ ↑n * x + ↑n * ↑n

Tactic:
have hnx : 0 < n → 0 ≤ x + n := fun hn => by
  have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
  rwa [neg_add_cancel] at this

Result:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
⊢ 0 ≤ ↑n * x + ↑n * ↑n

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
⊢ 0 ≤ x + ↑n

Tactic:
have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)

Result:
R : Type u_1
inst✝ : LinearOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
this : -1 + 1 ≤ x + ↑n
⊢ 0 ≤ x + ↑n