diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean
index 7ed1ffc7..1c3b1df3 100644
--- a/Iris/Iris/BI/Updates.lean
+++ b/Iris/Iris/BI/Updates.lean
@@ -403,7 +403,7 @@ theorem step_fupd_mask_mono {Eo₁ Eo₂ Ei₁ Ei₂ : CoPset} {P : PROP}
 
 theorem step_fupd_mono {Eo Ei : CoPset} {P Q : PROP} :
     (Q ⊢ P) → (|={Eo}[Ei]▷=> Q) ⊢ |={Eo}[Ei]▷=> P :=
-  (BIFUpdate.mono <| later_mono <| BIFUpdate.mono ·)
+  (mono <| later_mono <| mono ·)
 
 @[rocq_alias step_fupd_intro]
 theorem step_fupd_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) :
@@ -422,8 +422,7 @@ theorem step_fupdN_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) :
     simp only [Nat.repeat]
     refine .trans (later_laterN n).1 ?_
     refine .trans (step_fupd_intro Ei_Eo) ?_
-    refine mono <| later_mono  <| mono ?_
-    exact step_fupdN_intro Ei_Eo
+    exact step_fupd_mono <| step_fupdN_intro Ei_Eo
 
 @[rocq_alias step_fupdN_le]
 theorem step_fupdN_le {n m : Nat} {Eo Ei : CoPset} {P : PROP} :
@@ -434,7 +433,7 @@ theorem step_fupdN_le {n m : Nat} {Eo Ei : CoPset} {P : PROP} :
 
 @[rocq_alias step_fupd_fupd]
 theorem step_fupd_fupd {Eo Ei : CoPset} {P : PROP} : (|={Eo}[Ei]▷=> P) ⊣⊢ (|={Eo}[Ei]▷=> |={Eo}=> P) :=
-  ⟨mono <| later_mono <| mono fupd_intro, mono <| later_mono BIFUpdate.trans⟩
+  ⟨step_fupd_mono fupd_intro, mono <| later_mono BIFUpdate.trans⟩
 
 @[rocq_alias step_fupdN_mono]
 theorem step_fupdN_mono {n : Nat} {Eo Ei : CoPset} {P Q : PROP} (H : P ⊢ Q) :
@@ -486,7 +485,7 @@ theorem step_fupdN_plain {E1 E2 : CoPset} {n : Nat} {P : PROP} [Plain P] :
   | zero => exact except0_intro.trans fupd_intro
   | succ n ih =>
     simp only [Nat.repeat]
-    refine (mono <| later_mono <| mono ih).trans ?_
+    refine (step_fupd_mono ih).trans ?_
     refine step_fupd_fupd.2.trans ?_
     refine step_fupd_plain.trans ?_
     refine (mono <| later_mono <| except0_laterN n).trans ?_