coe_degree for simple graphs

Stream: mathlib4

[Moritz Firsching]

I'm stuck with one issue porting Combinatorics.SimpleGraph.Matching , mathlib4#3071:
There seems to be some sort of coe_degree missing, namely I need to have

∀ (v : M.verts), @SimpleGraph.degree (↑M.verts) (Subgraph.coe M) v (coeFiniteAt v)  =
        @SimpleGraph.degree (↑M.verts) (Subgraph.coe M) v (neighborSetFintype (Subgraph.coe M) v)

If I could prove this as a have inside IsMatching.even_card, I can finish porting the file. Can someone help?

[Kyle Miller]

@Moritz Firsching I think I figured it out. docs4#SimpleGraph.Subgraph.coe_degree is a simp lemma that should apply, but it uses an instance argument for its Fintype instance. A difference between Lean 3 and Lean 4 is that Lean 3 could treat instance arguments as implicit arguments. I inserted a convert_to to swap out a Fintype instance argument, which let the original simp go through.

[Moritz Firsching]

Cool, I used the same convert_to trick just now in mathlib4#3102, thanks for pointing it out @Kyle Miller!