simp and bundled structure

Stream: lean4

[pcpthm]

I have a bundled type like an add-homomorphism type.
I noticed simp discrimination tree is not efficiently used. This is because a field of a structure is reducible, the normal form of Struct.field ?meta is a metavariable and it matches any such form.
I could add semireducible attribute to the field, and now simp lemmas are efficiently discriminated, but then it seems like there is no way to reduce a field projection during a proof (simp doesn't work).
Is there any better way?

structure Hom where
  hom : Nat → Nat
  hom_add : hom (a + b) = hom a + hom b
attribute [simp] Hom.hom_add

set_option trace.Meta.Tactic true in
example (f : Hom) : f.hom 1 = f.hom 1 := by
  simp -- Hom.hom_add:1000, failed to unify Hom.hom ?self (?a + ?b) with Hom.hom

attribute [semireducible] Hom.hom

def Hom.refl : Hom := ⟨fun a => a, by rfl⟩

example : Hom.refl.hom a = a := by
  simp only [Hom.hom]
  traceState -- Hom.hom is not unfolded
  rfl