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 show a = 1, then show b = 1, and finally combine them into a = 1 ∧ b = 1.
Both sub-goals are solved: Lean uses the tactic linarith with the two given equations to derive a = 1, and then linarith again to derive b = 1.
So progress is complete: 2 out of 2 sub-problems have been proved, and nothing remains.
An interesting aspect is that this avoids manual algebra (substitution/elimination) by letting linarith automatically solve the linear constraints; an alternative strategy would be to rewrite b = 2 − a from a + b = 2, substitute into 3·a + 2·b = 5, and then solve, but linarith handles all of this directly.