struct equality

Stream: new members

[Evan Lohn]

I saw a topic about this in #general, but it didn't answer the more general question I have. How do I define equality for a new type of structure I want to use? i.e.

import data.equiv.basic
import data.finset.basic
import data.prod

structure foo (α β: ℕ):=
mk :: (edge : (fin α) → (fin β)) (h: α < β)

lemma foos_equal {a b : ℕ} {edge1 edge2 : (fin a) → (fin b)} {h1 h2: _} (h: edge1 = edge2): (foo.mk edge1 h1) = (foo.mk edge2 h2) :=
begin
  -- ext, -- (doesn't work?)
  sorry
end

I have a more complicated setting where I'd like to prove things that look like this; the general idea is to be able to define and use an equivalence that hinges on the data used to create the struct and not the proofs about that data. Any help would be greatly appreciated!

[Kevin Buzzard]

@[ext]
structure foo (α β: ℕ):=
mk :: (edge : (fin α) → (fin β)) (h: α < β)

lemma foos_equal {a b : ℕ} {edge1 edge2 : (fin a) → (fin b)} {h1 h2: _} (h: edge1 = edge2): (foo.mk edge1 h1) = (foo.mk edge2 h2) :=
begin
  ext, -- works!
  dsimp only,
  rw h,
end

[Eric Wieser]

subst h ought to work on your goal, no ext needed (because you have mk on both sides of the = so there's nothing that needs to be pulled apart)