我发现了一些非常漂亮的结构良好的证明，但我找不到以这种风格创建自己的证明的方法

Question

我发现这种显示方程式证明的方式非常漂亮。Vene Vermo 在他的论文中多次使用了这种方式，我想知道如何重现它。在 pdf 中选择内容时，我发现竖线是许多单独的字符，我没有其他线索。

Answer 1

它可以通过两个嵌套环境获得align(ed)at：

    \documentclass[french]{article}

    \usepackage[utf8]{inputenc}
    \usepackage[T1]{fontenc}
    \usepackage{empheq, stmaryrd}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\In}{in}
\DeclareMathOperator{\fst}{fst}
\DeclareMathOperator{\snd}{snd}
\DeclarePairedDelimiter\innerp\langle\rangle
\newcommand\sfF{\mathsf{F}}

    \begin{document}

 \begin{empheq}[left = {\empheqlbrack}]{alignat* = 2}
 &{} \triangleright{} & \enspace &f \circ\In = \varphi\circ\sfF\innerp{f, \id}\\[-2ex]
 \cline{2-4}\noalign{\vskip-0.5ex}
 & & & f \\
  & = & &\quad\text{-- pairing --} \\
 & & & \fst\circ \innerp{f, \id} \\
 & = & &\quad\text{-- cata-\textsc{Charn} --} \\
& \hphantom{{}={}} & &\hskip 0.75em \left[%
 \begin{alignedat}{2}
 & & & \innerp{f, \id}\circ \In \\
 & = & \quad & \quad\text{-- pairing --} \\
 & & & \innerp{f\circ\In, \In} \\
 & = & & \quad\text{-- $\sfF$ functor --} \\
 & & & \innerp{f\circ\In, \In\circ\sfF\id} \\
 & = & & \quad\text{-- pairing --} \\
 & & & \innerp[\big]{f\circ\In, \In\circ\sfF(\snd\circ\innerp{f, \id})} \\
 & = & & \quad\text{-- $\triangleleft, \mathsf{F}$ functor --} \\
 & & & \innerp[\big]{\varphi\circ\sfF\innerp{f, \id}, \In\circ\sfF\:\snd\circ\sfF\:\innerp{f, \id}} \\
 & = & & \quad\text{-- pairing --} \\
 & & & \innerp{\varphi, \In\circ\sfF\:\snd}\circ\sfF\:\innerp{f, \id}
 \end{alignedat}\right. \\[1ex]
  & & & \fst\circ\llparenthesis\innerp{\varphi, \In\circ\sfF\snd}\rrparenthesis
    \end{empheq}

    \end{document}