How to continue from here?

Stream: mathlib4

[Jeremy Tan]

In #9317:

theorem card_edgeFinset_turanGraph_add (hr : 0 < r) : (turanGraph (n + r) r).edgeFinset.card =
    (r - 1) * n + (turanGraph n r).edgeFinset.card + r.choose 2 := by
 rw [(turanGraph (n + r) r).edgeFinset_decompose_card (univ.map (Fin.castAddEmb r).toEmbedding)]

[Jeremy Tan]

For context, the proof I have currently goes through another 100-line proof of the number of edges in a Turán graph, which in turn requires a ton of imports. But I figure that I don't need all of that – I should be able to use the machinery of the forward direction of this theorem (decomposition into a clique and the rest)

[Jeremy Tan]

The problem is that after the above rw and a congr 2 I get impenetrable terms like
Sym2.map (fun x ↦ { val := ↑↑x, isLt := ⋯ }) (Eq.mp ⋯ (Quot.mk (Sym2.Rel ↑↑(Set.toFinset {x | ↑x < n})) (x, y))) ∈ edgeFinset (turanGraph n r)

[Jeremy Tan]

Is univ.map (Fin.castAddEmb r).toEmbedding really the best way to express the elements of Fin n mapped naturally to Fin (n + r)?

[Jeremy Tan]

I would have expected something like (Fin.castAddEmb r).range to work but thay doesn't

[Jeremy Tan]

(my parents dragged me out for dinner, please feel free to have a look at the sorries in my present code)

[Jeremy Tan]

OK I'm back

[Jeremy Tan]

Anyone?