>>270
>本文にその複雑な添え字付きの式が使われてないということは
>本文で図式に言及する時は必ず「次の図式が成立する」みたいな形で？

うん そこを 例示すれば
>>265より https://www.kurims.kyoto-u.ac.jp/~motizuki/Inter-universal%20Teichmuller%20Theory%20III.pdf
[3] Inter-universal Teichmuller Theory III: Canonical Splittings of the Log-theta-lattice. PDF NEW !! (2020-05-18)
より
P41
Fig. 1.2: Independent basepoint indeterminacies obstruct relationship between birational and affine geometric fundamental groups

これ、表題からして 私にはワケワカですがｗ　（＾＾
で、こいつを遡って辿ると
P30
Proposition 1.2. (log-links Between F-prime-strips) Let 略
（P34までつづく）
にたどり着く
そして
P35 で
Proof. The various assertions of Proposition 1.2 follow immediately from the definitions and the references quoted in the statements of these assertions.〇
となっています
その後
Remark 1.2.1.が始まって
P39
Remark 1.2.4.の(iii) がP40で
(iii) One way to understand the incompatibility discussed in (ii), (b), is as follows. Write Δbirat v Πbirat v , Δv for the respective kernels of the natural surjections ↠ Gv,Πv ↠ Gv. Then if one forgets about the scheme-theoretic basepoints discussed in (i), Gv,Δbirat v , andΔv may be understood on both sides of the log-wall as “some topological group”, and each of the topological groups Δbirat v , Δv may be understood on both sides of the log-wall as being equipped with “some outer Gv-action” — cf. the two diagonal arrows of Fig. 1.2 below.
とつづくのです

さて、纏めると
１）Proposition 1.2.については、（ショルツ氏のレビューに批判されていますが）
　命題が数ページあって 証明が 1〜2行で終わって
　そのあと 解説ぽい Remark 1.2.1.からRemark 1.2.4.まで４つあって Fig. 1.2だと
　なっています
２）いまの場合、Proposition 1.2.のみを Lean語に翻訳すれば足りるかもですね
　解説 Remarkは、Lean語に翻訳する必要がない
　図式＝diagram は、もともと Propositionに包含されている
３）なので、IUT I〜III の定理がすべてこの調子ならば
　解説 Remark とそこに付属する図式＝diagramは、人間向けの
　おまけです
（いまの場合は、望月氏は Fig. 1.2が脳内に先にあって それを Proposition 1.2.に落としたってことかも）

IUT I〜IIIを全部チェックしてはいないので どうなるか不明ですが
まあ、やってみるしかないでしょうね