-- Mathlib/NumberTheory/FLT/Polynomial.lean
private lemma ineq_pqr_contradiction {p q r a b c : ℕ}
    (hp : 0 < p) (hq : 0 < q) (hr : 0 < r)
    (hineq : q * r + r * p + p * q ≤ p * q * r)
    (hpa : p * a < a + b + c)
    (hqb : q * b < a + b + c)
    (hrc : r * c < a + b + c) : False

Proof state:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ (q * r + r * p + p * q) * (a + b + c) ≤ p * q * r * (a + b + c)

Tactic:
gcongr

Result:
no goals

Proof state:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) <
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)

Tactic:
gcongr

Result:
no goals

Proof state:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ False

Tactic:
suffices h : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c) by simp at h

Result:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)

Proof state:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1 ≤
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)

Tactic:
rw [Nat.succ_le]

Result:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) <
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)

Proof state:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) = (q * r + r * p + p * q) * (a + b + c)

Tactic:
ring

Result:
no goals

Proof state:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * q * r * (a + b + c) + 1 = p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1

Tactic:
ring

Result:
no goals

Proof state:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
h : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
p q r a b c : ℕ
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)

Tactic:
calc
  _ = (p * a) * (q * r) + (q * b) * (r * p) + (r * c) * (p * q) + 1 := by ring
  _ ≤ (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) := by
    rw [Nat.succ_le]
    gcongr
  _ = (q * r + r * p + p * q) * (a + b + c) := by ring
  _ ≤ _ := by gcongr

Result:
no goals