[Merged by Bors] - doc(docs): fix typos

docs/Conv/Guide.lean

@@ -80,7 +80,7 @@ in Lean 4 core.
 * `all_goals convSeq` runs the `conv` tactics on every `conv` goal, collecting all the produced
   subgoals (if any).
 
-* `any_goals convSeq` is like `all_goals` but succeeds if the tactic sequence succees for any
+* `any_goals convSeq` is like `all_goals` but succeeds if the tactic sequence succeeds for any
   of the goals.
 
 * `case tag => convSeq` focuses on a goal with a given tag, runs the tactic sequence, and then

docs/Conv/Introduction.lean

@@ -118,7 +118,7 @@ example (a b c : ℕ) : a * (b * c) = a * (c * b) := by
 ```
 
 In all those cases, only the first match is affected.
-One can also specify which occurences to convert using an `occs` clause, which
+One can also specify which occurrences to convert using an `occs` clause, which
 creates goals for every matched occurrence. These can then all be handled at once
 using the `all_goals` combinator.
 The following performs rewriting only for the second and third occurrences of `b * c`:

docs/overview.yaml

@@ -46,7 +46,7 @@ General algebra:
     cyclic group: 'IsCyclic'
     nilpotent group: 'Group.IsNilpotent'
     permutation group of a type: 'Equiv.Perm'
-    structure of fintely generated abelian groups: 'AddCommGroup.equiv_free_prod_directSum_zmod'
+    structure of finitely generated abelian groups: 'AddCommGroup.equiv_free_prod_directSum_zmod'
 
   Rings:
     ring: 'Ring'