From e7bb46ab49219240762e53df50723d6f4e7e1d62 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Tue, 17 Sep 2024 17:39:40 -0600 Subject: [PATCH] fix merge --- Mathlib/SetTheory/Game/Nim.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Game/Nim.lean b/Mathlib/SetTheory/Game/Nim.lean index 111bec1a5d828..dea7c7401922c 100644 --- a/Mathlib/SetTheory/Game/Nim.lean +++ b/Mathlib/SetTheory/Game/Nim.lean @@ -226,7 +226,8 @@ theorem grundyValue_eq_mex_left (G : PGame) : theorem grundyValue_ne_moveLeft {G : PGame} (i : G.LeftMoves) : grundyValue (G.moveLeft i) ≠ grundyValue G := by conv_rhs => rw [grundyValue_eq_sInf_moveLeft] - have := csInf_mem (compl_nonempty_of_small (Set.range fun i => grundyValue (G.moveLeft i))) + have := csInf_mem (nonempty_of_not_bddAbove <| + not_bddAbove_compl_of_small (Set.range fun i => grundyValue (G.moveLeft i))) rw [Set.mem_compl_iff, Set.mem_range, not_exists] at this exact this _