EmbeddingLike

Stream: mathlib4

[Eric Rodriguez]

I'm currently nearly done fixing at least all the syntax proof errors in mathlib4#631, and EmbeddingLike seems completely broken

[Eric Rodriguez]

I can't seem to get any methods of it whatsoever to work, and I guess this is to do with the coercion changes

[Eric Rodriguez]

I guess this will also go for FunLike, which is not a good sign considering how much we depend on it...

[Scott Morrison]

@Eric Rodriguez, did you mean a different PR? There's nothing about EmbeddingLike in mathlib4#631

[Eric Rodriguez]

no, but it uses its methods in many proofs

[Eric Rodriguez]

for example piCongrLeft'_update, try using the squeeze_simp from docs#function.Pi_congr_left'_update there

[Scott Morrison]

What syntax errors were you talking about, though? I thought there were only broken proofs since at least yesterday.

[Eric Rodriguez]

sorry, that's what I meant by syntax; I'll be more precise with my wording

[Eric Rodriguez]

essentially I can't seem to get the goals to unify at all

[Eric Rodriguez]

if you want a concrete example, see L1917 of the said file; I mention it a couple other times as it used to work with simp, too, and now it doesn't.