How to prove `LawfulBEq` for automatically generated `BEq`

Stream: lean4

[Geoffrey Irving]

I am not sure how to complete this proof:

import Mathlib.Data.UInt

/-- 64-bit two's complement integers -/
structure Int64 where
  n : UInt64
  deriving BEq

/-- `Int64` has nice equality -/
instance : LawfulBEq Int64 where
  eq_of_beq {x y} e := by
    induction' x with x; induction' y with y
    simp [BEq.beq, decide_eq_true_eq] at e
    sorry
  rfl {x} := sorry

After the simp, the environment looks like

x✝y✝: Int64
e✝²: (x✝ == y✝) = true
x: UInt64
e✝¹: ({ n := x } == y✝) = true
y: UInt64
e✝: (x✝ == { n := y }) = true
e: beqInt64✝ { n := x } { n := y } = true
⊢ { n := x } = { n := y }

If I could expand that beqInt64✝ function, I think I would get x = y. But I don't know how to name that instance, and thus I don't know how to expand it.

[Eric Rodriguez]

rw [eq_of_beq e] closes the goal; I guess that function is the beq on UInt64, but not sure why it pops up in such a way.

import Mathlib.Data.UInt

/-- 64-bit two's complement integers -/
structure Int64 where
  n : UInt64
  deriving BEq

/-- `Int64` has nice equality -/
instance : LawfulBEq Int64 where
  eq_of_beq {x y} e := by
    induction' x with x; induction' y with y
    simp [BEq.beq, decide_eq_true_eq] at e
    rw [eq_of_beq e]
  rfl {x} := beq_self_eq_true' x.n

(the rfl proof was found by exact?)

[Geoffrey Irving]

Thank you! (I already had the rfl proof; I just left it out for minimality purposes.)

Would it be reasonable for deriving BEq to always make a LawfulBEq instance, or to have deriving LawfulBEq work?