linear_combination

Stream: new members

[Vasily Ilin]

The examples for https://leanprover-community.github.io/mathlib_docs/tactic/linear_combination.html#tactic.interactive.linear_combination do not work on my machine. For example, I get

failed to synthesize type class instance for
x y : ℤ,
h1 : x * y + 2 * x = 1,
h2 : x = y
⊢ has_one
    (opt_param linear_combo.linear_combination_config
       {normalize := tt,
        normalization_tactic := has_bind.seq (tactic.save_info {line := 75, column := 41})
                                  (tactic.interactive.ring1 none).step})

from

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) :
  x*y = -2*y + 1 :=
by linear_combination 1*h1 - 2*h2

[Kevin Buzzard]

Did you try updating your mathlib? It moves fast.

[Vasily Ilin]

I have not! I'll try that