Shorten 139 using grind (#179)

Author: TwoFX

HumanEvalLean/HumanEval139.lean

@@ -37,20 +37,9 @@ theorem special_factorial_func_correct {n : Nat} :
     special_factorial n = n.brazilianFactorial := by
   simp [special_factorial]
   suffices ∀ (curr fact brazilFact : Nat), fact = curr ! → brazilFact = curr.brazilianFactorial →
-    curr ≤ n → special_factorial.go n fact brazilFact curr = n.brazilianFactorial by
-      apply this
-      · simp [Nat.factorial]
-      · simp [Nat.brazilianFactorial]
-      · simp
-  intro curr fact brazil_fact h₁ h₂ h₃
-  fun_induction special_factorial.go with
-  | case1 fact brazil_fact curr h =>
-    rw [h₂, (show curr = n by omega)]
-  | case2 fact brazilFact curr h fact' brazilFact' ih =>
-    simp only [ge_iff_le, Nat.not_le] at h
-    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
-    simp only [← ih, fact', h₁, brazilFact', h₂]
+      curr ≤ n → special_factorial.go n fact brazilFact curr = n.brazilianFactorial by
+    apply this <;> simp [Nat.factorial, Nat.brazilianFactorial]
+  intros; fun_induction special_factorial.go <;> grind [Nat.factorial, Nat.brazilianFactorial]
 
 theorem test1 : special_factorial 4 = 288 := by native_decide
 theorem test2 : special_factorial 5 = 34560 := by native_decide

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
+    exact LargestDivisorSpec.one (fun j hj hj' => hi' _ hj (Nat.mul_self_lt_mul_self_iff.1 (by grind)))
   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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-11
+leanprover/lean4:nightly-2025-08-18