typo

lengyijun · Oct 13, 2024 · 1db5cf2 · 1db5cf2
1 parent 0a77813
commit 1db5cf2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean
@@ -250,7 +250,7 @@ induction rb with intros i lb l r g p
 | zero => use 0
           simp! [g]
 | succ rb => apply step_12_n_dvd at g
-             by_cases (lb + 2 ∣ rb + 3) <;> rename_i h
+             by_cases h : (lb + 2 ∣ rb + 3)
              . have g : (lb + 2 ∣ lb + 2) := Nat.dvd_refl _
                have g := Nat.dvd_add g h
                ring_nf at p g
@@ -366,7 +366,7 @@ nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
   Turing.ListBlank.mk (List.replicate (lb+rb+4) Γ.one ++ List.cons Γ.zero r)⟩⟩
 := by
 induction rb with intros i lb l r g hd
-| zero => by_cases (lb+2) ∣ 2 <;> rename_i h
+| zero => by_cases h : (lb+2) ∣ 2
           . apply step_12_dvd at g
             apply g h
           . obtain ⟨divisor, _, _, h₃⟩ := hd