The intersection of two lines
ProvedWorkbookSource.problem_8402lean-workbooksource-checked
What is the coordinate of the intersection of and ?
Source: InternLM Lean-Workbook, record lean_workbook_8402 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_8402 (x y : ℝ) : (y = 2*x - 3 ∧ y = -7*x - 12) ↔ x = -1 ∧ y = -5 := by sorry
Source