DuperOnMathlib/Prime2.lean

DuperOnMathlib/DuperOnMathlib/Prime.lean

@@ -24,15 +24,16 @@ theorem prime_def_lt'_DUPER {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2
 
 #check prime_def_le_sqrt -- Reproving this theorem using duper:
 
+-- h2 times out if reduceInstances is set to false
 theorem prime_def_le_sqrt_DUPER' {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬m ∣ p := by
   constructor
   · have : ∀ m, 2 ≤ m → 1 < m := by intros; linarith
     duper [*, prime_def_lt', sqrt_lt_self, Nat.lt_of_le_of_lt]
   · intro h
     rw [prime_def_lt']
     refine ⟨h.1, ?_⟩
-    have h₂ : ∀ m, 2 ≤ m → m < p → m ∣ p → 2 ≤ (p / m) :=
-      by duper [*, Nat.lt_irrefl, Nat.dvd_iff_div_mul_eq, Nat.mul_zero, Nat.one_mul, two_le_iff]
+    have h₂ : ∀ m, 2 ≤ m → m < p → m ∣ p → 2 ≤ (p / m) := by
+      duper [*, Nat.lt_irrefl, Nat.dvd_iff_div_mul_eq, Nat.mul_zero, Nat.one_mul, two_le_iff] {portfolioInstance := 0}
     duper
       [*, Nat.div_dvd_of_dvd, Nat.dvd_iff_div_mul_eq, le_sqrt, Nat.mul_le_mul_right, Nat.mul_le_mul_left, mul_comm, Nat.le_total]
       {portfolioInstance := 0}

DuperOnMathlib/DuperOnMathlib/Prime2.lean

@@ -0,0 +1,39 @@
+import Duper.Tactic
+import Mathlib.Data.Nat.Prime
+
+set_option includeHoistRules false
+
+/- Duper can solve this theorem when `preprocessFact` in Util.Reduction.lean is disabled (set to the identity function).
+   When `preprocessFact` runs as it usually does, Duper times out when attempting to solve this theorem. Previously,
+   there were PANIC error messages caused by Duper's precCompare being incomplete, but those issues have since been resolved. -/
+theorem prime_def_lt''_new {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m) (_ : m ∣ p), m = 1 ∨ m = p := by
+  have h1 : (1 : Nat) < 2 := @one_lt_two Nat _ _ _ _ _
+  have h2 : ∀ {a b c : ℕ}, a < b → b ≤ c → a < c := @LT.lt.trans_le Nat _
+  have h3 : ∀ {a b c : ℕ}, a ≠ 0 → (a * b = a * c ↔ b = c) := @mul_right_inj' Nat _
+  have h4 : ∀ {n m : ℕ}, n < m → 0 < m:= @pos_of_gt Nat _
+  have h5 : ∀ (a b : ℕ), a ∣ a * b := @dvd_mul_right Nat _
+  have h6 : ∀ (a : ℕ), a * 1 = a := @mul_one Nat _
+  have h7 : ∀ {x y : ℕ}, x < y → y ≠ x := @LT.lt.ne' Nat _
+  have h8 : ∀ {n : ℕ}, IsUnit n ↔ n = 1 := @Nat.isUnit_iff
+  have h9 : ∀ {p : ℕ}, Nat.Prime p → 2 ≤ p := @Nat.Prime.two_le
+  have h10 : ∀ {p : ℕ}, Nat.Prime p → ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p := @Nat.Prime.eq_one_or_self_of_dvd
+  have h11 := Nat.irreducible_iff_nat_prime
+  have h12 : ∀ {p : ℕ}, Irreducible p ↔ ¬IsUnit p ∧ ∀ (a b : ℕ), p = a * b → IsUnit a ∨ IsUnit b := @irreducible_iff Nat _
+  duper [*] {portfolioInstance := 0}
+
+set_option reduceInstances false
+
+theorem prime_def_lt''_new2 {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m) (_ : m ∣ p), m = 1 ∨ m = p := by
+  have h1 : (1 : Nat) < 2 := @one_lt_two Nat _ _ _ _ _
+  have h2 : ∀ {a b c : ℕ}, a < b → b ≤ c → a < c := @LT.lt.trans_le Nat _
+  have h3 : ∀ {a b c : ℕ}, a ≠ 0 → (a * b = a * c ↔ b = c) := @mul_right_inj' Nat _
+  have h4 : ∀ {n m : ℕ}, n < m → 0 < m:= @pos_of_gt Nat _
+  have h5 : ∀ (a b : ℕ), a ∣ a * b := @dvd_mul_right Nat _
+  have h6 : ∀ (a : ℕ), a * 1 = a := @mul_one Nat _
+  have h7 : ∀ {x y : ℕ}, x < y → y ≠ x := @LT.lt.ne' Nat _
+  have h8 : ∀ {n : ℕ}, IsUnit n ↔ n = 1 := @Nat.isUnit_iff
+  have h9 : ∀ {p : ℕ}, Nat.Prime p → 2 ≤ p := @Nat.Prime.two_le
+  have h10 : ∀ {p : ℕ}, Nat.Prime p → ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p := @Nat.Prime.eq_one_or_self_of_dvd
+  have h11 := Nat.irreducible_iff_nat_prime
+  have h12 : ∀ {p : ℕ}, Irreducible p ↔ ¬IsUnit p ∧ ∀ (a b : ℕ), p = a * b → IsUnit a ∨ IsUnit b := @irreducible_iff Nat _
+  duper [*] {portfolioInstance := 0}