[Imo1992P2] simplification suggested by LeanCopilot with tryAtEachStep

dwrensha · Jan 15, 2025 · 67ac3cd · 67ac3cd
1 parent c0a1e46
commit 67ac3cd
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Compfiles/Imo1992P2.lean b/Compfiles/Imo1992P2.lean
@@ -83,8 +83,7 @@ problem imo1992_p2 (f : ℝ → ℝ) :
       rw [show -x + -y = - (x + y) by ring, h6, h6, h6] at h8
       linarith only [h8]
   have h8 : ∀ x y, f (x - y) = f x - f y := fun x y ↦ by
-    rw [show x - y = x + -y by ring, show f x - f y = f x + -f y by ring, ← h6]
-    exact h7 x (-y)
+    simp [sub_eq_add_neg, hf, h6, h7]
   ext x
   by_contra H
   obtain ⟨z, hz⟩ : ∃ z, 0 < z ∧ f z < 0 := by