simpler proof

lengyijun · Oct 17, 2024 · 385794c · 385794c
1 parent 2f1139c
commit 385794c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/GoldbachTm/Tm31/PBP.lean b/GoldbachTm/Tm31/PBP.lean
@@ -284,6 +284,6 @@ induction l1 with
       ring_nf at hpp
       simp at hpp
       ring_nf
-      by_cases Nat.Prime (2+l1) <;> tauto
+      tauto
 
 end Tm31