mathlib documentation

tactic.transport

The transport tactic #

transport attempts to move an s : S α expression across an equivalence e : α ≃ β to solve a goal of the form S β, by building the new object field by field, taking each field of s and rewriting it along e using the equiv_rw tactic.

We try to ensure good definitional properties, so that, for example, when we transport a monoid α to a monoid β, the new multiplication is definitionally λ x y, e (e.symm a * e.symm b).

source
meta def simp_attr.transport_simps  :
(user_attribute simp_lemmas)

The simpset transport_simps is used by the tactic transport to simplify certain expressions involving application of equivalences, and trivial eq.rec or ep.mpr conversions. It's probably best not to adjust it without understanding the algorithm used by transport.

source
@[nolint]
meta def tactic.transport (s e : expr) :
tactic unit

Given s : S α for some structure S depending on a type α, and an equivalence e : α ≃ β, try to produce an S β, by transporting data and axioms across e using equiv_rw.

source
meta def tactic.interactive.transport (s : interactive.parse interactive.types.texpr?) (e : interactive.parse (lean.parser.tk "using" *> interactive.types.texpr)) :
tactic.interactive.itactic

Given a goal ⊢ S β for some type class S, and an equivalence e : α ≃ β. transport using e will look for a hypothesis s : S α, and attempt to close the goal by transporting s across the equivalence e.

example {α : Type} [ring α] {β : Type} (e : α ≃ β) : ring β :=
by transport using e.

You can specify the object to transport using transport s using e.

transport works by attempting to copy each of the operations and axiom fields of s, rewriting them using equiv_rw e and defining a new structure using these rewritten fields.

If it fails to fill in all the new fields, transport will produce new subgoals. It's probably best to think about which missing simp lemmas would have allowed transport to finish, rather than solving these goals by hand. (This may require looking at the implementation of tranport to understand its algorithm; there are several examples of "transport-by-hand" at the end of test/equiv_rw.lean, which transport is an abstraction of.)