Proof for mathd_algebra_513

[aleph-prover-test]

Proven lemmas: 1/1

The goal is to prove that if a, b ∈ ℝ satisfy the linear system 3·a + 2·b = 5 and a + b = 2, then necessarily a = 1 and b = 1.
The proof is decomposed into two sub-goals because the conclusion is a conjunction: first prove a = 1, then prove b = 1, and finally combine them with “constructor” to get a = 1 ∧ b = 1.
Both sub-goals have been solved: Lean uses the linear arithmetic tactic linarith with the hypotheses h₀ and h₁ to derive each equality directly.
So progress is complete: 2 out of 2 sub-problems are finished, and the overall theorem is proved.
An interesting aspect is that this avoids manual elimination; alternatively, one could solve by substituting b = 2 − a from a + b = 2 into 3·a + 2·b = 5 to get a = 1, then back-substitute to get b = 1, but linarith automates this linear reasoning.