Beta reduction in proofs

Stream: lean4

[Siddhartha Gadgil]

I am new to lean which is probably why I am struggling with the following problem. I have a definition and I want to prove something that is a direct consequence of beta-reduction after substituting the definition. But the elaborator fails. Can someone help me with what I should be trying (some tactic?)

def restrict{α : Type}(n : Nat) : (Fin (Nat.succ n) → α) → Fin n →  α :=
  fun fn =>
    fun arg =>
      fn (plusOne n arg)

def lem1{α : Type}(zeroVal : α)(j: Fin 7)(g: (Fin (8)) → α)
        : (restrict 7 g j) = g (plusOne 7 j) :=
        _

The response I get is

don't know how to synthesize placeholder
context:
α : Type
zeroVal : α
j : Fin 7
g : Fin 8 → α
⊢ restrict 7 g j = g (plusOne 7 j)

Thanks.

[David Renshaw]

Does rfl work?

[Siddhartha Gadgil]

Thanks a lot. Yes it worked here. Will try where I really wanted it.

[Siddhartha Gadgil]

Worked where I needed it too. Need some more but I have to work on that. Thanks again.