Proof for mathd_algebra_513

[aleph-prover-test]

Proven lemmas: 1/1

The goal is to prove that for real numbers a, b ∈ ℝ, if 3a + 2b = 5 and a + b = 2, then necessarily a = 1 and b = 1. The proof is decomposed into two subgoals because the conclusion is a conjunction: first show a = 1, and then show b = 1. Both subgoals are handled simultaneously by a single strategy: after using constructor to split the ∧ goal, Lean’s linarith tactic solves each equality directly from the two given linear equations h₀ and h₁. At this point, the full proof is complete: 2 out of 2 subgoals are solved, with no remaining obligations. An alternative (also described) would be to solve the system manually by rewriting b = 2 − a from h₁, substituting into h₀ to get a = 1, and then back-substituting to get b = 1, but linarith neatly automates this linear-algebra step. The main “interesting strategy” here is leveraging linarith to solve a 2×2 linear system without explicit substitution or rearrangement.