Lean4: calculate simple equation

Question

I am just starting to learn Lean4. I have a simple equation a = b - c + d and I try to calculate the missing variable by giving any other three of the variables.

My code looks like this:

import Mathlib.Data.Real.Basic

structure equation :=
  (a b c d : ℤ)
  (rule : a = b - c + d)

def example1 : equation :=
{
  a := 2
  --b := 4
  c := 3
  d := 1
  rule := rfl
}

#eval example1.b

And it does not work. It can calculate only the a variable when commenting it out. And also it can "check" the equation when all the variables are given.

I assume that my code can be totally wrong and the solution requires another approach. Maybe the "rfl" is a wrong choice.