## Stream: new members

### Topic: equality for structures

#### Jake Levinson (Sep 07 2021 at 22:32):

Here is a lemma I am stuck on:

structure bundle (B : Type) :=
(space : Type)
(π : space → B)

structure bundle_map {B : Type} (E F : bundle B) :=
(map : E.space → F.space)
(h : F.π ∘ map = E.π)

lemma bundle_map.eq_of_map {B : Type} {E F : bundle B} (φ1 φ2 : bundle_map E F)
(h1 : φ1.map = φ2.map) : φ1 = φ2 :
begin
split
/- invalid apply tactic, failed to unify
φ1 = φ2
with
?m_2 = ?m_2 -/
end


I thought that split or cases or something should work here. For example I can prove associativity of compositions (which involves showing that two bundle_maps are equal) that way:

def bundle_map.comp {B : Type} {E F G : bundle B}
(φ' : bundle_map F G) (φ : bundle_map E F) : bundle_map E G :=
{ map := φ'.map ∘ φ.map,
h   := by rw [← function.comp.assoc, φ'.h, φ.h], }
infix ∘∘:110 := bundle_map.comp

lemma bundle_map.comp.assoc {B : Type} {E F G H : bundle B}
(φ'' : bundle_map G H) (φ' : bundle_map F G) (φ : bundle_map E F) :
(φ'' ∘∘ φ') ∘∘ φ = φ'' ∘∘ φ' ∘∘ φ := by split


Thanks for any help!

#### Kyle Miller (Sep 07 2021 at 22:35):

For this, you need an extensionality lemma. The @[ext] attribute is a way to generate one for you automatically:

@[ext]
structure bundle_map {B : Type} (E F : bundle B) :=
(map : E.space → F.space)
(h : F.π ∘ map = E.π)

lemma bundle_map.eq_of_map {B : Type} {E F : bundle B} (φ1 φ2 : bundle_map E F)
(h1 : φ1.map = φ2.map) : φ1 = φ2 :=
begin
ext x,  -- or ext1 to just do a single level; follow by exact h1

end


#### Kevin Buzzard (Sep 07 2021 at 22:35):

Cases works for me:

lemma bundle_map.eq_of_map {B : Type} {E F : bundle B} (φ1 φ2 : bundle_map E F)
(h1 : φ1.map = φ2.map) : φ1 = φ2 :=
begin
cases φ1 with map1 h1,
cases φ2 with map2 h2,
simp * at *,
end


#### Kevin Buzzard (Sep 07 2021 at 22:36):

(Kyle's answer is in some sense "the same as mine", because you prove ext lemmas for structures precisely by doing cases on the components)

Thank you both!

#### Kevin Buzzard (Sep 07 2021 at 22:37):

PS your by split proof is bogus:

lemma bundle_map.comp.assoc {B : Type} {E F G H : bundle B}
(φ'' : bundle_map G H) (φ' : bundle_map F G) (φ : bundle_map E F) :
(φ'' ∘∘ φ') ∘∘ φ = φ'' ∘∘ φ' ∘∘ φ := rfl


Oooh.

#### Kevin Buzzard (Sep 07 2021 at 22:39):

split never closes goals unless they are somehow degenerate, in my experience.

#### Kyle Miller (Sep 07 2021 at 22:42):

Also, split is for splitting a goal that's a constructor of some kind (something with parts) -- the goal is an equality, which can't be split.

Using Kevin's direct proof, you'd want congr, like cases φ1, cases φ2, congr, exact h1,

#### Kyle Miller (Sep 07 2021 at 22:46):

I should have been paying more attention... you're proving the extensionality lemma that @[ext] generates of course, so my suggestion is sort of absurd.

@[ext]
structure bundle_map {B : Type} (E F : bundle B) :=
(map : E.space → F.space)
(h : F.π ∘ map = E.π)

lemma bundle_map.eq_of_map {B : Type} {E F : bundle B} (φ1 φ2 : bundle_map E F)
(h1 : φ1.map = φ2.map) : φ1 = φ2 := bundle_map.ext _ _ h1


#### Jake Levinson (Sep 07 2021 at 23:14):

Thanks Kyle and Kevin! That's very helpful.

Last updated: Dec 20 2023 at 11:08 UTC