diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index e76b96a91c7455d9e708e349ebae6730a9d001ca..36cdaa1b0fd29d7c41e8c611625fdd622c043afb 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -206,7 +206,8 @@ Section lemmas.
     unseal. iIntros "H1 H2".
     (* We need to explicitly specify the Inj instances instead of
     using inj _ since we need to specify [leibnizO] for [to_agree_inj]. *)
-    iCombine "H1 H2" gives %[? ?%(map_fmap_equiv_inj _ (to_agree_inj (A:=(leibnizO _))))]%gmap_view_auth_dfrac_op_valid.
+    iCombine "H1 H2" gives %[? ?%(map_fmap_equiv_inj _
+      (to_agree_inj (A:=(leibnizO _))))]%gmap_view_auth_dfrac_op_valid.
     iPureIntro. split; first done. by fold_leibniz.
   Qed.
   Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :