unfold through instance of Type Class

Stream: new members

[LB]

Sorry if I post in the wrong stream...

I try to unfold an instance of Add to be able to use an hypothesis in an if then else. When I unfold the immediate add, it works; but when I unfold the implicit add, it doesn't work. This is an MWE:

inductive FooNat where
  | bar : Nat → FooNat
  | bor : Nat → FooNat

namespace FooNat

def add (m n: FooNat) : FooNat :=
  match m , n with
  | bar _ , bar _ => bar 0
  | bar _ , bor _ => bar 1
  | bor _ , bar _ => bar 2
  | bor a , bor b => if a < b then bar 3 else bar 4

instance : Add FooNat where
  add := add

example (m n: Nat) : m < n → add (bor m) (bor n) = bar 3 := by
  intro h
  unfold add -- this works
  simp [h]

example (m n: Nat) : m < n → bor m + bor n = bar 3 := by
  intro h
  unfold add -- this doesn't work
  simp [h]

What should I do to reduce bor m + bor n using hypothesis h : m < n?

Toolchain is leanprover/lean4:stable (Lean 4.4.0).

[Eric Wieser]

You need to unfold HAdd.hAdd and Add.add too

[LB]

@Eric Wieser Thank you for your answer.

unfold HAdd.hAdd does something and morphs my goal to instHAdd.1 (bor m) (bor n) = bar 3

Chaining this with unfold Add.add does nothing more: tactic 'unfold' failed to unfold 'Add.add' at instHAdd.1 (bor m) (bor n) = bar 3

[Newell Jensen]

you can replace the line with your comment like this:

simp [Add.add, HAdd.hAdd, add] -- this doesn't work --> now it does

[LB]

@Newell Jensen Thank you. That worked!

[Ruben Van de Velde]

You can make life easier for yourself by adding a lemma a+b = add a b with proof rfl