simp of structures equality

Stream: general

[kana]

I have such goal

{hom := λ (y : Cᵒᵖ), category.comp 𝟭, nat := _} = {hom := λ (_x : Cᵒᵖ), id, nat := _}

where nat : Prop.

Both homs have the same type.

λ (y : Cᵒᵖ), category.comp 𝟭 : Π (y : Cᵒᵖ), (y.unop ⟶ x) → (y.unop ⟶ x)

λ (_x : Cᵒᵖ), id             : Π (_x : Cᵒᵖ), (_x.unop ⟶ x) → (_x.unop ⟶ x)

But simp does not simplify goal to just

λ (y : Cᵒᵖ), category.comp 𝟭 = λ (_x : Cᵒᵖ), id

Is it a bug, or I missed something?

Not minimal example line 191

[Adam Topaz]

Looks like you should prove an ext lemma.

[Yakov Pechersky]

You're dealing with equality of structures. You have to use ext, the extensionality tactic, which splats out the structure, and asks you to prove that all the fields of the two structures match.

[Adam Topaz]

I assume these are natural transformations. If you put a @[ext] over your structure natural_transformation ... then lean will make the extensionality lemma for you automatically. Then use the ext tactic in the proof

[kana]

Thanks. It works.

But with that structure just simp works, what is the difference?

structure qwe :=
(a : nat) (b : a = a)

example : ({ a := 1, b := rfl } : qwe) = { a := 2, b := rfl } :=
begin
  simp,
end