[litexlang]

Thank you thau! Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. We are comparing Lean and Litex under conditions where they don’t rely too much on external packages, which makes the comparison a bit fairer. (since Lean does have a very rich set of libraries, but building libraries is itself a challenge. Litex really needs to learn from Lean on how to build a successful library!).)(afterall, Litex can also abstract all proofs here and give it a name linear_combination, right?)

[thaumasiotes]

> 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.