diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
index d1e41003a7577..da2e61956cb17 100644
--- a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
+++ b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
@@ -622,7 +622,7 @@ theorem filter_true : (π.filter fun _ => True) = π :=
 theorem iUnion_filter_not (π : Prepartition I) (p : Box ι → Prop) :
     (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion := by
   simp only [Prepartition.iUnion]
-  convert (@Set.biUnion_diff_biUnion_eq _ (Box ι) π.boxes (π.filter p).boxes (↑) _).symm
+  convert (@Set.biUnion_diff_biUnion_eq _ (Box ι) π.boxes (π.filter p).boxes Box.toSet _).symm
   · simp (config := { contextual := true })
   · rw [Set.PairwiseDisjoint]
     convert π.pairwiseDisjoint
diff --git a/Mathlib/Analysis/Convex/Segment.lean b/Mathlib/Analysis/Convex/Segment.lean
index d3b4e756dfd9d..ba856596ca1e2 100644
--- a/Mathlib/Analysis/Convex/Segment.lean
+++ b/Mathlib/Analysis/Convex/Segment.lean
@@ -337,12 +337,12 @@ theorem midpoint_mem_segment [Invertible (2 : 𝕜)] (x y : E) : midpoint 𝕜 x
 #align midpoint_mem_segment midpoint_mem_segment
 
 theorem mem_segment_sub_add [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x - y -[𝕜] x + y] := by
-  convert @midpoint_mem_segment 𝕜 _ _ _ _ _ _ _
+  convert @midpoint_mem_segment 𝕜 E _ _ _ _ _ _
   rw [midpoint_sub_add]
 #align mem_segment_sub_add mem_segment_sub_add
 
 theorem mem_segment_add_sub [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x + y -[𝕜] x - y] := by
-  convert @midpoint_mem_segment 𝕜 _ _ _ _ _ _ _
+  convert @midpoint_mem_segment 𝕜 E _ _ _ _ _ _
   rw [midpoint_add_sub]
 #align mem_segment_add_sub mem_segment_add_sub
 
diff --git a/Mathlib/CategoryTheory/Category/PartialFun.lean b/Mathlib/CategoryTheory/Category/PartialFun.lean
index 3ad583e91c562..6d90ae19a9fd3 100644
--- a/Mathlib/CategoryTheory/Category/PartialFun.lean
+++ b/Mathlib/CategoryTheory/Category/PartialFun.lean
@@ -184,6 +184,9 @@ noncomputable def typeToPartialFunIsoPartialFunToPointed :
     fun f =>
     Pointed.Hom.ext _ _ <|
       funext fun a => Option.recOn a rfl fun a => by
-        classical
-        convert Part.some_toOption _
+        simp
+        rw [← Part.get_eq_iff_mem]
+        · rfl
+        · trivial
+
 #align Type_to_PartialFun_iso_PartialFun_to_Pointed typeToPartialFunIsoPartialFunToPointed
diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean
index 4681b52cbac37..a165d53495caf 100644
--- a/Mathlib/NumberTheory/Padics/PadicVal.lean
+++ b/Mathlib/NumberTheory/Padics/PadicVal.lean
@@ -768,7 +768,7 @@ digits of `k` plus the sum of the digits of `n - k` minus the sum of digits of `
 theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits {k n : ℕ} [hp : Fact p.Prime]
     (h : k ≤ n) : (p - 1) * padicValNat p (choose n k) =
     (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum := by
-  convert @sub_one_mul_padicValNat_choose_eq_sub_sum_digits' _ _ _ _
+  convert @sub_one_mul_padicValNat_choose_eq_sub_sum_digits' p _ _ _
   all_goals exact Nat.eq_add_of_sub_eq h rfl
 
 end padicValNat