# The `to_app`

attribute #

Adding `@[to_app]`

to a lemma named `F`

of shape `∀ .., η = θ`

, where `η θ : f ⟶ g`

are 2-morphisms
in some bicategory, create a new lemma named `F_app`

. This lemma is obtained by first specializing
the bicategory in which the equality is taking place to `Cat`

, then applying `NatTrans.congr_app`

to obtain a proof of `∀ ... (X : Cat), η.app X = θ.app X`

, and finally simplifying the conclusion
using some basic lemmas in the bicategory `Cat`

:
`Cat.whiskerLeft_app`

, `Cat.whiskerRight_app`

, `Cat.id_app`

, `Cat.comp_app`

and `Cat.eqToHom_app`

So, for example, if the conclusion of `F`

is `f ◁ η = θ`

then the conclusion of `F_app`

will be
`η.app (f.obj X) = θ.app X`

.

This is useful for automatically generating lemmas that can be applied to expressions of 1-morphisms
in `Cat`

which contain components of 2-morphisms.

There is also a term elaborator `to_app_of% t`

for use within proofs.

Simplify an expression in `Cat`

using basic properties of `NatTrans.app`

.

## Equations

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

## Instances For

Given a term of type `∀ ..., η = θ`

, where `η θ : f ⟶ g`

are 2-morphisms in some bicategory
`B`

, which is bound by the `∀`

binder, get the corresponding equation in the bicategory `Cat`

.

It is important here that the levels in the term are level metavariables, as otherwise these will
not be reassignable to the corresponding levels of `Cat`

.

## Equations

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

## Instances For

Recursive function which applies `mkLambdaFVars`

stepwise
(so that each step can have different binderinfos)

## Equations

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

## Instances For

Given morphisms `f g : C ⟶ D`

in the bicategory `Cat`

, and an equation `η = θ`

between 2-morphisms
(possibly after a `∀`

binder), produce the equation `∀ (X : C), f.app X = g.app X`

, and simplify
it using basic lemmas about `NatTrans.app`

.

## Equations

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

## Instances For

Adding `@[to_app]`

to a lemma named `F`

of shape `∀ .., η = θ`

, where `η θ : f ⟶ g`

are 2-morphisms
in some bicategory, create a new lemma named `F_app`

. This lemma is obtained by first specializing
the bicategory in which the equality is taking place to `Cat`

, then applying `NatTrans.congr_app`

to obtain a proof of `∀ ... (X : Cat), η.app X = θ.app X`

, and finally simplifying the conclusion
using some basic lemmas in the bicategory `Cat`

:
`Cat.whiskerLeft_app`

, `Cat.whiskerRight_app`

, `Cat.id_app`

, `Cat.comp_app`

and `Cat.eqToHom_app`

So, for example, if the conclusion of `F`

is `f ◁ η = θ`

then the conclusion of `F_app`

will be
`η.app (f.obj X) = θ.app X`

.

This is useful for automatically generating lemmas that can be applied to expressions of 1-morphisms
in `Cat`

which contain components of 2-morphisms.

Note that if you want both the lemma and the new lemma to be `simp`

lemmas, you should tag the lemma
`@[to_app (attr := simp)]`

. The variant `@[simp, to_app]`

on a lemma `F`

will tag `F`

with
`@[simp]`

, but not `F_app`

(this is sometimes useful).

## Equations

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

## Instances For

Given an equation `t`

of the form `η = θ`

between 2-morphisms `f ⟶ g`

with `f g : C ⟶ D`

in the
bicategory `Cat`

(possibly after a `∀`

binder), `to_app_of% t`

produces the equation
`∀ (X : C), η.app X = θ.app X`

(where `X`

is an object in the domain of `f`

and `g`

), and simplifies
it suitably using basic lemmas about `NatTrans.app`

.

## Equations

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