Proof Tree Composer

intro

Introduce hypothesis from forall/implication

intros

Introduce all hypotheses

apply

Apply a hypothesis or lemma

exact

Provide exact proof term

rewrite

Rewrite using equality hypothesis

simp

Simplify using known lemmas

induction

Prove by induction on natural number

cases

Case analysis on hypothesis

rfl

Prove by reflexivity

trivial

Solve trivial goals

assumption

Use exact hypothesis