diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 6afa47b6a194b098bbaf6ef278a60ff574cbe1c6..cfc26604ab4b4c85c82071a6fffe0e40c56d7eae 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -367,7 +367,7 @@ Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
 Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusive_l. Qed.
 Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
-Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
+Proof. destruct my as [y|]; last done. move=> /(exclusiveN_l _ x) []. Qed.
 Lemma exclusive_includedN n x `{!Exclusive x} y : x ≼{n} y → ✓{n} y → False.
 Proof. intros [? ->]. by apply exclusiveN_l. Qed.
 Lemma exclusive_included x `{!Exclusive x} y : x ≼ y → ✓ y → False.
@@ -747,7 +747,13 @@ End cmra_total.
 
 (** * Properties about morphisms *)
 Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
-Proof. split=>//=. apply _. intros. by rewrite option_fmap_id. Qed.
+Proof.
+  split => /=.
+  - apply _.
+  - done.
+  - intros. by rewrite option_fmap_id.
+  - done.
+Qed.
 Instance cmra_morphism_proper {A B : cmraT} (f : A → B) `{!CmraMorphism f} :
   Proper ((≡) ==> (≡)) f := ne_proper _.
 Instance cmra_morphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
@@ -1018,7 +1024,7 @@ Section discrete.
 
   Instance discrete_cmra_discrete :
     CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
-  Proof. split. apply _. done. Qed.
+  Proof. split; first apply _. done. Qed.
 End discrete.
 
 (** A smart constructor for the discrete RA over a carrier [A]. It uses
@@ -1192,7 +1198,7 @@ Section prod.
 
   Global Instance prod_cmra_discrete :
     CmraDiscrete A → CmraDiscrete B → CmraDiscrete prodR.
-  Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
+  Proof. split; [apply _|]. by intros ? []; split; apply cmra_discrete_valid. Qed.
 
   (* FIXME(Coq #6294): This is not an instance because we need it to use the new
   unification. *)
@@ -1425,7 +1431,7 @@ Section option.
 
   Instance option_unit : Unit (option A) := None.
   Lemma option_ucmra_mixin : UcmraMixin optionR.
-  Proof. split. done. by intros []. done. Qed.
+  Proof. split; [done|  |done]. by intros []. Qed.
   Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
 
   (** Misc *)
@@ -1456,13 +1462,13 @@ Section option.
 
   Lemma exclusiveN_Some_l n a `{!Exclusive a} mb :
     ✓{n} (Some a ⋅ mb) → mb = None.
-  Proof. destruct mb. move=> /(exclusiveN_l _ a) []. done. Qed.
+  Proof. destruct mb; last done. move=> /(exclusiveN_l _ a) []. Qed.
   Lemma exclusiveN_Some_r n a `{!Exclusive a} mb :
     ✓{n} (mb ⋅ Some a) → mb = None.
   Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
 
   Lemma exclusive_Some_l a `{!Exclusive a} mb : ✓ (Some a ⋅ mb) → mb = None.
-  Proof. destruct mb. move=> /(exclusive_l a) []. done. Qed.
+  Proof. destruct mb; last done. move=> /(exclusive_l a) []. Qed.
   Lemma exclusive_Some_r a `{!Exclusive a} mb : ✓ (mb ⋅ Some a) → mb = None.
   Proof. rewrite comm. by apply exclusive_Some_l. Qed.
 
@@ -1474,9 +1480,9 @@ Section option.
   Proof. rewrite Some_included; eauto. Qed.
 
   Lemma Some_includedN_total `{CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
-  Proof. rewrite Some_includedN. split. by intros [->|?]. eauto. Qed.
+  Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.
   Lemma Some_included_total `{CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
-  Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed.
+  Proof. rewrite Some_included. split; [|by eauto]. by intros [->|?]. Qed.
 
   Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
     Some a ≼{n} Some b → ✓{n} b → a ≡{n}≡ b.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index edce5cb70dfb3ac99db7c5ee89b4de6bfbc15c70..37ae379318e422f97c87ec8f9d3a80c99c40958b 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -8,7 +8,7 @@ Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l :
 Proof.
   revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
   - intros [??] [|k] y ?; naive_solver.
-  - intros Hl. split. by apply (Hl 0). intros k. apply (Hl (S k)).
+  - intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
 Qed.
 Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K → A → option M) m :
   ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 2cff617b22b1e5c94cde5e377f3e7753a4a38d7f..dcd07527b2f44ed3006152d757a4ee7d56e42a71 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -43,7 +43,7 @@ Section coPset.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Lemma coPset_ucmra_mixin : UcmraMixin coPset.
-  Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed.
+  Proof. split; [done | | done]. intros X. by rewrite coPset_op_union left_id_L. Qed.
   Canonical Structure coPsetUR := UcmraT coPset coPset_ucmra_mixin.
 
   Lemma coPset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
@@ -56,7 +56,7 @@ Section coPset.
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
     rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split. done. rewrite coPset_op_union. set_solver.
+    split; first done. rewrite coPset_op_union. set_solver.
   Qed.
 End coPset.
 
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index c418dd97b75798e7000ff57b063bc3212ca12807..74d83490b6859d6b14a4121efc8b4b15c4ce8b55 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -349,7 +349,7 @@ Proof.
   intros Hup n mf ? Ha1; simpl in *.
   destruct (Hup n (mf ≫= maybe Cinl)); auto.
   { by destruct mf as [[]|]; inversion_clear Ha1. }
-  split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
+  split; first done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
 Qed.
 Lemma csum_local_update_r (b1 b2 b1' b2' : B) :
   (b1,b2) ~l~> (b1',b2') → (Cinr b1,Cinr b2) ~l~> (Cinr b1',Cinr b2').
@@ -357,7 +357,7 @@ Proof.
   intros Hup n mf ? Ha1; simpl in *.
   destruct (Hup n (mf ≫= maybe Cinr)); auto.
   { by destruct mf as [[]|]; inversion_clear Ha1. }
-  split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
+  split; first done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
 Qed.
 End cmra.
 
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 6fcb9e9bd257463eb7ec7d850bf4f0c9721e9109..10a86de7442ae024fcf1dd7d1d2fc065a8cfb339 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -82,7 +82,7 @@ Proof.
   split; try discriminate.
   - by intros n []; destruct 1; constructor.
   - by destruct 1; intros ?.
-  - intros x; split. done. by move=> /(_ 0).
+  - intros x; split; [done|]. by move=> /(_ 0).
   - intros n [?|]; simpl; auto with lia.
   - by intros [?|] [?|] [?|]; constructor.
   - by intros [?|] [?|]; constructor.
@@ -92,7 +92,7 @@ Qed.
 Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin.
 
 Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
-Proof. split. apply _. by intros []. Qed.
+Proof. split; first apply _. by intros []. Qed.
 
 (** Exclusive *)
 Global Instance excl_exclusive x : Exclusive x.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index 1d7353182eea738249eefc391e8a52eebd9bfb69..dd40746ecac32593d192a3c366397d8e08ac4363 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -62,7 +62,10 @@ Section cmra.
 
   Global Instance discrete_fun_singleton_ne x :
     NonExpansive (discrete_fun_singleton x : B x → _).
-  Proof. intros n y1 y2 ?; apply discrete_fun_insert_ne. done. by apply equiv_dist. Qed.
+  Proof.
+    intros n y1 y2 ?; apply discrete_fun_insert_ne; [done|].
+    by apply equiv_dist.
+  Qed.
   Global Instance discrete_fun_singleton_proper x :
     Proper ((≡) ==> (≡)) (discrete_fun_singleton x) := ne_proper _.
 
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index ed15a0559722da3c6c6608a769379748a2bd1870..cab92a41893b2db2c49468383d6ef8125a499a6f 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -243,7 +243,11 @@ Implicit Types x y : A.
 
 Global Instance lookup_op_homomorphism i :
   MonoidHomomorphism op op (≡) (lookup i : gmap K A → option A).
-Proof. split; [split|]; try apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
+Proof.
+  split; [split|]; try apply _.
+  - intros m1 m2; by rewrite lookup_op.
+  - done.
+Qed.
 
 Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (.!! i)).
 Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
@@ -261,7 +265,7 @@ Lemma singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x.
 Proof.
   split.
   - move=>/(_ i); by simplify_map_eq.
-  - intros. apply insert_validN. done. apply: ucmra_unit_validN.
+  - intros. apply insert_validN; first done. apply: ucmra_unit_validN.
 Qed.
 Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
 Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
@@ -311,7 +315,7 @@ Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hi.
     exists (x â‹…? m' !! i). rewrite -Some_op_opM.
-    split. done. apply cmra_includedN_l.
+    split; first done. apply cmra_includedN_l.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
@@ -324,7 +328,7 @@ Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
     exists (x â‹…? m' !! i). rewrite -Some_op_opM.
-    split. done. apply cmra_included_l.
+    split; first done. apply cmra_included_l.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 701bb9d5a942f4988efadbe285640dc88c138d3a..822a952e3156f2659266ee6fc354f9213db9bebc 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -47,7 +47,10 @@ Section gmultiset.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
-  Proof. split. done. intros X. by rewrite gmultiset_op_disj_union left_id_L. done. Qed.
+  Proof.
+    split; [done | | done]. intros X.
+    by rewrite gmultiset_op_disj_union left_id_L.
+  Qed.
   Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.
 
   Global Instance gmultiset_cancelable X : Cancelable X.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index b3a5d578c42c8fef3286ea5bde298c442df02394..5283498c8da39193a9db51426608c4decafc0c76 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -37,7 +37,7 @@ Section gset.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Lemma gset_ucmra_mixin : UcmraMixin (gset K).
-  Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
+  Proof. split; [ done | | done ]. intros X. by rewrite gset_op_union left_id_L. Qed.
   Canonical Structure gsetUR := UcmraT (gset K) gset_ucmra_mixin.
 
   Lemma gset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
@@ -50,7 +50,7 @@ Section gset.
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
     rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split. done. rewrite gset_op_union. set_solver.
+    split; [done|]. rewrite gset_op_union. set_solver.
   Qed.
 
   Global Instance gset_core_id X : CoreId X.
@@ -164,7 +164,7 @@ Section gset_disj.
       (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
     Proof.
       intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
-      intros Y ?; exists (fresh Y). split. apply is_fresh. done.
+      intros Y ?; exists (fresh Y). split; [|done]. apply is_fresh.
     Qed.
     Lemma gset_disj_alloc_updateP' X :
       GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index d9a1f62fb929b9001b430edaecda2019194c8d21..6174a3e54c5c1ad608982618833e20677d57251a 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -78,7 +78,8 @@ Section frac_auth.
   Lemma frac_auth_auth_validN n a : ✓{n} (●F a) ↔ ✓{n} a.
   Proof.
     rewrite auth_auth_frac_validN Some_validN. split.
-    by intros [?[]]. intros. by split.
+    - by intros [?[]].
+    - intros. by split.
   Qed.
   Lemma frac_auth_auth_valid a : ✓ (●F a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index e2ab06b4e8595e9cfc40b93629b561b294358b10..1f5705f2de9510459d5fbb908a93a2755bf8205c 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -96,15 +96,24 @@ Section ufrac_auth.
   Lemma ufrac_auth_auth_validN n q a : ✓{n} (●U{q} a) ↔ ✓{n} a.
   Proof.
     rewrite auth_auth_frac_validN Some_validN. split.
-    by intros [?[]]. intros. by split.
+    - by intros [?[]].
+    - intros. by split.
   Qed.
   Lemma ufrac_auth_auth_valid q a : ✓ (●U{q} a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite ufrac_auth_auth_validN. Qed.
 
   Lemma ufrac_auth_frag_validN n q a : ✓{n} (◯U{q} a) ↔ ✓{n} a.
-  Proof. rewrite auth_frag_validN. split. by intros [??]. by split. Qed.
+  Proof.
+    rewrite auth_frag_validN. split.
+    - by intros [??].
+    - by split.
+  Qed.
   Lemma ufrac_auth_frag_valid q a : ✓ (◯U{q} a) ↔ ✓ a.
-  Proof. rewrite auth_frag_valid. split. by intros [??]. by split. Qed.
+  Proof.
+    rewrite auth_frag_valid. split.
+    - by intros [??].
+    - by split.
+  Qed.
 
   Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U{q1+q2} (a1 ⋅ a2) ≡ ◯U{q1} a1 ⋅ ◯U{q2} a2.
   Proof. done. Qed.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 7a02bd42db701a5bcea62b77de7ec4b05cab814e..92110f0b247e3b0148168f8ead8dc82b749816e8 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -187,5 +187,5 @@ Proof.
   move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
   destruct z as [z|]; last done. exfalso.
   move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
-  eapply cmra_validN_le. eapply Hy. lia.
+  eapply cmra_validN_le; [|lia]. eapply Hy.
 Qed.
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index ab55d9545b8570f2269dd1ea2b166d6de37239c8..98656d914caea33b580950fea4813d15a710ead9 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -170,7 +170,9 @@ Proof.
     intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.
     intros i. move: (Hdisj i). rewrite lookup_op.
     case: (m1 !! i)=> [a|]; last auto.
-    move=> []. by case: (m2 !! i). set_solver.
+    move=> [].
+    { by case: (m2 !! i). }
+    set_solver.
   - intros n x y1 y2 ? [??]; simpl in *.
     destruct (cmra_extend n (namespace_map_data_proj x)
       (namespace_map_data_proj y1) (namespace_map_data_proj y2))
@@ -195,7 +197,7 @@ Instance namespace_map_empty : Unit (namespace_map A) := NamespaceMap ε ε.
 Lemma namespace_map_ucmra_mixin : UcmraMixin (namespace_map A).
 Proof.
   split; simpl.
-  - rewrite namespace_map_valid_eq /=. split. apply ucmra_unit_valid. set_solver.
+  - rewrite namespace_map_valid_eq /=. split; [apply ucmra_unit_valid|]. set_solver.
   - split; simpl; [by rewrite left_id|by rewrite left_id_L].
   - do 2 constructor; [apply (core_id_core _)|done].
 Qed.
@@ -209,7 +211,7 @@ Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
 Lemma namespace_map_data_valid N a : ✓ (namespace_map_data N a) ↔ ✓ a.
 Proof. rewrite namespace_map_valid_eq /= singleton_valid. set_solver. Qed.
 Lemma namespace_map_token_valid E : ✓ (namespace_map_token E).
-Proof. rewrite namespace_map_valid_eq /=. split. done. by left. Qed.
+Proof. rewrite namespace_map_valid_eq /=. split; first done. by left. Qed.
 Lemma namespace_map_data_op N a b :
   namespace_map_data N (a â‹… b) = namespace_map_data N a â‹… namespace_map_data N b.
 Proof.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 55c1b3af1f2d0dcdd681a1af0154766eba8c3b4d..0b0963f54a6172a35c875a23c9fb08336323d53f 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -203,7 +203,7 @@ Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
 Arguments dist_later _ _ !_ _ _ /.
 
 Global Instance dist_later_equivalence (A : ofeT) n : Equivalence (@dist_later A _ n).
-Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.
+Proof. destruct n as [|n]; [by split|]. apply dist_equivalence. Qed.
 
 Lemma dist_dist_later {A : ofeT} n (x y : A) : dist n x y → dist_later n x y.
 Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.
@@ -279,7 +279,12 @@ Section limit_preserving.
   Lemma limit_preserving_and (P1 P2 : A → Prop) :
     LimitPreserving P1 → LimitPreserving P2 →
     LimitPreserving (λ x, P1 x ∧ P2 x).
-  Proof. intros Hlim1 Hlim2 c Hc. split. apply Hlim1, Hc. apply Hlim2, Hc. Qed.
+  Proof.
+    intros Hlim1 Hlim2 c Hc.
+    split.
+    - apply Hlim1, Hc.
+    - apply Hlim2, Hc.
+  Qed.
 
   Lemma limit_preserving_impl (P1 P2 : A → Prop) :
     Proper (dist 0 ==> impl) P1 → LimitPreserving P2 →
@@ -662,8 +667,9 @@ Section product.
   Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodO :=
     { compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
   Next Obligation.
-    intros ?? n c; split. apply (conv_compl n (chain_map fst c)).
-    apply (conv_compl n (chain_map snd c)).
+    intros ?? n c; split.
+    - apply (conv_compl n (chain_map fst c)).
+    - apply (conv_compl n (chain_map snd c)).
   Qed.
 
   Global Instance prod_discrete (x : A * B) :
@@ -1096,7 +1102,9 @@ Section later.
   Proof.
     split.
     - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
-      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
+      split.
+      + intros Hxy [|n]; [done|apply Hxy].
+      + intros Hxy n; apply (Hxy (S n)).
     - split; rewrite /dist /later_dist.
       + by intros [x].
       + by intros [x] [y].
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 29682927c857afd3ee4f7c6a12fb1b6cba246666..fae53edbd92b431d35084883bf06c501242b3ad4 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -319,7 +319,9 @@ Lemma sts_frag_up_valid s T : ✓ sts_frag_up s T ↔ tok s ## T.
 Proof.
   split.
   - move=>/sts_frag_valid [H _]. apply H, elem_of_up.
-  - intros. apply sts_frag_valid; split. by apply closed_up. set_solver.
+  - intros. apply sts_frag_valid; split.
+    + by apply closed_up.
+    + set_solver+.
 Qed.
 
 Lemma sts_auth_frag_valid_inv s S T1 T2 :
@@ -377,8 +379,12 @@ Proof.
   rewrite /sts_frag=> HC HS HT. apply validity_update.
   inversion 3 as [|? S ? Tf|]; simplify_eq/=;
     (destruct HC as (? & ? & ?); first by destruct_and?).
-  - split_and!. done. set_solver. constructor; set_solver.
-  - split_and!. done. set_solver. constructor; set_solver.
+  - split_and!; first done.
+    + set_solver.
+    + constructor; set_solver.
+  - split_and!; first done.
+    + set_solver.
+    + constructor; set_solver.
 Qed.
 
 Lemma sts_update_frag_up s1 S2 T1 T2 :
@@ -393,7 +399,9 @@ Lemma sts_up_set_intersection S1 Sf Tf :
   closed Sf Tf → S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.
 Proof.
   intros Hclf. apply (anti_symm (⊆)).
-  - move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
+  - move=>s [HS1 HSf]. split.
+    + by apply HS1.
+    + by apply subseteq_up_set.
   - move=>s [HS1 [s' [/elem_of_PropSet Hsup Hs']]]. split; first done.
     eapply closed_steps, Hsup; first done. set_solver +Hs'.
 Qed.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 411f1f2b7db866a2560634a2fa42c5fc7088b385..d98af92a11b071cec7dc9ea6667493fd2c93cd50 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -89,7 +89,9 @@ Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
 Proof.
   intros H n mz Hmz. apply H, Hmz.
   apply (cmra_validN_le n); last lia.
-  destruct mz. eapply cmra_validN_op_l, Hmz. apply Hmz.
+  destruct mz.
+  - eapply cmra_validN_op_l, Hmz.
+  - apply Hmz.
 Qed.
 
 (** ** Frame preserving updates for total CMRAs *)
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index dd904042e1b9c7bd2911d6c18e36b129f8c087fa..17f964f61304f4d6e7d49731cab1c51e2c4de4e7 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -27,7 +27,9 @@ Section ofe.
     Discrete x → Discrete v → Discrete (x ::: v).
   Proof.
     intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1.
-    constructor. by apply discrete. change (v ≡ v'). by apply discrete.
+    constructor.
+    - by apply discrete.
+    - change (v ≡ v'). by apply discrete.
   Qed.
   Global Instance vec_ofe_discrete m : OfeDiscrete A → OfeDiscrete (vecO m).
   Proof. intros ? v. induction v; apply _. Qed.
diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index 51a5c1673f50d325f940cd7836ed2cc70624746b..c8d95b720b45de331dfc01ee1c6523b666b6ea05 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -78,7 +78,9 @@ Section excl.
                         | _, _ => False
                         end.
   Proof.
-    uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
+    uPred.unseal. do 2 split.
+    - by destruct 1.
+    - by destruct x, y; try constructor.
   Qed.
   Lemma excl_validI x :
     ✓ x ⊣⊢ if x is ExclBot then False else True.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 3bcb256e3c37a2320ba33ff02897bed909320a86..091da0fedc4f885e741a91cbb37a6dc43b7e4c24 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -82,7 +82,7 @@ Qed.
 (** For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
-Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
+Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
 
 (** Consistency/soundness statement *)
 Lemma bupd_plain_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 8b443a61b35095e79a23e1f4f81ee662e8a5a329..3db95759cafbaaa29c9e4d8ee8259fbdbaa35ad4 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -142,8 +142,9 @@ Section cofe.
     {| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'} x → c n' n' x |}.
   Next Obligation.
     move=> /= c n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv. eapply uPred_mono.
-    eapply HP, cmra_validN_includedN, cmra_includedN_le=>//; lia.
-    eapply cmra_includedN_le=>//; lia. done.
+    - eapply HP, cmra_validN_includedN, cmra_includedN_le=>//; lia.
+    - eapply cmra_includedN_le=>//; lia.
+    - done.
   Qed.
   Global Program Instance uPred_cofe : Cofe uPredO := {| compl := uPred_compl |}.
   Next Obligation.
@@ -592,7 +593,11 @@ Proof. unseal; split=> n x ??; left; auto. Qed.
 Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
 Proof. unseal; split=> n x ??; right; auto. Qed.
 Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
-Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
+Proof.
+  intros HP HQ; unseal; split=> n x ? [?|?].
+  - by apply HP.
+  - by apply HQ.
+Qed.
 
 Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
 Proof.
@@ -820,7 +825,9 @@ Lemma ownM_op (a1 a2 : M) :
 Proof.
   unseal; split=> n x ?; split.
   - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
-    split. by exists (core a1); rewrite cmra_core_r. by exists z.
+    split.
+    + by exists (core a1); rewrite cmra_core_r.
+    + by exists z.
   - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
     by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
       -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 99a6783b752a99786230e770ced8e41b78d35f6f..d5fd0ae0c74431d58f633a86a492346946044a3a 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -321,7 +321,11 @@ Proof.
 Qed.
 
 Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q).
-Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed.
+Proof.
+  split.
+  - intros ->; auto.
+  - intros; apply (anti_symm _); auto.
+Qed.
 
 Global Instance iff_ne : NonExpansive2 (@bi_iff PROP).
 Proof. unfold bi_iff; solve_proper. Qed.
@@ -1002,7 +1006,9 @@ Section persistently_affine_bi.
 
   Lemma impl_wand_persistently P Q : (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q).
   Proof.
-    apply (anti_symm (⊢)). by rewrite -impl_wand_1. apply impl_wand_persistently_2.
+    apply (anti_symm (⊢)).
+    - by rewrite -impl_wand_1.
+    - apply impl_wand_persistently_2.
   Qed.
 
   Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ <pers> (P ∗ R → Q).
@@ -1552,30 +1558,34 @@ Global Instance bi_sep_monoid : Monoid (@bi_sep PROP) :=
 Global Instance bi_persistently_and_homomorphism :
   MonoidHomomorphism bi_and bi_and (≡) (@bi_persistently PROP).
 Proof.
-  split; [split|]; try apply _. apply persistently_and. apply persistently_pure.
+  split; [split|]; try apply _.
+  - apply persistently_and.
+  - apply persistently_pure.
 Qed.
 
 Global Instance bi_persistently_or_homomorphism :
   MonoidHomomorphism bi_or bi_or (≡) (@bi_persistently PROP).
 Proof.
-  split; [split|]; try apply _. apply persistently_or. apply persistently_pure.
+  split; [split|]; try apply _.
+  - apply persistently_or.
+  - apply persistently_pure.
 Qed.
 
 Global Instance bi_persistently_sep_weak_homomorphism `{BiPositive PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
-Proof. split; try apply _. apply persistently_sep. Qed.
+Proof. split; [by apply _ ..|]. apply persistently_sep. Qed.
 
 Global Instance bi_persistently_sep_homomorphism `{BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
-Proof. split. apply _. apply persistently_emp. Qed.
+Proof. split; [by apply _ ..|]. apply persistently_emp. Qed.
 
 Global Instance bi_persistently_sep_entails_weak_homomorphism :
   WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
-Proof. split; try apply _. intros P Q; by rewrite persistently_sep_2. Qed.
+Proof. split; [by apply _ ..|]. intros P Q; by rewrite persistently_sep_2. Qed.
 
 Global Instance bi_persistently_sep_entails_homomorphism :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
-Proof. split. apply _. simpl. apply persistently_emp_intro. Qed.
+Proof. split; [by apply _ ..|]. simpl. apply persistently_emp_intro. Qed.
 
 (* Limits *)
 Lemma limit_preserving_entails {A : ofeT} `{Cofe A} (Φ Ψ : A → PROP) :
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index a683467de724d154d0e9fc20e20c22eba4df1cec..1af9dd81e8fb0dbcf9edb8b867791d29cbb8f195 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -118,7 +118,7 @@ Proof.
 Qed.
 
 Lemma löb_alt_strong : BiLöb PROP ↔ ∀ P, (▷ P → P) ⊢ P.
-Proof. split; intros HLöb P. apply löb. by intros ->%entails_impl_True. Qed.
+Proof. split; intros HLöb P; [by apply löb|]. by intros ->%entails_impl_True. Qed.
 
 (** Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
 Their [Ψ] is called [Q] in our proof. *)
@@ -173,7 +173,7 @@ Proof. apply entails_impl, löb. Qed.
 
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@bi_laterN PROP m).
-Proof. induction m; simpl. by intros ???. solve_proper. Qed.
+Proof. induction m; simpl; [by intros ???|]. solve_proper. Qed.
 Global Instance laterN_proper m :
   Proper ((⊣⊢) ==> (⊣⊢)) (@bi_laterN PROP m) := ne_proper _.
 
@@ -405,13 +405,25 @@ Proof. destruct mx; apply _. Qed.
 (* Big op stuff *)
 Global Instance bi_later_monoid_and_homomorphism :
   MonoidHomomorphism bi_and bi_and (≡) (@bi_later PROP).
-Proof. split; [split|]; try apply _. apply later_and. apply later_True. Qed.
+Proof.
+  split; [split|]; try apply _.
+  - apply later_and.
+  - apply later_True.
+Qed.
 Global Instance bi_laterN_and_homomorphism n :
   MonoidHomomorphism bi_and bi_and (≡) (@bi_laterN PROP n).
-Proof. split; [split|]; try apply _. apply laterN_and. apply laterN_True. Qed.
+Proof.
+  split; [split|]; try apply _.
+  - apply laterN_and.
+  - apply laterN_True.
+Qed.
 Global Instance bi_except_0_and_homomorphism :
   MonoidHomomorphism bi_and bi_and (≡) (@bi_except_0 PROP).
-Proof. split; [split|]; try apply _. apply except_0_and. apply except_0_True. Qed.
+Proof.
+  split; [split|]; try apply _.
+  - apply except_0_and.
+  - apply except_0_True.
+Qed.
 
 Global Instance bi_later_monoid_or_homomorphism :
   WeakMonoidHomomorphism bi_or bi_or (≡) (@bi_later PROP).
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 3ffb1d71f4332e5eba60fdfde98813cf1226f948..df3f1a817bf9c7e06877cd697d1e0f2ff771d10a 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -151,7 +151,11 @@ Proof.
 Qed.
 
 Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
-Proof. apply (anti_symm _). apply sig_equivI_1. apply f_equivI, _. Qed.
+Proof.
+  apply (anti_symm _).
+  - apply sig_equivI_1.
+  - apply f_equivI, _.
+Qed.
 
 Section sigT_equivI.
 Import EqNotations.
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index ead88c5ca4ee8d4ada3008774de4f0b5706c01de..4d4b9ffa5f0661a6a677aea8257d9b4a2d2c78f5 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -117,14 +117,14 @@ Section fractional.
   Instance mul_as_fractional_l P Φ p q :
     AsFractional P Φ (q * p) → AsFractional P (λ q, Φ (q * p)%Qp) q.
   Proof.
-    intros H. split. apply H. eapply (mul_fractional_l _ Φ p).
-    split. done. apply H.
+    intros H. split; first apply H. eapply (mul_fractional_l _ Φ p).
+    split; first done. apply H.
   Qed.
   Instance mul_as_fractional_r P Φ p q :
     AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) q.
   Proof.
-    intros H. split. apply H. eapply (mul_fractional_r _ Φ p).
-    split. done. apply H.
+    intros H. split; first apply H. eapply (mul_fractional_r _ Φ p).
+    split; first done. apply H.
   Qed.
 
   (** Proof mode instances *)
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index f5f9e780c0cb9687d27ab912a4124b8cae72fcc3..f2bb21e9a3f0d255a31d0ab44790c21675dbce3d 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -309,8 +309,9 @@ Proof.
   - intros P Q. split=> i. by apply bi.later_sep_2.
   - intros P. split=> i. by apply bi.later_persistently_1.
   - intros P. split=> i. by apply bi.later_persistently_2.
-  - intros P. split=> i /=. rewrite -bi.forall_intro. apply bi.later_false_em.
-    intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij. by rewrite Hij.
+  - intros P. split=> i /=. rewrite -bi.forall_intro.
+    + apply bi.later_false_em.
+    + intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij. by rewrite Hij.
 Qed.
 
 Canonical Structure monPredI : bi :=
@@ -519,14 +520,20 @@ Qed.
 Lemma monPred_objectively_and P Q : <obj> (P ∧ Q) ⊣⊢ <obj> P ∧ <obj> Q.
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=.
-  - apply bi.and_intro; do 2 f_equiv. apply bi.and_elim_l. apply bi.and_elim_r.
+  - apply bi.and_intro; do 2 f_equiv.
+    + apply bi.and_elim_l.
+    + apply bi.and_elim_r.
   - apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
 Qed.
 Lemma monPred_objectively_exist {A} (Φ : A → monPred) :
   (∃ x, <obj> (Φ x)) ⊢ <obj> (∃ x, (Φ x)).
 Proof. apply bi.exist_elim=>?. f_equiv. apply bi.exist_intro. Qed.
 Lemma monPred_objectively_or P Q : <obj> P ∨ <obj> Q ⊢ <obj> (P ∨ Q).
-Proof. apply bi.or_elim; f_equiv. apply bi.or_intro_l. apply bi.or_intro_r. Qed.
+Proof.
+  apply bi.or_elim; f_equiv.
+  - apply bi.or_intro_l.
+  - apply bi.or_intro_r.
+Qed.
 
 Lemma monPred_objectively_sep_2 P Q : <obj> P ∗ <obj> Q ⊢ <obj> (P ∗ Q).
 Proof. unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim. Qed.
@@ -538,7 +545,8 @@ Qed.
 Lemma monPred_objectively_embed (P : PROP) : <obj> ⎡P⎤ ⊣⊢ ⎡P⎤.
 Proof.
   apply bi.equiv_spec; split; unseal; split=>i /=.
-  by rewrite (bi.forall_elim inhabitant). by apply bi.forall_intro.
+  - by rewrite (bi.forall_elim inhabitant).
+  - by apply bi.forall_intro.
 Qed.
 Lemma monPred_objectively_emp : <obj> (emp : monPred) ⊣⊢ emp.
 Proof. rewrite monPred_emp_unfold. apply monPred_objectively_embed. Qed.
@@ -552,7 +560,11 @@ Lemma monPred_subjectively_forall {A} (Φ : A → monPred) :
   (<subj> (∀ x, Φ x)) ⊢ ∀ x, <subj> (Φ x).
 Proof. apply bi.forall_intro=>?. f_equiv. apply bi.forall_elim. Qed.
 Lemma monPred_subjectively_and P Q : <subj> (P ∧ Q) ⊢ <subj> P ∧ <subj> Q.
-Proof. apply bi.and_intro; f_equiv. apply bi.and_elim_l. apply bi.and_elim_r. Qed.
+Proof.
+  apply bi.and_intro; f_equiv.
+  - apply bi.and_elim_l.
+  - apply bi.and_elim_r.
+Qed.
 Lemma monPred_subjectively_exist {A} (Φ : A → monPred) : <subj> (∃ x, Φ x) ⊣⊢ ∃ x, <subj> (Φ x).
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=;
@@ -562,7 +574,9 @@ Lemma monPred_subjectively_or P Q : <subj> (P ∨ Q) ⊣⊢ <subj> P ∨ <subj>
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=.
   - apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
-  - apply bi.or_elim; do 2 f_equiv. apply bi.or_intro_l. apply bi.or_intro_r.
+  - apply bi.or_elim; do 2 f_equiv.
+    + apply bi.or_intro_l.
+    + apply bi.or_intro_r.
 Qed.
 
 Lemma monPred_subjectively_sep P Q : <subj> (P ∗ Q) ⊢ <subj> P ∗ <subj> Q.
@@ -656,13 +670,13 @@ Qed.
 (** Big op *)
 Global Instance monPred_at_monoid_and_homomorphism i :
   MonoidHomomorphism bi_and bi_and (≡) (flip monPred_at i).
-Proof. split; [split|]; try apply _. apply monPred_at_and. apply monPred_at_pure. Qed.
+Proof. split; [split|]; try apply _; [apply monPred_at_and | apply monPred_at_pure]. Qed.
 Global Instance monPred_at_monoid_or_homomorphism i :
   MonoidHomomorphism bi_or bi_or (≡) (flip monPred_at i).
-Proof. split; [split|]; try apply _. apply monPred_at_or. apply monPred_at_pure. Qed.
+Proof. split; [split|]; try apply _; [apply monPred_at_or | apply monPred_at_pure]. Qed.
 Global Instance monPred_at_monoid_sep_homomorphism i :
   MonoidHomomorphism bi_sep bi_sep (≡) (flip monPred_at i).
-Proof. split; [split|]; try apply _. apply monPred_at_sep. apply monPred_at_emp. Qed.
+Proof. split; [split|]; try apply _; [apply monPred_at_sep | apply monPred_at_emp]. Qed.
 
 Lemma monPred_at_big_sepL {A} i (Φ : nat → A → monPred) l :
   ([∗ list] k↦x ∈ l, Φ k x) i ⊣⊢ [∗ list] k↦x ∈ l, Φ k x i.
@@ -680,20 +694,23 @@ Proof. apply (big_opMS_commute (flip monPred_at i)). Qed.
 Global Instance monPred_objectively_monoid_and_homomorphism :
   MonoidHomomorphism bi_and bi_and (≡) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_objectively_and.
-  apply monPred_objectively_pure.
+  split; [split|]; try apply _.
+  - apply monPred_objectively_and.
+  - apply monPred_objectively_pure.
 Qed.
 Global Instance monPred_objectively_monoid_sep_entails_homomorphism :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_objectively_sep_2.
-  by rewrite monPred_objectively_emp.
+  split; [split|]; try apply _.
+  - apply monPred_objectively_sep_2.
+  - by rewrite monPred_objectively_emp.
 Qed.
 Global Instance monPred_objectively_monoid_sep_homomorphism `{BiIndexBottom bot} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_objectively_sep.
-  by rewrite monPred_objectively_emp.
+  split; [split|]; try apply _.
+  - apply monPred_objectively_sep.
+  - by rewrite monPred_objectively_emp.
 Qed.
 
 Lemma monPred_objectively_big_sepL_entails {A} (Φ : nat → A → monPred) l :
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 756dba593fd955d1b4067b4da66f758d15af765c..7a8646f184447f1c6317d8e9b61e414442248f4f 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -301,7 +301,9 @@ Section plainly_affine_bi.
 
   Lemma impl_wand_plainly P Q : (■ P → Q) ⊣⊢ (■ P -∗ Q).
   Proof.
-    apply (anti_symm (⊢)). by rewrite -impl_wand_1. by rewrite impl_wand_plainly_2.
+    apply (anti_symm (⊢)).
+    - by rewrite -impl_wand_1.
+    - by rewrite impl_wand_plainly_2.
   Qed.
 End plainly_affine_bi.
 
@@ -393,17 +395,17 @@ Global Instance plainly_sep_entails_weak_homomorphism :
 Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed.
 Global Instance plainly_sep_entails_homomorphism `{!BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
-Proof. split. apply _. simpl. rewrite plainly_emp. done. Qed.
+Proof. split; try apply _. simpl. rewrite plainly_emp. done. Qed.
 
 Global Instance plainly_sep_homomorphism `{BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
-Proof. split. apply _. apply plainly_emp. Qed.
+Proof. split; try apply _. apply plainly_emp. Qed.
 Global Instance plainly_and_homomorphism :
   MonoidHomomorphism bi_and bi_and (≡) (@plainly PROP _).
-Proof. split; [split|]; try apply _. apply plainly_and. apply plainly_pure. Qed.
+Proof. split; [split|]; try apply _; [apply plainly_and | apply plainly_pure]. Qed.
 Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} :
   MonoidHomomorphism bi_or bi_or (≡) (@plainly PROP _).
-Proof. split; [split|]; try apply _. apply plainly_or. apply plainly_pure. Qed.
+Proof. split; [split|]; try apply _; [apply plainly_or | apply plainly_pure]. Qed.
 
 Lemma big_sepL_plainly `{!BiAffine PROP} {A} (Φ : nat → A → PROP) l :
   ■ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, ■ (Φ k x).
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index c3f4c1cd646726ef8f95490907f1ac40b9d8f4c3..0674386abc4d2714d604fbd9c6128a51d077baf9 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -187,7 +187,7 @@ Section bupd_derived.
 
   Global Instance bupd_homomorphism :
     MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (bupd (PROP:=PROP)).
-  Proof. split; [split|]; try apply _. apply bupd_sep. apply bupd_intro. Qed.
+  Proof. split; [split|]; try apply _; [apply bupd_sep | apply bupd_intro]. Qed.
 
   Lemma big_sepL_bupd {A} (Φ : nat → A → PROP) l :
     ([∗ list] k↦x ∈ l, |==> Φ k x) ⊢ |==> [∗ list] k↦x ∈ l, Φ k x.
@@ -327,7 +327,7 @@ Section fupd_derived.
 
   Global Instance fupd_homomorphism E :
     MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (fupd (PROP:=PROP) E E).
-  Proof. split; [split|]; try apply _. apply fupd_sep. apply fupd_intro. Qed.
+  Proof. split; [split|]; try apply _; [apply fupd_sep | apply fupd_intro]. Qed.
 
   Lemma big_sepL_fupd {A} E (Φ : nat → A → PROP) l :
     ([∗ list] k↦x ∈ l, |={E}=> Φ k x) ={E}=∗ [∗ list] k↦x ∈ l, Φ k x.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 6f2af1ea3b4b02b6910f4179ae3b7a0ca4592619..502326653c7672a06f2219b79cf99bfbb91bba18 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -35,9 +35,9 @@ Implicit Types mP : option PROP.
 Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (⊢ P) P | 0.
 Proof. by rewrite /AsEmpValid. Qed.
 Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
-Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
+Proof. split; [ apply bi.entails_wand | apply bi.wand_entails ]. Qed.
 Global Instance as_emp_valid_equiv P Q : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
-Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
+Proof. split; [ apply bi.equiv_wand_iff | apply bi.wand_iff_equiv ]. Qed.
 
 Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
   (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀ x, φ x) (∀ x, P x).
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index baa2514ea02660585ce60420dc38a5fe1e233a63..6dbcd41a34c1c9529af05f1d7c3b3846c46e2490 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -58,7 +58,7 @@ Proof.
   - (* emp ∗ P ⊢ P *)
     intros P. apply and_elim_r.
   - (* P ∗ Q ⊢ Q ∗ P *)
-    intros P Q. apply and_intro. apply and_elim_r. apply and_elim_l.
+    intros P Q. apply and_intro; [ apply and_elim_r | apply and_elim_l ].
   - (* (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R) *)
     intros P Q R. repeat apply and_intro.
     + etrans; first apply and_elim_l. by apply and_elim_l.
@@ -97,13 +97,19 @@ Proof.
   - exact: @later_exist_false.
   - (* ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q *)
     intros P Q.
-    apply and_intro; apply later_mono. apply and_elim_l. apply and_elim_r.
+    apply and_intro; apply later_mono.
+    + apply and_elim_l.
+    + apply and_elim_r.
   - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
     intros P Q.
     trans (siProp_forall (λ b : bool, siProp_later (if b then P else Q))).
-    { apply forall_intro=> -[]. apply and_elim_l. apply and_elim_r. }
+    { apply forall_intro=> -[].
+      - apply and_elim_l.
+      - apply and_elim_r. }
     etrans; [apply later_forall_2|apply later_mono].
-    apply and_intro. refine (forall_elim true). refine (forall_elim false).
+    apply and_intro.
+    + refine (forall_elim true).
+    + refine (forall_elim false).
   - (* ▷ <pers> P ⊢ <pers> ▷ P *)
     done.
   - (* <pers> ▷ P ⊢ ▷ <pers> P *)
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index cddd8489805368ef7c9e875ea29498482585091c..30343ff494346216306dfd3917d5e3768d14f97d 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -215,14 +215,23 @@ Proof. unseal; by split=> n [??]. Qed.
 Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
 Proof. unseal; by split=> n [??]. Qed.
 Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
-Proof. intros HQ HR; unseal; split=> n ?; by split; [apply HQ|apply HR]. Qed.
+Proof.
+  intros HQ HR; unseal; split=> n ?.
+  split.
+  - by apply HQ.
+  - by apply HR.
+Qed.
 
 Lemma or_intro_l P Q : P ⊢ P ∨ Q.
 Proof. unseal; split=> n ?; left; auto. Qed.
 Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
 Proof. unseal; split=> n ?; right; auto. Qed.
 Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
-Proof. intros HP HQ. unseal; split=> n [?|?]. by apply HP. by apply HQ. Qed.
+Proof.
+  intros HP HQ. unseal; split=> n [?|?].
+  - by apply HP.
+  - by apply HQ.
+Qed.
 
 Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
 Proof.