# Documentation

Mathlib.Tactic.Relation.Trans

# trans tactic #

This implements the trans tactic, which can apply transitivity theorems with an optional middle variable argument.

Environment extension storing transitivity lemmas

def Trans.simple {α : Sort u_1} {r : ααSort u_2} {a : α} {b : α} {c : α} [inst : Trans r r r] :
r a br b cr a c

Composition using the Trans class in the homogeneous case.

Equations
• Trans.simple = trans
def Trans.het {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {a : α} {b : β} {c : γ} {r : αβSort u} {s : βγSort v} {t : outParam (αγSort w)} [inst : Trans r s t] :
r a bs b ct a c

Composition using the Trans class in the general case.

Equations
• Trans.het = trans

solving e ← mkAppM' f #[x]← mkAppM' f #[x]

Equations
• One or more equations did not get rendered due to their size.

solving tgt ← mkAppM' rel #[x, z]← mkAppM' rel #[x, z] given tgt = f z

Equations
• One or more equations did not get rendered due to their size.
• = pure none

refining tgt ← mkAppM' rel #[x, z]← mkAppM' rel #[x, z] dropping more arguments if possible

Equations
• One or more equations did not get rendered due to their size.
• = pure (rel, x)

trans applies to a goal whose target has the form t ~ u where ~ is a transitive relation, that is, a relation which has a transitivity lemma tagged with the attribute [trans].

• trans s replaces the goal with the two subgoals t ~ s and s ~ u.
• If s is omitted, then a metavariable is used instead.
Equations
• One or more equations did not get rendered due to their size.