Making auxiliary goals when `refine` fails by type mismatch

Stream: general

[nrs]

I'm trying to figure out a workflow to make finding terms for Fin2 easier by using tactics. Consider the following function:

def makeSuccNTimesFunc {n : Nat} : (m : Nat) -> Fin2 n.succ -> Fin2 (n.succ + m)
| .zero => id
| .succ mm => (Fin2.fs .) ∘ (makeSuccNTimesFunc mm)

Attempting to use refine with it in a proof causes a type mismatch:

example {n : Nat} : Fin2 n.succ := by
  refine @makeSuccNTimesFunc ?firstUnknown n ?finToSucc

The error is: has type Fin2 (Nat.succ ?firstUnknown + n) but Fin2 n.succ is expected. This particular case is easy to solve just by reading off the types, but it's a mwe for more difficult cases. I've rewritten the function in the following way for there to be a proof that will simplify the x : Nat in the goal Fin2 x:

def makeSuccNTimesFunc' {n : Nat} : (m x : Nat) -> n.succ + m = x -> Fin2 n.succ -> Fin2 x
| .zero, x, p => by rw [<- p]; exact id
| .succ mm, x, p => by rw [<- p]; exact @makeSuccNTimesFunc _ _

which allows me to help me prove the statement using refine like so:

example {n : Nat} : Fin2 n.succ := by
  refine @makeSuccNTimesFunc' ?whichn ?applyAmount n.succ ?eqproof ?fin
  case applyAmount => exact n
  case whichn => exact 0
  case eqproof => simp_arith
  case fin => exact .fz

We can then rewrite it in term mode now that we know what goes where and use our previous function makeSuccNTimesFunc instead of the new one.

My question is this: is there a way to produce auxiliary goals, which behave like the result of rewriting the function makeSuccNTimesFunc into makeSuccNTimesFunc', without needing to actually rewrite the function, when refine fails to produce auxiliary goals?

[nrs]

hm combining convert with named holes does seem like an intermediary solution (didn't know you could use ?var holes with convert). edit: hm but it's hard to control it this way and it will resolve holes that you want to keep open

[nrs]

in case it helps someone: I've turned the let/revert/refold/intro sequence in the following piece of code into a macro and found using it provided the same benefits as refactoring the function to allow the typechecker to help finding a desired value (it plays the role of ?eqproof above). This solution is inspired by comments at https://github.com/leanprover-community/mathlib4/pull/12745

example {n : Nat} : Fin2 n.succ := by
  have ha := @makeSuccNTimesFunc ?n ?applyAmount ?finToApplyTo
  let x := Nat.succ ?n + ?applyAmount
  revert ha
  refold_let x
  intro ha
  suffices x = n.succ by rwa [<-this]
  case finToApplyTo := .fz
  case applyAmount := n
  unfold x
  case n := 0
  simp_arith

edit: whoops I think this is effectively the same as using convert ... using 1