proof refiner

Stream: Is there code for X?

[Vasily Ilin]

Is there a command to "refine" a proof? E.g. I have

import tactic -- imports all the Lean tactics
import linear_algebra.basis
import data.real.basic

example : ∃ t a b c : ℝ, a • ((3,1,4) : ℝ × ℝ × ℝ) + b • (2,-3,5) + c • (5,9,t) = (0,0,0) ∧ (a,b,c) ≠ (0,0,0) :=
begin
  use 2,
  use 3,
  use -2,
  use -1,
  split,
    {simp, split, ring, split, ring, ring,},
    {simp,},
end

and I want to make it shorter. Can I call a command to do so? If not, can you just tell me how to make it shorter? Surely I should be able to fit all four uses in one command

[Violeta Hernández]

I think you're looking for refine

[Violeta Hernández]

Try refine ⟨2, 3, -2, -1, _⟩

[Violeta Hernández]

You can also use the use tactic for this though, use [2, 3, -2, -1]

[Violeta Hernández]

Up to you

[Vasily Ilin]

Nice, thanks!

[Kyle Miller]

It's tactic#zulip :wink: