diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index c260a1b21c16ad7e56478ea94f2812a3eb3ac2a9..85ec57056d066ccacaec38523a49e6611daddd54 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -210,15 +210,15 @@ Section cmra.
       | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
   Local Definition view_pcore_eq :
-      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x)))
-    := eq_refl _.
+      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x))) :=
+    eq_refl _.
   Local Definition view_core_eq :
-      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x))
-    := eq_refl _.
+      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x)) :=
+    eq_refl _.
   Local Definition view_op_eq :
       op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y)
-                       (view_frag_proj x â‹… view_frag_proj y)
-    := eq_refl _.
+                       (view_frag_proj x â‹… view_frag_proj y) :=
+    eq_refl _.
 
   Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index f803dbd1061fce8c1b8dc19602a383dae4a27a56..d8574dee580d05bd10bb247ccc3641b6e9f70b5d 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -194,8 +194,8 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
 Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
-Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A)
-  := uPred_primitive.cmra_valid_ne.
+Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
+  uPred_primitive.cmra_valid_ne.
 
 (** Re-exporting primitive lemmas that are not in any interface *)
 Lemma ownM_op (a1 a2 : M) :
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index b9ea90171d274cf9d7428eb49bfe56a328dccae6..992fb12cb797154ff0e2fc5ab88b6542438d1e0d 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -57,8 +57,8 @@ Proof.
     rewrite /curry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Local Definition twp_def `{!irisGS_gen hlc Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
-  := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
+Local Definition twp_def `{!irisGS_gen hlc Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness :=
+  λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Local Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
 Global Arguments twp' {hlc Λ Σ _}.