algebra_map over nat.cast

Stream: general

[Yaël Dillies]

I don't have a MWE, but it should be easy to reproduce by having big enough imports (topology.metric_space.isometry I suspect?). The coercion from ℕ → ℝ now goes through docs#algebra_map.has_lift_t since @Kevin Buzzard's PR. I think they are defeq, but we should certainly monitor the situation and maybe tweak the priorities so that nat.cast stays over.

[Yaël Dillies]

I'm mostly worried about positivity extensions, like docs#tactic.positivity_coe breaking. @Anne Baanen, is your "unification workaround" able to fix the potential breakage?

[Kevin Buzzard]

OMG did that get merged? I've been quite busy this month...

[Eric Wieser]

Unification sounds like the right solution in the first place, not a workaround

[Eric Wieser]

Tactics should never syntactically match on instances