eta expansion in dependent elimination

Stream: lean4

[Matthew Ballard]

This is a bit of a throw-away but for something like

abbrev Foo := ℕ

def SubFoo : Type := { f : Foo // f = 0 }

inductive Bar : ∀ (_ : Foo), Type
  | A (f : SubFoo) : Bar f.val

example : (f : Foo) → Bar f → Bar f → True
  | _, Bar.A f, Bar.A _ => trivial
/- dependent elimination failed, failed to solve equation
  f✝¹.1 = f✝.1
at case Bar.A after processing
  _, (Bar.A _), _ -/

would doing some eta expansion and continuing reasonable? Feel free to tell me this is a bad pattern and there is something else I should be doing.

[Mario Carneiro]

I think you can pattern match on f as well there to make it work

[Kyle Miller]

Yeah, that works:

example : (f : Foo) → Bar f → Bar f → True
  | _, Bar.A ⟨f, _⟩, Bar.A _ => trivial

[Matthew Ballard]

Thanks. That helps.