calc with bij_on

Stream: general

[Reid Barton]

Is there a way I could use calc to chain together bij_on_comp?
bij_on_comp : bij_on g b c → bij_on f a b → bij_on (g ∘ f) a c

[Reid Barton]

wow, it actually works! local notation a ` ~~ ` b := bij_on _ a b, and define a @[trans] version of bij_on_comp with arguments in the right order

[Kevin Buzzard]

Yeah we took apart calc recently and found out that it was just reading from left to right and attempting to prove a R b S c -> a T c by using results tagged with @trans

[Kevin Buzzard]

https://github.com/kbuzzard/mathlib/blob/master/docs/extras/calc.md

[Kevin Buzzard]

Calc is great.

[Reid Barton]

I wasn't sure whether it would also be able to handle the accumulation going on in the first parameter of bij_on

[Reid Barton]

but apparently it doesn't care

[Kevin Buzzard]

Oh I see

[Kevin Buzzard]

You should add a comment to the docs :-)

[Kevin Buzzard]

I guess the elaborator just does its best. This software is so cool