From 9d9fee5ba77226bcf22351ea6cfd5e156302faa6 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Fri, 27 Jun 2025 08:37:07 +0200
Subject: [PATCH 1/3] Start

---
 HumanEvalLean/HumanEval24.lean | 3 ---
 lean-toolchain                 | 2 +-
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/HumanEvalLean/HumanEval24.lean b/HumanEvalLean/HumanEval24.lean
index b82886a..8d65073 100644
--- a/HumanEvalLean/HumanEval24.lean
+++ b/HumanEvalLean/HumanEval24.lean
@@ -31,16 +31,13 @@ theorem largestDivisorSpec_go {n i : Nat} (hi : 2 ≤ i)
     (hi' : ∀ j, 2 ≤ j → j < i → n % j ≠ 0) : LargestDivisorSpec n (largestDivisor.go n i) := by
   fun_induction largestDivisor.go n i
   case case1 i hni =>
-    rw [largestDivisor.go, dif_pos hni]
     apply LargestDivisorSpec.one
     intro j hj hj'
     apply hi' _ hj
     exact Nat.mul_self_lt_mul_self_iff.1 (Nat.lt_of_le_of_lt hj' hni)
   case case2 i hni hni' =>
-    rw [largestDivisor.go, dif_neg hni, if_pos hni']
     exact LargestDivisorSpec.div hi' hi hni'
   case case3 i hni hni' ih =>
-    rw [largestDivisor.go, dif_neg hni, if_neg hni']
     apply ih (by omega)
     intro j hj hij
     by_cases hij' : j = i
diff --git a/lean-toolchain b/lean-toolchain
index 78adacd..4b945b4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.20.1
+leanprover/lean4:nightly-2025-06-25

From e91c2b753cda54c5107d7e04bf6779f1ab6b1284 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Fri, 27 Jun 2025 08:36:22 +0200
Subject: [PATCH 2/3] Start shortening 24

---
 HumanEvalLean/HumanEval24.lean | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

diff --git a/HumanEvalLean/HumanEval24.lean b/HumanEvalLean/HumanEval24.lean
index 8d65073..cab7929 100644
--- a/HumanEvalLean/HumanEval24.lean
+++ b/HumanEvalLean/HumanEval24.lean
@@ -31,18 +31,12 @@ theorem largestDivisorSpec_go {n i : Nat} (hi : 2 ≤ i)
     (hi' : ∀ j, 2 ≤ j → j < i → n % j ≠ 0) : LargestDivisorSpec n (largestDivisor.go n i) := by
   fun_induction largestDivisor.go n i
   case case1 i hni =>
-    apply LargestDivisorSpec.one
-    intro j hj hj'
-    apply hi' _ hj
-    exact Nat.mul_self_lt_mul_self_iff.1 (Nat.lt_of_le_of_lt hj' hni)
+    have := @Nat.mul_self_lt_mul_self_iff i
+    grind [LargestDivisorSpec.one]
   case case2 i hni hni' =>
-    exact LargestDivisorSpec.div hi' hi hni'
+    grind [LargestDivisorSpec.div]
   case case3 i hni hni' ih =>
-    apply ih (by omega)
-    intro j hj hij
-    by_cases hij' : j = i
-    · exact hij' ▸ hni'
-    · exact hi' _ hj (by omega)
+    grind
 
 theorem largestDivisorSpec_largestDivisor {n : Nat} :
     LargestDivisorSpec n (largestDivisor n) := by

From 75a2f1f12119659625f7d8ed67bb633c76713812 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Fri, 27 Jun 2025 08:38:45 +0200
Subject: [PATCH 3/3] Fix build

---
 HumanEvalLean/HumanEval139.lean | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/HumanEvalLean/HumanEval139.lean b/HumanEvalLean/HumanEval139.lean
index e96b839..c0eebdb 100644
--- a/HumanEvalLean/HumanEval139.lean
+++ b/HumanEvalLean/HumanEval139.lean
@@ -46,8 +46,6 @@ theorem special_factorial_func_correct {n : Nat} :
   fun_induction special_factorial.go with
   | case1 fact brazil_fact curr h =>
     rw [h₂]
-    unfold special_factorial.go
-    simp [h]
     have : curr = n := by omega
     rw [this]
   | case2 fact brazilFact curr h fact' brazilFact' ih =>
@@ -55,8 +53,7 @@ theorem special_factorial_func_correct {n : Nat} :
     simp only [h₁, Nat.succ_eq_add_one, Nat.factorial_succ, h₂, Nat.brazilianFactorial_succ,
       Nat.succ_le_of_lt h, forall_const, fact', brazilFact'] at ih
     have : ¬ curr >= n := by omega
-    unfold special_factorial.go
-    simp [this, h₁, h₂, ih]
+    grind
 
 theorem test1 : special_factorial 4 = 288 := by native_decide
 theorem test2 : special_factorial 5 = 34560 := by native_decide