Bump to Lean 4.21.0 (#181)

Author: TwoFX

HumanEvalLean/HumanEval139.lean

@@ -45,18 +45,12 @@ theorem special_factorial_func_correct {n : Nat} :
   intro curr fact brazil_fact h₁ h₂ h₃
   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]
+    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
-    have : ¬ curr >= n := by omega
-    unfold special_factorial.go
-    simp [this, h₁, h₂, ih]
+    simp only [← ih, fact', h₁, brazilFact', h₂]
 
 theorem test1 : special_factorial 4 = 288 := by native_decide
 theorem test2 : special_factorial 5 = 34560 := by native_decide

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.1
+leanprover/lean4:v4.21.0