diff --git a/theories/base_logic/bupd_alt.v b/theories/base_logic/bupd_alt.v
index c058493a20cdeb382bba742f73368465aa5437bf..307f388509763355a70d964b891279050da82f2f 100644
--- a/theories/base_logic/bupd_alt.v
+++ b/theories/base_logic/bupd_alt.v
@@ -88,7 +88,11 @@ Proof.
 Qed.
 
 Lemma bupd_alt_bupd_iff {M} (P : uPred M) : bupd_alt P ⊣⊢ |==> P.
-Proof. apply (anti_symm _). apply bupd_alt_bupd. apply bupd_bupd_alt. Qed.
+Proof.
+  apply (anti_symm _).
+  - apply bupd_alt_bupd.
+  - apply bupd_bupd_alt.
+Qed.
 
 (** The law about the interaction between [uPred_ownM] and plainly holds. *)
 Lemma ownM_updateP {M : ucmraT} x (Φ : M → Prop) (R : uPred M) :
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index a186d80b6fe81107f5a1a40ecb182a45174a5902..aa110f947f6232a3f671b6828513f65a7b54a7ec 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -183,7 +183,8 @@ Proof.
   iIntros (?) "HQ Hbox".
   iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
   iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
-  by apply lookup_insert. by rewrite insert_insert.
+  - by apply lookup_insert.
+  - by rewrite insert_insert.
 Qed.
 
 Lemma slice_delete_full E q f P Q γ :
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index f0b3719daab960d4571842c57e7329b714a3e9a0..edc62ff7a345b709b882cee7c624347375c5bd01 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -42,7 +42,7 @@ Section proofs.
   Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
   Global Instance cinv_own_as_fractional γ q :
     AsFractional (cinv_own γ q) (cinv_own γ) q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; [done|]. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
   Proof. rewrite -frac_validI. apply (own_valid_2 γ q1 q2). Qed.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index ac6140a6602e0d055f987f85829de9e38da70035..c30ba89986e7310b7294a2c46ca5b40aa70f2f76 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -155,7 +155,7 @@ Section gen_heap.
   Qed.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; [done|]. apply _. Qed.
 
   Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜q ≤ 1⌝%Qp.
   Proof.
diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index 0632b0c24f6ce076358239442e0a486d7ccb28e5..2bcb89251454f298054b3ac7309d4a3545ebc5e6 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/theories/base_logic/lib/ghost_var.v
@@ -33,7 +33,7 @@ Section lemmas.
   Proof. intros q1 q2. rewrite /ghost_var -own_op -frac_agree_op //. Qed.
   Global Instance ghost_var_as_fractional γ a q :
     AsFractional (ghost_var γ q a) (λ q, ghost_var γ q a) q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; [done|]. apply _. Qed.
 
   Lemma ghost_var_alloc_strong a (P : gname → Prop) :
     pred_infinite P →
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index c991982418c605ceca2c0ca42c45c324447fdf58..c900737bd28176cd1b2197febd06203f84e74f6f 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -78,13 +78,14 @@ Section proofs.
     iIntros "HP".
     iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
     iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
-    { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
-      apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset))).
-      intros Ef. exists (coPpick (↑ N ∖ gset_to_coPset Ef)).
-      rewrite -elem_of_gset_to_coPset comm -elem_of_difference.
-      apply coPpick_elem_of=> Hfin.
-      eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
-      apply gset_to_coPset_finite. }
+    { apply prod_updateP'.
+      - apply cmra_updateP_id, (reflexivity (R:=eq)).
+      - apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset))).
+        intros Ef. exists (coPpick (↑ N ∖ gset_to_coPset Ef)).
+        rewrite -elem_of_gset_to_coPset comm -elem_of_difference.
+        apply coPpick_elem_of=> Hfin.
+        eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
+        apply gset_to_coPset_finite. }
     simpl. iDestruct "Hm" as %(<- & i & -> & ?).
     rewrite /na_inv.
     iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
diff --git a/theories/options.v b/theories/options.v
index 895e51f007c38d235f66bb186ce7ea14ceef50bf..1e4c1f31180de56458fb5f0c68d15a150293786e 100644
--- a/theories/options.v
+++ b/theories/options.v
@@ -6,6 +6,10 @@ but not transitively. *)
 Export Set Default Proof Using "Type".
 Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
 
+(* Enforces that every tactic is executed with a single focused goal, meaning
+that bullets and curly braces must be used to structure the proof. *)
+Export Set Default Goal Selector "!".
+
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.
 From iris Require Import options.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index fc3abc68ca672391c6cb66da6e151a86ccefd4a0..3a1bf860bb7c98029b957673fec65b44b9175b97 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -174,7 +174,11 @@ Lemma adequate_alt {Λ} s e1 σ1 (φ : val Λ → state Λ → Prop) :
     rtc erased_step ([e1], σ1) (t2, σ2) →
       (∀ v2 t2', t2 = of_val v2 :: t2' → φ v2 σ2) ∧
       (∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2).
-Proof. split. intros []; naive_solver. constructor; naive_solver. Qed.
+Proof.
+  split.
+  - intros []; naive_solver.
+  - constructor; naive_solver.
+Qed.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
   adequate NotStuck e1 σ1 φ →
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 06f722a4fdcf9a211ef9f299c8677c6a609e2b6b..1fa5c032451c0deda1c75b38eb8a6a57143415e2 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -204,7 +204,8 @@ Proof.
   { destruct s; eauto using reducible_no_obs_reducible. }
   iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as (->) "(Hσ & H & Hfork)".
   iApply step_fupd_intro; [set_solver+|]. iNext.
-  iFrame "Hσ". iSplitL "H". by iApply "IH".
+  iFrame "Hσ". iSplitL "H".
+  { by iApply "IH". }
   iApply (@big_sepL_impl with "Hfork").
   iIntros "!>" (k ef _) "H". by iApply "IH".
 Qed.