> Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer.
I learned about the `linear_combination` tactic from your example. Other than that, I use `have` and `exact`, which (a) are not advanced, and (b) are also used in your example.
Before that, my first attempt at the lean proof looked like this:
example (x y : ℝ)
(h₁ : 2 * x + 3 * y = 10)
(h₂ : 4 * x + 5 * y = 14)
: x = -4 ∧ y = 6 := by
-- double h₁ to cancel the x term
have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁]
conv at h₃ => ring_nf -- "ring normal form"
-- subtract h₂ from h₃
have h₄ : (x * 4 + y * 6) - (4 * x + 5 * y) = 20 - 14 := by rw [h₂, h₃]
conv at h₄ => ring_nf
conv at h₁ =>
-- substitute y = 6 into h₁
rw [h₄]
ring_nf
-- solve for x
have h₅ : ((18 + x * 2) - 18) / 2 = (10 - 18) / 2 := by rw [h₁]
conv at h₅ => ring_nf
apply And.intro h₅ h₄
> We are comparing Lean and Litex under conditions where they don’t rely too much on external packages
This proof does have the advantage of not needing to import Mathlib.Tactic. Although again, that's something your proof does.
