Make rel justify a substitution defined by many constraints

Stream: new members

[Michael Bucko]

I wrote a proof from The Mechanics.. (calc + add_le_add_left-add_le_add_right or linarith), but I hoped I can solve it using rel or something similar, given H : a ≤ 1 ∧ a + b ≤ 3 and LHS = a + (a + b). Rel, however, was not able to justify a substitution.

Proof with calc + add_le_add_left-add_le_add_right

import Mathlib
import Lean

example {a b : ℚ} (H : a ≤ 1 ∧ a + b ≤ 3) : 2 * a + b ≤ 4 := by
  calc
    2 * a + b = a + (a + b) := by ring
    _ ≤ a + 3 := add_le_add_left H.2 a
    _ ≤ 1 + 3 := add_le_add_right H.1 3
    _ ≤ 4 := by norm_num

Proof with linarith

import Mathlib
import Lean

example {a b : ℚ} (H : a ≤ 1 ∧ a + b ≤ 3) : 2 * a + b ≤ 4 := by
  linarith

[Michael Bucko]

I guess I have to look at the actual code of linarith/ nlinarith. They are solving a bunch of other proofs from The Mechanics .

More proofs

import Mathlib
import Lean

example {a b : ℚ} (H : a ≤ 1 ∧ a + b ≤ 3) : 2 * a + b ≤ 4 := by
  linarith

example {r s : ℝ} (H : r + s ≤ 1 ∧ r - s ≤ 5) : 2 * r ≤ 6 := by
  linarith

example {m n : ℤ} (H : n ≤ 8 ∧ m + 5 ≤ n) : m ≤ 3 := by
  linarith

example {p : ℤ} (hp : p + 2 ≥ 9) : p ^ 2 ≥ 49 ∧ 7 ≤ p := by
  constructor
  . nlinarith
  . linarith

example {a : ℚ} (h : a - 1 ≥ 5) : a ≥ 6 ∧ 3 * a ≥ 10 := by
  constructor
  . linarith
  . linarith

example {x y : ℚ} (h : x + y = 5 ∧ x + 2 * y = 7) : x = 3 ∧ y = 2 := by
  constructor
  . linarith
  . linarith

, and so on.