AlphaProof IMO 2024 P1 in LEAN 之 repeat 与 nlinarith 策略（Tactic）

        书接上文，此时，AlphaProof 关注的目的如下：

        接着，AlphaProof 使用了 simp_all 与 have 策略，如下：

        此前已对上述两策略进行讲解，这里就不再赘述了。

        在第二个 simp_all 策略完成后，目的被改写为：

        此时，AlphaProof 使用 cases 策略进行分类讨论，其策略参数为 this.eq_or_lt。其中的 this 为最近的 this，即

this : ↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

        那么，eq_or_lt 的定义如下：

        即，等于（=）或小于（<）。

        那么，原目的 case this.ind.intro.inl 被 cases 策略，分解为两个目的，case this.ind.intro.inl.inl 与 this.ind.intro.inl.inr。如下：

        关注两目的（goal）的最后假设 h。符合，cases 策略 的拆分。

        接着，AlphaProof 使用点策略，关于第一个目的，即 this.ind.intro.inl.inl 。并使用了 repeat 策略，如下：

        这里的 repeat 策略，重复使用 use 策略，同时 by nlinarith 提供 use 策略的参数。 也就是，by 启动策略机制，通过 nlinarith 策略，产生一个 值，供给 use 策略使用。

        也就是，上图所示的，等价于，下图所示的：

        那么，首先，需要查看 nlinarith 策略的意思，其定义如下：

        其介绍如下：

        其作用，也就是连续使用线性计算灯饰，完成上面的等式转换，使得 证明

⌊(n+1) α⌋ = 2n(l-⌊α⌋) + ⌊α⌋

        也就是，证明目的 this.ind.intro.inl.inl，如下：

        另，AlphaProof 使用 nlinarith 策略，通过 反证法，证明 目的 this.ind.intro.inl.inr，如下：

        目的 this.ind.intro.inl.inr 如下：

        因假设产生矛盾，那么其目标（Target）自然成立。

        通过  this.ind.intro.inl.inl 与  this.ind.intro.inl.inr 的证明，实现了  this.ind.intro.inl 的证明，即

        成立。

        那么，接下来，需要证明的是目的 this.ind.intro.inr，以及由两个 suffices 策略产生的 两个假设 this。敬请期待。