typo

lengyijun · Oct 13, 2024 · 8798556 · 8798556
1 parent af77bdc
commit 8798556
Showing 1 changed file with 2 additions and 28 deletions.
diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean
@@ -107,15 +107,7 @@ induction rb with intros i la lb ra l r g hm
               repeat any_goals constructor
               any_goals tauto
               . rw [← Nat.add_assoc i, g]
-                apply congr <;> try rfl
-                apply congr <;> try rfl
-                apply congr <;> try rfl
-                apply congr <;> try rfl
-                apply congr <;> try rfl
-                apply congr <;> try rfl
-                apply congr <;> try rfl
-                apply congr <;> try rfl
-                omega
+                repeat any_goals first | omega | rfl | apply congr
               . have h : ra + (rb + 1) +2 = ra + 1 + rb + 2:= by omega
                 rw [h]
                 assumption
@@ -192,25 +184,7 @@ cases lb' with (simp! [*, -nth_cfg] at g; simp_all)
               use (n + (22 + m + k + j + rb + lb' * 3 + la' * 2 + (1 + lb' + la' - 1)))
               ring_nf at *
               rw [g]
-              any_goals apply congr
-              any_goals rfl
-              any_goals apply congr
-              any_goals rfl
-              any_goals apply congr
-              any_goals rfl
-              any_goals apply congr
-              any_goals rfl
-              any_goals apply congr
-              any_goals rfl
-              any_goals apply congr
-              any_goals rfl
-              any_goals apply congr
-              any_goals rfl
-              any_goals apply congr
-              any_goals rfl
-              any_goals apply congr
-              any_goals rfl
-              omega
+              repeat any_goals first | omega | rfl | apply congr
 
 -- r1 : count of 1 on the right
 theorem lemma_23 : ∀ (i r1: ℕ) (l r : List Γ),