feat(set_theory/game/pgame): Strengthen move_{left/right}_mk (#13646)

leanprover-community · Apr 23, 2022 · 34b1cfd · 34b1cfd
1 parent 44a05db
commit 34b1cfd
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
@@ -138,15 +138,15 @@ pgame.mk (fin L.length) (fin R.length) (λ i, L.nth_le i i.is_lt) (λ j, R.nth_l
 
 /-- The new game after Left makes an allowed move. -/
 def move_left : Π (g : pgame), left_moves g → pgame
-| (mk l _ L _) i := L i
+| (mk l _ L _) := L
 /-- The new game after Right makes an allowed move. -/
 def move_right : Π (g : pgame), right_moves g → pgame
-| (mk _ r _ R) j := R j
+| (mk _ r _ R) := R
 
 @[simp] lemma left_moves_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).left_moves = xl := rfl
-@[simp] lemma move_left_mk {xl xr xL xR i} : (⟨xl, xr, xL, xR⟩ : pgame).move_left i = xL i := rfl
+@[simp] lemma move_left_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).move_left = xL := rfl
 @[simp] lemma right_moves_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).right_moves = xr := rfl
-@[simp] lemma move_right_mk {xl xr xL xR j} : (⟨xl, xr, xL, xR⟩ : pgame).move_right j = xR j := rfl
+@[simp] lemma move_right_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).move_right = xR := rfl
 
 /-- `subsequent p q` says that `p` can be obtained by playing
   some nonempty sequence of moves from `q`. -/