solve_by_elim question

Stream: metaprogramming / tactics

[Patrick Massot]

This is probably a question for @Scott Morrison but everybody is welcome to answer. Consider the following code

import Mathlib.Tactic

example (n : Nat) (h : ∃ k, n = 2*k) : True := by
  -- have : ∃ k, n = 2*k := by solve_by_elim only [(by assumption : ∃ k, n = 2*k)] --fails
  have := (by assumption : ∃ k, n = 2*k)
  have : ∃ k, n = 2*k := by solve_by_elim only [this]
  trivial

I would expect the first line to succeed given the success of the next two lines. But it fails. I guess this is due to things solve_by_elim needs to do to handle backtracking without unintended metavar instantiation. But is there a way around this?

[Patrick Massot]

The context is that for a teaching tactic I want a version of solve_by_elim where you give additional facts that should be proven by a tactic instead of directly giving additional proofs.

[Patrick Massot]

Of course the fact the tactic I'm using is assumption is only for the #mwe.

[Patrick Massot]

I am aware that I could have a loop creating the relevant have, but I'd like to know whether there is a simpler way.