diff --git a/templates/contribute/style.md b/templates/contribute/style.md
index 441d59170..8f3d21f7e 100644
--- a/templates/contribute/style.md
+++ b/templates/contribute/style.md
@@ -363,8 +363,25 @@ theorem reverse_reverse : ∀ (l : List α), reverse (reverse l) = l
       _ = a :: l := rfl
 ```
 
-However, because the expressions and proofs are relatively short, the following style
-might be preferable in this situation.
+The following style has the substantial advantage of having all lines be interchangeable, which is
+particularly useful when editing the proof in eg VSCode:
+
+```lean
+import Init.Data.List.Basic
+
+open List
+
+theorem reverse_reverse : ∀ (l : List α), reverse (reverse l) = l
+  | []       => rfl
+  | (a :: l) => calc
+          reverse (reverse (a :: l))
+      _ = reverse (reverse l ++ [a]) := by rw [reverse_cons]
+      _ = reverse [a] ++ reverse (reverse l) := reverse_append _ _
+      _ = reverse [a] ++ l := by rw [reverse_reverse l]
+      _ = a :: l := rfl
+```
+
+If the expressions and proofs are relatively short, the following style is also an option:
 
 ```lean
 import Init.Data.List.Basic