Solving a two-variable linear system
ProvedWorkbookSource.problem_7824lean-workbooksource-checked
Solve the system of equations: & .
Source: InternLM Lean-Workbook, record lean_workbook_7824 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_7824 (x y : ℝ) (h₁ : 2*x-3*y+1 = 1) (h₂ : 2*x+y-3 = 13) : x = 6 ∧ y = 4 := by sorry
Source