From d7f61f1fdc3215a97845591992dfe554f0e0e1d5 Mon Sep 17 00:00:00 2001
From: Xyndra <71836523+Xyndra@users.noreply.github.com>
Date: Sat, 15 Aug 2026 16:37:56 +0200
Subject: [PATCH] Simplify AdvMult L04

---
 Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean b/Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean
index 97de4141..a4c836d4 100644
--- a/Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean
+++ b/Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean
@@ -21,5 +21,5 @@ Statement one_le_of_ne_zero (a : ℕ) (ha : a ≠ 0) : 1 ≤ a := by
   Hint (hidden := true) "Now take apart the existence statement with `cases ha with n hn`."
   cases ha with n hn
   use n
-  rw [hn, succ_eq_add_one, add_comm]
-  rfl
+  rw [add_comm, <-succ_eq_add_one]
+  exact hn