From 1db5cf234cbc905918c1bd84446b66c9050e98b2 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sun, 13 Oct 2024 20:12:36 +0800
Subject: [PATCH] typo

---
 GoldbachTm/Tm31/Prime.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean
index 5db16ae..0809499 100644
--- 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