Applying constructors/theorems with equal arguments

Stream: Is there code for X?

[Elias Castegren]

I come from Rocq where the TLC library has a very useful tactic called applys_eq. It works like apply but first replaces arguments of propositions with placeholder variables which it unifies with the expected arguments, introducing sub-goals asserting the equality of the actual arguments and the expected ones. This lets you apply constructors or theorems first and handle rewriting later, which is usually easier if you have several expressions. (applys_eq also solves trivial equalities automatically)

Here is the feature I would like to have in Lean:

inductive is_double : Nat → Nat → Prop
| times_two : (n : Nat) → is_double n (n * 2)

theorem is_double_add : (n : Nat) →
  is_double n (n + n) :=
  by
  intro n
  apply_eq is_double.times_two /- wishful thinking at the moment -/
  · show n + n = n * 2
    omega

I can do this manually for any constructor or theorem I am interested in, but what's nice about applys_eq is that I don't have to:

/- I don't want to have to do this -/
theorem is_double_eq : (n m : Nat) →
  m = n * 2 →
  is_double n m :=
  by
  intro n m h
  rw [h]
  constructor

[Ruben Van de Velde]

Like this?

import Mathlib.Tactic
inductive is_double : Nat → Nat → Prop
| times_two : (n : Nat) → is_double n (n * 2)

theorem is_double_add : (n : Nat) →
  is_double n (n + n) :=
  by
  intro n
  convert is_double.times_two n using 1
  · show n + n = n * 2
    omega

[Elias Castegren]

That seems like exactly what I want! Thanks!