Documentation

Mathlib.Tactic.Relation.Trans

trans tactic #

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

Discrimation tree settings for the trans extension.

Equations
Instances For
    def Trans.simple {α : Sort u} {r : ααSort v} {a : α} {b : α} {c : α} [Trans r r r] :
    r a br b cr a c

    Composition using the Trans class in the homogeneous case.

    Equations
    • Trans.simple = trans
    Instances For
      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)} [Trans r s t] :
      r a bs b ct a c

      Composition using the Trans class in the general case.

      Equations
      • Trans.het = trans
      Instances For

        solving e ← mkAppM' f #[x]

        Equations
        Instances For

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

          Equations
          Instances For

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

            Equations
            Instances For

              Internal definition for trans tactic. Either a binary relation or a non-dependent arrow.

              Instances For

                Finds an explicit binary relation in the argument, if possible.

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

                  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.

                  Additionally, trans also applies to a goal whose target has the form t → u, in which case it replaces the goal with t → s and s → u.

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