introduce 'trans' on Logos or Implis (and also use it elsewhere)

[TentativeConvert]

'trans' as a replacement for 'calc' will feel more natural if we introduce it early. I even think there are many instances of repeated 'rw's where repeated 'trans' will be more intuitive. Implis level 8 is a good example. The hint spells out a "calculation" (sequence of equivalences), which is easy to follow using 'trans'.

It's unfortunate that 'trans' does not apply to implications. But of course 'rw' doesn't either, so that's not a loss.

[TentativeConvert]

Here's a first attempt: 08bf4dc

[joneugster]

leanprover-community/mathlib4#13719 adds functionality to trans to work with implications.

example {A B C: Prop} (h : A → B) (g : B → C) : A → C := by
  trans B
  · -- ⊢ A → B
    exact h
  · -- ⊢ B → C
    exact g