chore(set_theory/game/pgame): Cleanup (#13612)

We remove redundant parentheses, and make arguments explicit when they can't be inferred.

src/set_theory/game/impartial.lean

@@ -129,7 +129,7 @@ iff.symm $ iff_not_comm.1 $ iff.symm $ not_first_wins G
 
 lemma add_self (G : pgame) [G.impartial] : (G + G).first_loses :=
   first_loses_is_zero.2 $ equiv_trans (add_congr (neg_equiv_self G) G.equiv_refl)
-  add_left_neg_equiv
+  (add_left_neg_equiv G)
 
 lemma equiv_iff_sum_first_loses (G H : pgame) [G.impartial] [H.impartial] :
   G ≈ H ↔ (G + H).first_loses :=

src/set_theory/game/pgame.lean

@@ -899,7 +899,7 @@ using_well_founded { dec_tac := pgame_wf_tac }
 theorem add_assoc_equiv {x y z : pgame} : (x + y) + z ≈ x + (y + z) :=
 (add_assoc_relabelling x y z).equiv
 
-private lemma add_le_add_right : Π {x y z : pgame} (h : x ≤ y), x + z ≤ y + z
+private lemma add_le_add_right : ∀ {x y z : pgame} (h : x ≤ y), x + z ≤ y + z
 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
 begin
   intros h,
@@ -965,7 +965,7 @@ theorem add_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w + y 
 theorem sub_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w - y ≈ x - z :=
 add_congr h₁ (neg_congr h₂)
 
-theorem add_left_neg_le_zero : Π {x : pgame}, (-x) + x ≤ 0
+theorem add_left_neg_le_zero : ∀ (x : pgame), -x + x ≤ 0
 | ⟨xl, xr, xL, xR⟩ :=
 begin
   rw [le_def],
@@ -988,35 +988,32 @@ begin
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-theorem zero_le_add_left_neg : Π {x : pgame}, 0 ≤ (-x) + x :=
+theorem zero_le_add_left_neg (x : pgame) : 0 ≤ -x + x :=
 begin
-  intro x,
   rw [le_iff_neg_ge, pgame.neg_zero],
-  exact le_trans neg_add_le add_left_neg_le_zero
+  exact le_trans neg_add_le (add_left_neg_le_zero _)
 end
 
-theorem add_left_neg_equiv {x : pgame} : (-x) + x ≈ 0 :=
-⟨add_left_neg_le_zero, zero_le_add_left_neg⟩
+theorem add_left_neg_equiv (x : pgame) : -x + x ≈ 0 :=
+⟨add_left_neg_le_zero x, zero_le_add_left_neg x⟩
 
-theorem add_right_neg_le_zero {x : pgame} : x + (-x) ≤ 0 :=
-calc x + (-x) ≤ (-x) + x : add_comm_le
-     ... ≤ 0 : add_left_neg_le_zero
+theorem add_right_neg_le_zero (x : pgame) : x + -x ≤ 0 :=
+le_trans add_comm_le (add_left_neg_le_zero x)
 
-theorem zero_le_add_right_neg {x : pgame} : 0 ≤ x + (-x) :=
-calc 0 ≤ (-x) + x : zero_le_add_left_neg
-     ... ≤ x + (-x) : add_comm_le
+theorem zero_le_add_right_neg (x : pgame) : 0 ≤ x + -x :=
+le_trans (zero_le_add_left_neg x) add_comm_le
 
-theorem add_right_neg_equiv {x : pgame} : x + (-x) ≈ 0 :=
-⟨add_right_neg_le_zero, zero_le_add_right_neg⟩
+theorem add_right_neg_equiv (x : pgame) : x + -x ≈ 0 :=
+⟨add_right_neg_le_zero x, zero_le_add_right_neg x⟩
 
 instance covariant_class_swap_add_lt : covariant_class pgame pgame (swap (+)) (<) :=
 ⟨λ x y z h, suffices z + x ≤ y + x → z ≤ y, by { rw ←not_le at ⊢ h, exact mt this h }, λ w,
   calc z ≤ z + 0        : (add_zero_relabelling _).symm.le
-     ... ≤ z + (x + -x) : add_le_add_left zero_le_add_right_neg _
+     ... ≤ z + (x + -x) : add_le_add_left (zero_le_add_right_neg x) _
      ... ≤ z + x + -x   : (add_assoc_relabelling _ _ _).symm.le
      ... ≤ y + x + -x   : add_le_add_right w _
      ... ≤ y + (x + -x) : (add_assoc_relabelling _ _ _).le
-     ... ≤ y + 0        : add_le_add_left add_right_neg_le_zero _
+     ... ≤ y + 0        : add_le_add_left (add_right_neg_le_zero x) _
      ... ≤ y            : (add_zero_relabelling _).le⟩
 
 instance covariant_class_add_lt : covariant_class pgame pgame (+) (<) :=
@@ -1025,20 +1022,20 @@ instance covariant_class_add_lt : covariant_class pgame pgame (+) (<) :=
                    ... ≤ x + z   : add_comm_le⟩
 
 theorem le_iff_sub_nonneg {x y : pgame} : x ≤ y ↔ 0 ≤ y - x :=
-⟨λ h, le_trans zero_le_add_right_neg (add_le_add_right h _),
+⟨λ h, le_trans (zero_le_add_right_neg x) (add_le_add_right h _),
  λ h,
   calc x ≤ 0 + x : (zero_add_relabelling x).symm.le
      ... ≤ y - x + x : add_le_add_right h _
      ... ≤ y + (-x + x) : (add_assoc_relabelling _ _ _).le
-     ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero) _
+     ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero x) _
      ... ≤ y : (add_zero_relabelling y).le⟩
 theorem lt_iff_sub_pos {x y : pgame} : x < y ↔ 0 < y - x :=
-⟨λ h, lt_of_le_of_lt zero_le_add_right_neg (add_lt_add_right h _),
+⟨λ h, lt_of_le_of_lt (zero_le_add_right_neg x) (add_lt_add_right h _),
  λ h,
   calc x ≤ 0 + x : (zero_add_relabelling x).symm.le
      ... < y - x + x : add_lt_add_right h _
      ... ≤ y + (-x + x) : (add_assoc_relabelling _ _ _).le
-     ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero) _
+     ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero x) _
      ... ≤ y : (add_zero_relabelling y).le⟩
 
 /-- The pre-game `star`, which is fuzzy/confused with zero. -/

src/set_theory/surreal/basic.lean

@@ -316,10 +316,10 @@ instance : ordered_add_comm_group surreal :=
 { add               := (+),
   add_assoc         := by { rintros ⟨_⟩ ⟨_⟩ ⟨_⟩, exact quotient.sound add_assoc_equiv },
   zero              := 0,
-  zero_add          := by { rintros ⟨_⟩, exact quotient.sound (pgame.zero_add_equiv _) },
-  add_zero          := by { rintros ⟨_⟩, exact quotient.sound (pgame.add_zero_equiv _) },
+  zero_add          := by { rintros ⟨_⟩, exact quotient.sound (pgame.zero_add_equiv a) },
+  add_zero          := by { rintros ⟨_⟩, exact quotient.sound (pgame.add_zero_equiv a) },
   neg               := has_neg.neg,
-  add_left_neg      := by { rintros ⟨_⟩, exact quotient.sound pgame.add_left_neg_equiv },
+  add_left_neg      := by { rintros ⟨_⟩, exact quotient.sound (pgame.add_left_neg_equiv a) },
   add_comm          := by { rintros ⟨_⟩ ⟨_⟩, exact quotient.sound pgame.add_comm_equiv },
   le                := (≤),
   lt                := (<),