## Stream: general

### Topic: simp of structures equality

#### kana (Jun 24 2021 at 21:37):

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 (Jun 24 2021 at 21:41):

Looks like you should prove an ext lemma.

#### Yakov Pechersky (Jun 24 2021 at 21:41):

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 (Jun 24 2021 at 21:42):

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 (Jun 24 2021 at 22:57):

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


Last updated: Aug 03 2023 at 10:10 UTC