From b270396314d83347e8f8e80f37fc8203156416ed Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Sun, 27 Aug 2023 07:22:23 -0400 Subject: [PATCH] [Iran1998Q9] simplify after field_simp improvement https://github.com/leanprover-community/mathlib4/commit/6b391efa697c6b0e8590cac08cc1c3ec02974702 --- MathPuzzles/Iran1998Q9.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/MathPuzzles/Iran1998Q9.lean b/MathPuzzles/Iran1998Q9.lean index 22975319..b94230a8 100644 --- a/MathPuzzles/Iran1998Q9.lean +++ b/MathPuzzles/Iran1998Q9.lean @@ -46,10 +46,6 @@ theorem iran1998_q9 -- -- The desired result follows. - have hxz : x ≠ 0 := by positivity - have hyz : y ≠ 0 := by positivity - have hzz : z ≠ 0 := by positivity - have hx0 : 0 ≤ x := by positivity have hy0 : 0 ≤ y := by positivity have hz0 : 0 ≤ z := by positivity