mathlib3

4e872238 - feat(tactic/transport): transport structures across equivalences (#2251)

feat(tactic/transport): transport structures across equivalences (#2251) ~~Blocked by #2246.~~ ~~Blocked on #2319 and #2334, which both fix lower tactic layers used by `transport`.~~ From the doc-string: --- Given a goal `⊢ S β` for some parametrized structure type `S`, `transport` will look for a hypothesis `s : S α` and an equivalence `e : α ≃ β`, and attempt to close the goal by transporting `s` across the equivalence `e`. ```lean example {α : Type} [ring α] {β : Type} (e : α ≃ β) : ring β := by transport. ``` You can specify the object to transport using `transport s`, and the equivalence to transport across using `transport s using e`. --- You can just as easily transport a [`semilattice_sup_top`](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/lattice.20with.20antiautomorphism) or a `lie_ring`. In the `test/transport.lean` file we transport `semiring` from `nat` to `mynat`, and verify that it's possible to do simple things with the transported structure.