English
Let IH24 x1 x2 y and IH4 x1 x2 y hold, and hl: MulOptionsLTMul x2 y. Then for all i in LeftMoves(x2) and j in LeftMoves(y), IH3 x1 (x2.moveLeft i) x2 (y.moveLeft j) y.
Русский
Пусть выполняются IH24 x1 x2 y и IH4 x1 x2 y, и hl: MulOptionsLTMul x2 y. Тогда для всех i из LeftMoves(x2) и j из LeftMoves(y) выполняется IH3 x1 (x2.moveLeft i) x2 (y.moveLeft j) y.
LaTeX
$$$\\\\forall x_1 x_2 y,\\\\ IH24 x_1 x_2 y \\\\rightarrow IH4 x_1 x_2 y \\\\rightarrow MulOptionsLTMul x_2 y \\\\rightarrow \\\\forall i \\\\in x_2.LeftMoves, \\\\forall j \\\\in y.LeftMoves, \\\\ IH3 x_1 (x_2.moveLeft i) x_2 (y.moveLeft j) y.$$$
Lean4
theorem ih3_of_ih (h24 : IH24 x₁ x₂ y) (h4 : IH4 x₁ x₂ y) (hl : MulOptionsLTMul x₂ y) (i j) :
IH3 x₁ (x₂.moveLeft i) x₂ (y.moveLeft j) y :=
have ml := @IsOption.moveLeft
have h24 := (@h24 _).2.1 (ml i)
⟨(h4 <| ml j).2 (ml i), h24.1, mulOption_lt_mul_iff_P3.1 (@hl i j), fun l ↦ (h24.2 l).1 _⟩
