#explode decl_name displays a proof term in a line-by-line format somewhat akin to a Fitch-style
proof or the Metamath proof style.
#explode_widget decl_name renders a widget that displays an #explode proof.
The output of #explode is a Fitch-style proof in a four-column diagram modeled after Metamath
proof displays like this. The headers of the columns are
"Step", "Hyp", "Ref", "Type" (or "Expression" in the case of Metamath):
Step: An increasing sequence of numbers to number each step in the proof, used in the Hyp field.
Hyp: The direct children of the current step. Most theorems are implications like A -> B -> C,
and so on the step proving C the Hyp field will refer to the steps that prove A and B.
Ref: The name of the theorem being applied. This is well-defined in Metamath, but in Lean there
are some special steps that may have long names because the structure of proof terms doesn't
exactly match this mold.
If the theorem is foo (x y : Z) : A x -> B y -> C x y:
the Ref field will contain foo,
x and y will be suppressed, because term construction is not interesting, and
the Hyp field will reference steps proving A x and B y. This corresponds to a proof term
like @foo x y pA pB where pA and pB are subproofs.
If the head of the proof term is a local constant or lambda, then in this case the Ref will
say ∀E for forall-elimination. This happens when you have for example h : A -> B and
ha : A and prove b by h ha; we reinterpret this as if it said ∀E h ha where ∀E is
(n-ary) modus ponens.
If the proof term is a lambda, we will also use ∀I for forall-introduction, referencing the
body of the lambda. The indentation level will increase, and a bracket will surround the proof
of the body of the lambda, starting at a proof step labeled with the name of the lambda variable
and its type, and ending with the ∀I step. Metamath doesn't have steps like this, but the
style is based on Fitch proofs in first-order logic.
Type: This contains the type of the proof term, the theorem being proven at the current step.
This proof layout differs from #print in using lots of intermediate step displays so that you
can follow along and don't have to see term construction steps because they are implicitly in the
intermediate step displays.
Also, it is common for a Lean theorem to begin with a sequence of lambdas introducing local
constants of the theorem. In order to minimize the indentation level, the ∀I steps at the end of
the proof will be introduced in a group and the indentation will stay fixed. (The indentation
brackets are only needed in order to delimit the scope of assumptions, and these assumptions
have global scope anyway so detailed tracking is not necessary.)