Shorten 24 proof

Author: TwoFX

HumanEvalLean/HumanEval24.lean

@@ -57,8 +57,9 @@ theorem Nat.lt_mul_iff {a b : Nat} : a < a * b ↔ 0 < a ∧ 1 < b := by
   · simp
   · simp [ha]
 
-theorem helper {n i : Nat} (hn : 1 < n) (h : ∀ j, 2 ≤ j → j < i → n % j ≠ 0) (hi : n % i = 0)
-    (k : Nat) (hk : n / i < k) (hk₁ : k < n) : n % k ≠ 0 := by
+theorem mod_ne_zero_of_forall_of_div_lt {n i : Nat} (hn : 1 < n)
+    (h : ∀ j, 2 ≤ j → j < i → n % j ≠ 0) (hi : n % i = 0) (k : Nat) (hk : n / i < k) (hk₁ : k < n) :
+    n % k ≠ 0 := by
   intro hk₂
   obtain ⟨d, rfl⟩ := Nat.dvd_of_mod_eq_zero hk₂
   rw [Nat.lt_mul_iff] at hk₁
@@ -72,8 +73,9 @@ theorem helper {n i : Nat} (hn : 1 < n) (h : ∀ j, 2 ≤ j → j < i → n % j
   · rw [Nat.div_lt_iff_lt_mul hi₀] at hk
     exact Nat.lt_of_mul_lt_mul_left hk
 
-theorem similar_helper {n : Nat} (hn : 1 < n) (h : ∀ j, 2 ≤ j → j * j ≤ n → n % j ≠ 0)
-    (k : Nat) (hk : n < k * k) (hk₁ : k < n) : n % k ≠ 0 := by
+theorem mod_ne_zero_of_forall_of_lt_mul_self {n : Nat} (hn : 1 < n)
+    (h : ∀ j, 2 ≤ j → j * j ≤ n → n % j ≠ 0) (k : Nat) (hk : n < k * k) (hk₁ : k < n) :
+    n % k ≠ 0 := by
   intro hk₂
   obtain ⟨d, rfl⟩ := Nat.dvd_of_mod_eq_zero hk₂
   rw [Nat.lt_mul_iff] at hk₁
@@ -82,53 +84,23 @@ theorem similar_helper {n : Nat} (hn : 1 < n) (h : ∀ j, 2 ≤ j → j * j ≤
   · refine Nat.mul_le_mul_right _ (Nat.le_of_lt ?_)
     exact Nat.lt_of_mul_lt_mul_left hk
 
-theorem largestDivisorSpec_iff {n i : Nat} (hn : 1 < n) :
-    LargestDivisorSpec n i ↔ i < n ∧ n % i = 0 ∧ ∀ j, j < n → n % j = 0 → j ≤ i := by
-  constructor
-  · rintro (h|h)
-    · refine ⟨hn, Nat.mod_one _, fun j hj hj₁ => Nat.not_lt.1 (fun hj₂ => ?_)⟩
-      by_cases hj₃ : j * j ≤ n
-      · exact h j (by omega) hj₃ hj₁
-      · exact similar_helper hn h j (by omega) hj hj₁
-    · rename_i i hi hi'
-      refine ⟨?_, ?_, fun j hj hj₁ => ?_⟩
-      · apply Nat.div_lt_self <;> omega
-      · exact Nat.mod_eq_zero_of_dvd (Nat.div_dvd_of_dvd (Nat.dvd_of_mod_eq_zero hi'))
-      · exact Nat.not_lt.1 (fun hj₂ => helper hn h hi' j hj₂ hj hj₁)
-  · rintro ⟨hi₁, hi₂, hi₃⟩
-    obtain (h|rfl|h) := Nat.lt_trichotomy i 1
-    · obtain rfl : i = 0 := by omega
-      omega
-    · refine LargestDivisorSpec.one (fun j hj hj₁ hj₂ => absurd (hi₃ j ?_ hj₂) (by omega))
-      exact Nat.lt_of_lt_of_le (Nat.lt_mul_self_iff.2 (by omega)) hj₁
-    · obtain ⟨d, rfl⟩ := Nat.dvd_of_mod_eq_zero hi₂
-      have hd : 0 < d := Nat.pos_iff_ne_zero.2 (fun hd => by simp [hd] at hn)
-      rw (occs := [2]) [← Nat.mul_div_cancel (m := i) (n := d) hd]
-      refine LargestDivisorSpec.div ?_ ?_ (by simp)
-      · intro j hj₁ hj₂ hj₃
-        have : ¬ i * d / j ≤ i := by
-          rw [Nat.not_le, Nat.lt_div_iff_mul_lt_of_dvd (by omega) (Nat.dvd_of_mod_eq_zero hj₃)]
-          exact Nat.mul_lt_mul_of_pos_left hj₂ (by omega)
-        refine absurd (hi₃ _ ?_ ?_) this
-        · apply Nat.div_lt_self (by omega) (by omega)
-        · exact Nat.mod_eq_zero_of_dvd (Nat.div_dvd_of_dvd (Nat.dvd_of_mod_eq_zero hj₃))
-      · rw [Nat.lt_mul_iff] at hi₁
-        omega
-
-theorem largestDivisorSpec_unique {n i k : Nat} (hn : 1 < n)
-    (hi : LargestDivisorSpec n i) (hk : LargestDivisorSpec n k) : i = k := by
-  simp only [largestDivisorSpec_iff hn] at hi hk
-  apply Nat.le_antisymm
-  · apply hk.2.2 _ hi.1 hi.2.1
-  · apply hi.2.2 _ hk.1 hk.2.1
+theorem largestDivisorSpec.out {n i : Nat} (hn : 1 < n) :
+    LargestDivisorSpec n i → i < n ∧ n % i = 0 ∧ ∀ j, j < n → n % j = 0 → j ≤ i := by
+  rintro (h|h)
+  · refine ⟨hn, Nat.mod_one _, fun j hj hj₁ => Nat.not_lt.1 (fun hj₂ => ?_)⟩
+    by_cases hj₃ : j * j ≤ n
+    · exact h j (by omega) hj₃ hj₁
+    · exact mod_ne_zero_of_forall_of_lt_mul_self hn h j (by omega) hj hj₁
+  · rename_i i hi hi'
+    refine ⟨?_, ?_, fun j hj hj₁ => ?_⟩
+    · apply Nat.div_lt_self <;> omega
+    · exact Nat.mod_eq_zero_of_dvd (Nat.div_dvd_of_dvd (Nat.dvd_of_mod_eq_zero hi'))
+    · exact Nat.not_lt.1 (fun hj₂ => mod_ne_zero_of_forall_of_div_lt hn h hi' j hj₂ hj hj₁)
 
 theorem largestDivisor_eq_iff {n i : Nat} (hn : 1 < n) :
     largestDivisor n = i ↔ i < n ∧ n % i = 0 ∧ ∀ j, j < n → n % j = 0 → j ≤ i := by
-  rw [← largestDivisorSpec_iff hn]
-  refine ⟨?_, fun hi => ?_⟩
-  · rintro rfl
-    apply largestDivisorSpec_largestDivisor
-  · apply largestDivisorSpec_unique hn largestDivisorSpec_largestDivisor hi
+  have h := largestDivisorSpec.out hn (by exact largestDivisorSpec_largestDivisor)
+  exact ⟨fun h' => h' ▸ h, fun hi => Nat.le_antisymm (hi.2.2 _ h.1 h.2.1) (h.2.2 _ hi.1 hi.2.1)⟩
 
 /-!
 ## Prompt