Fixup in Computability

leanprover-community · Feb 21, 2025 · eaaf1b5 · eaaf1b5
1 parent c0228d3
commit eaaf1b5
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/Mathlib/Computability/Partrec.lean b/Mathlib/Computability/Partrec.lean
@@ -296,8 +296,8 @@ theorem sumInl : Computable (@Sum.inl α β) :=
 theorem sumInr : Computable (@Sum.inr α β) :=
   Primrec.sumInr.to_comp
 
-@[deprecated (since := "2025-02-21")] alias Computable.sum_inl := Computable.sumInl
-@[deprecated (since := "2025-02-21")] alias Computable.sum_inr := Computable.sumInr
+@[deprecated (since := "2025-02-21")] alias sum_inl := Computable.sumInl
+@[deprecated (since := "2025-02-21")] alias sum_inr := Computable.sumInr
 
 theorem list_cons : Computable₂ (@List.cons α) :=
   Primrec.list_cons.to_comp
@@ -686,7 +686,7 @@ theorem sumCasesOn_right {f : α → β ⊕ γ} {g : α → β → σ} {h : α
           (some (Sum.casesOn (f a) (fun b => some (g a b)) fun _ => Option.none)) fun c =>
           (h a c).map Option.some :
         Part (Option σ)) :=
-    option_casesOn_right (g := fun a n => Part.map Option.some (h a n))
+    optionCasesOn_right (g := fun a n => Part.map Option.some (h a n))
       (sumCasesOn hf (const Option.none).to₂ (option_some.comp snd).to₂)
       (sumCasesOn (g := fun a n => Option.some (g a n)) hf (option_some.comp hg)
         (const Option.none).to₂)
@@ -699,7 +699,7 @@ theorem sumCasesOn_left {f : α → β ⊕ γ} {g : α → β →. σ} {h : α
   (sumCasesOn_right (sumCasesOn hf (sumInr.comp snd).to₂ (sumInl.comp snd).to₂) hh hg).of_eq
     fun a => by cases f a <;> simp
 
-@[deprecated (since := "2025-02-21")] alias sum_casesOn_left := sumCasesOn_left :=
+@[deprecated (since := "2025-02-21")] alias sum_casesOn_left := sumCasesOn_left
 @[deprecated (since := "2025-02-21")] alias sum_casesOn_right := sumCasesOn_right
 
 theorem fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) :

diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean
@@ -818,8 +818,8 @@ theorem sumInl : Primrec (@Sum.inl α β) :=
 theorem sumInr : Primrec (@Sum.inr α β) :=
   encode_iff.1 <| nat_double_succ.comp Primrec.encode
 
-@[deprecated (since := "2025-02-21")] alias Primrec.sum_inl := Primrec.sumInl
-@[deprecated (since := "2025-02-21")] alias Primrec.sum_inr := Primrec.sumInr
+@[deprecated (since := "2025-02-21")] alias sum_inl := Primrec.sumInl
+@[deprecated (since := "2025-02-21")] alias sum_inr := Primrec.sumInr
 
 theorem sumCasesOn {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ} (hf : Primrec f)
     (hg : Primrec₂ g) (hh : Primrec₂ h) : @Primrec _ σ _ _ fun a => Sum.casesOn (f a) (g a) (h a) :=
@@ -829,7 +829,7 @@ theorem sumCasesOn {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ
           (option_map (Primrec.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hg)).of_eq
       fun a => by rcases f a with b | c <;> simp [Nat.div2_val, encodek]
 
-@[deprecated (since := "2025-02-21")] alias Primrec.sum_casesOn := Primrec.sumCasesOn
+@[deprecated (since := "2025-02-21")] alias sum_casesOn := Primrec.sumCasesOn
 
 theorem list_cons : Primrec₂ (@List.cons α) :=
   list_cons' Primcodable.prim