Disjoint Union of Graphs, or type overrides

Stream: Is there code for X?

[Sigma]

Hello, I'm not sure if this belongs here or in new-members, but I am trying to define the disjoint union for a family of graphs; where we just want a b : Σ m, β m to be adjacent when they are in the same graph and adjacent in it so adj _ a.snd b.snd -> adj _ a b but this doesn't typecheck since a.snd and b.snd have type β a.fst and β b.fst. The only case we care about is when theyre in the same graph a.fst = b.fst anyway, so adding that in explicitly is fine, and we modify it to

def ds_union_broke {M : _} {β : M → Type} {h : ∀ m, simple_graph (β m)}
  : simple_graph (Σ m, β m) := {
  adj := begin
    intros a b,
    exact a.fst = b.fst ∧ (a.fst = b.fst →
    simple_graph.adj (h _) a.snd b.snd),
  end,
  symm := sorry, loopless := sorry, }

they still dont typecheck in the adjacency condition, but now by assumption these are equal. So I was wondering if there was someway we could tell Lean to allow it.

I was able to modify it by adding a coercion, it typechecks just fine now, but its too unwieldy for me to prove anything with it. I think the rw in the coe isn't explicit enough, but I don't know of any other approach

def worthless_coe {M : _} {β : M → Type} {a b : _} (eq : a = b)
  : β a → β b :=
begin
  rw eq,
  exact id,
end

def ds_union {M : _} {β : M → Type} {h : ∀ m, simple_graph (β m)}
  : simple_graph (Σ m, β m) := {
  adj := begin
    intros a b,
    exact a.fst = b.fst ∧ (a.fst = b.fst →
    simple_graph.adj (h _) (worthless_coe ᾰ a.snd) b.snd),
  end,
  symm := sorry, loopless := sorry, } -- cant prove symm, but loopless is easy

So I was wondering how people usually deal with Σ types and how to force lean to bend the knee in these situations.