P3_of_le_left — Mathlib

English

Let i be a left move; if IH3 x1 (x2.moveLeft i) x2 y1 y2 holds and hl : x1 ≤ x2.moveLeft i, then P3 x1 x2 y1 y2.

Русский

Пусть i принадлежит левому ходу; если IH3 x1 (x2.moveLeft i) x2 y1 y2 выполняется и hl: x1 ≤ x2.moveLeft i, тогда P3 x1 x2 y1 y2.

LaTeX

$$$\\\\forall x_1 x_2 y_1 y_2,\\\\\\\\forall i \\\\in x_2.LeftMoves, IH3 x_1 (x_2.moveLeft i) x_2 y_1 y_2 \\\\rightarrow (x_1 \\\\le x_2.moveLeft i) \\\\rightarrow P3 x_1 x_2 y_1 y_2.$$$

Lean4

theorem P3_of_le_left {y₁ y₂} (i) (h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂) (hl : x₁ ≤ x₂.moveLeft i) : P3 x₁ x₂ y₁ y₂ :=
  by
  obtain (hl | he) := lt_or_equiv_of_le hl
  · exact (h.2.2.2 hl).trans h.2.2.1
  · rw [P3, h.1 he, h.2.1 he]
    exact h.2.2.1

Похожие утверждения