-- Mathlib/SetTheory/Surreal/Multiplication.lean
/-- Symmetry properties of `IH24`. -/
lemma ih24_neg : IH24 x₁ x₂ y → IH24 (-x₂) (-x₁) y ∧ IH24 x₁ x₂ (-y)

Proof state:
case refine_3
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ z.IsOption y → P24 x₁ x₂ z

Tactic:
first | exact (@h <| -z).2.1 | exact (@h <| -z).1 | exact (@h z).2.2

Result:
no goals

Proof state:
case refine_3
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ z.IsOption y → P24 (- -x₁) (- -x₂) z

Tactic:
simp only [neg_neg]

Result:
case refine_3
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ z.IsOption y → P24 x₁ x₂ z

Proof state:
case refine_3
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ z.IsOption y → P24 x₁ x₂ z

Tactic:
exact (@h z).2.2

Result:
no goals

Proof state:
x₁ x₂ y : PGame
⊢ (∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)) →
    (∀ ⦃z : PGame⦄,
        ((-z).IsOption x₂ → P24 z (-x₁) y) ∧ ((-z).IsOption x₁ → P24 (-x₂) z y) ∧ (z.IsOption y → P24 (-x₂) (-x₁) z)) ∧
      ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ ((-z).IsOption y → P24 x₁ x₂ z)

Tactic:
refine fun h ↦ ⟨fun z ↦ ⟨?_, ?_, ?_⟩,
  fun z ↦ ⟨(@h z).1, (@h z).2.1, P24_neg_right.2 ∘ (@h <| -z).2.2⟩⟩

Result:
case refine_1
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ (-z).IsOption x₂ → P24 z (-x₁) y

case refine_2
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ (-z).IsOption x₁ → P24 (-x₂) z y

case refine_3
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ z.IsOption y → P24 (-x₂) (-x₁) z

Proof state:
case refine_3
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ z.IsOption y → P24 (-x₂) (-x₁) z

Tactic:
rw [P24_neg_left]

Result:
case refine_3
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ z.IsOption y → P24 (- -x₁) (- -x₂) z

Proof state:
x₁ x₂ y : PGame
⊢ IH24 x₁ x₂ y → IH24 (-x₂) (-x₁) y ∧ IH24 x₁ x₂ (-y)

Tactic:
simp_rw [IH24, ← P24_neg_right, isOption_neg]

Result:
x₁ x₂ y : PGame
⊢ (∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)) →
    (∀ ⦃z : PGame⦄,
        ((-z).IsOption x₂ → P24 z (-x₁) y) ∧ ((-z).IsOption x₁ → P24 (-x₂) z y) ∧ (z.IsOption y → P24 (-x₂) (-x₁) z)) ∧
      ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ ((-z).IsOption y → P24 x₁ x₂ z)

Proof state:
case refine_1
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ (-z).IsOption x₂ → P24 z (-x₁) y

case refine_2
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ (-z).IsOption x₁ → P24 (-x₂) z y

case refine_3
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ z.IsOption y → P24 (-x₂) (-x₁) z

Tactic:
all_goals
  rw [P24_neg_left]
  simp only [neg_neg]
  first | exact (@h <| -z).2.1 | exact (@h <| -z).1 | exact (@h z).2.2

Result:
no goals

Proof state:
case refine_1
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ (-z).IsOption x₂ → P24 x₁ (-z) y

Tactic:
exact (@h <| -z).2.1

Result:
no goals

Proof state:
case refine_2
x₁ x₂ y : PGame
h : ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)
z : PGame
⊢ (-z).IsOption x₁ → P24 (-z) x₂ y

Tactic:
exact (@h <| -z).1

Result:
no goals