-- Mathlib/SetTheory/Surreal/Multiplication.lean
theorem mul_right_le_of_equiv (h₁ : x₁.Numeric) (h₂ : x₂.Numeric)
    (h₁₂ : IH24 x₁ x₂ y) (h₂₁ : IH24 x₂ x₁ y) (he : x₁ ≈ x₂) : x₁ * y ≤ x₂ * y

Proof state:
case h₂.left
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
i✝ : x₂.LeftMoves
j✝ : (-y).LeftMoves
⊢ ⟦x₂.mulOption (-y) i✝ j✝⟧ < ⟦x₁ * -y⟧

Tactic:
apply mulOption_lt_mul_of_equiv h₂ (ih24_neg h₂₁).2 (symm he)

Result:
no goals

Proof state:
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ x₁ * y ≤ x₂ * y

Tactic:
apply PGame.le_of_forall_lt <;> simp_rw [lt_iff_game_lt]

Result:
case h₁
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ ∀ (i : (x₁ * y).LeftMoves), ⟦(x₁ * y).moveLeft i⟧ < ⟦x₂ * y⟧

case h₂
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ ∀ (j : (x₂ * y).RightMoves), ⟦x₁ * y⟧ < ⟦(x₂ * y).moveRight j⟧

Proof state:
case h₁
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ ∀ (i : (-x₁).LeftMoves) (j : (-y).LeftMoves), ⟦-x₂ * -y⟧ > ⟦(-x₁).mulOption (-y) i j⟧

Tactic:
exact mulOption_lt_mul_of_equiv h₁.neg (ih24_neg <| (ih24_neg h₂₁).1).2 he'

Result:
no goals

Proof state:
case h₂
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ (∀ (i : x₂.LeftMoves) (j : (-y).LeftMoves), ⟦x₁ * y⟧ < -⟦x₂.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x₂).LeftMoves) (j : y.LeftMoves), ⟦x₁ * y⟧ < -⟦(-x₂).mulOption y i j⟧

Tactic:
constructor <;> intros <;> rw [lt_neg]

Result:
case h₂.left
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
i✝ : x₂.LeftMoves
j✝ : (-y).LeftMoves
⊢ ⟦x₂.mulOption (-y) i✝ j✝⟧ < -⟦x₁ * y⟧

case h₂.right
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
i✝ : (-x₂).LeftMoves
j✝ : y.LeftMoves
⊢ ⟦(-x₂).mulOption y i✝ j✝⟧ < -⟦x₁ * y⟧

Proof state:
case h₂.right
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
i✝ : (-x₂).LeftMoves
j✝ : y.LeftMoves
⊢ ⟦(-x₂).mulOption y i✝ j✝⟧ < -⟦x₁ * y⟧

Tactic:
rw [← quot_neg_mul]

Result:
case h₂.right
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
i✝ : (-x₂).LeftMoves
j✝ : y.LeftMoves
⊢ ⟦(-x₂).mulOption y i✝ j✝⟧ < ⟦-x₁ * y⟧

Proof state:
case h₂
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ ∀ (j : (x₂ * y).RightMoves), ⟦x₁ * y⟧ < ⟦(x₂ * y).moveRight j⟧

Tactic:
rw [rightMoves_mul_iff]

Result:
case h₂
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ (∀ (i : x₂.LeftMoves) (j : (-y).LeftMoves), ⟦x₁ * y⟧ < -⟦x₂.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x₂).LeftMoves) (j : y.LeftMoves), ⟦x₁ * y⟧ < -⟦(-x₂).mulOption y i j⟧

Proof state:
case h₁
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ (∀ (i : x₁.LeftMoves) (j : y.LeftMoves), ⟦x₂ * y⟧ > ⟦x₁.mulOption y i j⟧) ∧
    ∀ (i : (-x₁).LeftMoves) (j : (-y).LeftMoves), ⟦x₂ * y⟧ > ⟦(-x₁).mulOption (-y) i j⟧

Tactic:
refine ⟨mulOption_lt_mul_of_equiv h₁ h₁₂ he, ?_⟩

Result:
case h₁
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ ∀ (i : (-x₁).LeftMoves) (j : (-y).LeftMoves), ⟦x₂ * y⟧ > ⟦(-x₁).mulOption (-y) i j⟧

Proof state:
case h₂.left
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
i✝ : x₂.LeftMoves
j✝ : (-y).LeftMoves
⊢ ⟦x₂.mulOption (-y) i✝ j✝⟧ < -⟦x₁ * y⟧

Tactic:
rw [← quot_mul_neg]

Result:
case h₂.left
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
i✝ : x₂.LeftMoves
j✝ : (-y).LeftMoves
⊢ ⟦x₂.mulOption (-y) i✝ j✝⟧ < ⟦x₁ * -y⟧

Proof state:
case h₂.right
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
i✝ : (-x₂).LeftMoves
j✝ : y.LeftMoves
⊢ ⟦(-x₂).mulOption y i✝ j✝⟧ < ⟦-x₁ * y⟧

Tactic:
apply mulOption_lt_mul_of_equiv h₂.neg (ih24_neg h₁₂).1 (symm he')

Result:
no goals

Proof state:
case h₁
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ ∀ (i : (-x₁).LeftMoves) (j : (-y).LeftMoves), ⟦x₂ * y⟧ > ⟦(-x₁).mulOption (-y) i j⟧

Tactic:
rw [← quot_neg_mul_neg]

Result:
case h₁
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ ∀ (i : (-x₁).LeftMoves) (j : (-y).LeftMoves), ⟦-x₂ * -y⟧ > ⟦(-x₁).mulOption (-y) i j⟧

Proof state:
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
⊢ x₁ * y ≤ x₂ * y

Tactic:
have he' := neg_equiv_neg_iff.2 he

Result:
x₁ x₂ y : PGame
h₁ : x₁.Numeric
h₂ : x₂.Numeric
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
he : x₁ ≈ x₂
he' : -x₁ ≈ -x₂
⊢ x₁ * y ≤ x₂ * y