diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b1304e73985b39146323e0cb0e767e3823702bb2..4a7325f8bbf842e860357885f6af65158bfc39cc 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1425,7 +1425,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 +1456,13 @@ Section option.
 
   Lemma exclusiveN_Some_l n a `{!Exclusive a} mb :
     ✓{n} (Some a ⋅ mb) → mb = None.
-  Proof. destruct mb; [|done]. move=> /(exclusiveN_l _ a) []. 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; [|done]. move=> /(exclusive_l a) []. 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 +1474,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; [|eauto]. by intros [->|?]. 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; [|eauto]. by intros [->|?]. 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/coPset.v b/theories/algebra/coPset.v
index 0250c6922dd282329fdd19bbe1eb38808869d8de..dcd07527b2f44ed3006152d757a4ee7d56e42a71 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -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/gmultiset.v b/theories/algebra/gmultiset.v
index 27f1eab6753378149c3cd1ab98a48dc822f82e33..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 | | done]. intros X. by rewrite gmultiset_op_disj_union left_id_L. 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/ofe.v b/theories/algebra/ofe.v
index 8a7f5cb70720e48409668969acd96bd2bb5d9549..0b0963f54a6172a35c875a23c9fb08336323d53f 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -281,7 +281,9 @@ Section limit_preserving.
     LimitPreserving (λ x, P1 x ∧ P2 x).
   Proof.
     intros Hlim1 Hlim2 c Hc.
-    split; [ apply Hlim1, Hc | apply Hlim2, Hc ].
+    split.
+    - apply Hlim1, Hc.
+    - apply Hlim2, Hc.
   Qed.
 
   Lemma limit_preserving_impl (P1 P2 : A → Prop) :
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index f8bc17d885b01866f85b28dd2ed4beb9dca3c92e..13926381f41499485cb2fe164f6adba79d64ff88 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1565,19 +1565,19 @@ 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; try 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; try 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 d693e22e0ad860d8047b2d2a9d667c52611ec2e9..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. *)
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index bb30eb594a5f0d60b2240624e1e09f7292911611..f2bb21e9a3f0d255a31d0ab44790c21675dbce3d 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -520,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.
@@ -554,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=>/=;
@@ -564,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.