Structure Extensions

Stream: lean4

[François G. Dorais]

First, I think it's really cool that this works as I expect it to:

structure Bar (α) where bar : α

structure Foo {α} (x : α) : Prop where foo : True

structure FooBar (α) extends Bar α, Foo bar

#print FooBar
/-
inductive FooBar.{u_1} : Sort u_1 → Sort (max 1 u_1)
constructors:
FooBar.mk : {α : Sort u_1} → (_toBar : Bar α) → Foo _toBar.bar → FooBar α
-/

However, I don't understand how to make this work:

protected theorem FooBar.eq {α} : ∀ (f g : FooBar α), f.bar = g.bar → f = g
| ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
/-
dependent elimination failed, stuck at auxiliary equation
  { toBar := _toBar✝, toFoo := _toFoo✝ }.toBar.1 = { toBar := _toBar✝¹, toFoo := _toFoo✝¹ }.toBar.1
-/

Is there a reason why this shouldn't work?

PS: I kind of wish this shorthand worked too but this one seems like more of a rabbit hole.

structure Foo {α} (x : α) : Prop where foo : True

structure FooBar (α) extends Foo bar where bar : α

[Mario Carneiro]

protected theorem FooBar.eq {α} : ∀ (f g : FooBar α), f.bar = g.bar → f = g
| ⟨⟨_⟩,_⟩, ⟨⟨_⟩,_⟩, rfl => rfl

works

[François G. Dorais]

Of course! I see the .1 was the hint in the error message... subtle! Thanks!