leanprover-community · harahu · Oct 16, 2025 · Oct 17, 2025 · Oct 17, 2025
diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean
@@ -14,7 +14,7 @@ import Mathlib.Data.ZMod.Defs
 /-!
 # Freiman homomorphisms
 
-In this file, we define Freiman homomorphisms and isomorphism.
+In this file, we define Freiman homomorphisms and isomorphisms.
 
 An `n`-Freiman homomorphism from `A` to `B` is a function `f : α → β` such that `f '' A ⊆ B` and
 `f x₁ * ... * f xₙ = f y₁ * ... * f yₙ` for all `x₁, ..., xₙ, y₁, ..., yₙ ∈ A` such that
@@ -57,7 +57,7 @@ an `AddMonoid`/`Monoid` instead of the `AddMonoid`/`Monoid` itself.
 
 * `MonoidHomClass.isMulFreimanHom` could be relaxed to `MulHom.toFreimanHom` by proving
   `(s.map f).prod = (t.map f).prod` directly by induction instead of going through `f s.prod`.
-* Affine maps are Freiman homs.
+* Affine maps are Freiman homomorphisms.
 -/
 
 assert_not_exists Field Ideal TwoSidedIdeal

diff --git a/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/Mathlib/Combinatorics/Enumerative/DyckWord.lean
@@ -62,7 +62,7 @@ structure DyckWord where
   toList : List DyckStep
   /-- There are as many `U`s as `D`s -/
   count_U_eq_count_D : toList.count U = toList.count D
-  /-- Each prefix has as least as many `U`s as `D`s -/
+  /-- Each prefix has at least as many `U`s as `D`s -/
   count_D_le_count_U i : (toList.take i).count D ≤ (toList.take i).count U
   deriving DecidableEq
 

diff --git a/Mathlib/Combinatorics/Quiver/Cast.lean b/Mathlib/Combinatorics/Quiver/Cast.lean
@@ -10,7 +10,7 @@ import Mathlib.Combinatorics.Quiver.Path
 
 # Rewriting arrows and paths along vertex equalities
 
-This files defines `Hom.cast` and `Path.cast` (and associated lemmas) in order to allow
+This file defines `Hom.cast` and `Path.cast` (and associated lemmas) in order to allow
 rewriting arrows and paths along equalities of their endpoints.
 
 -/

diff --git a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@@ -17,12 +17,12 @@ import Mathlib.Algebra.BigOperators.Group.Finset.Powerset
 # The Ahlswede-Zhang identity
 
 This file proves the Ahlswede-Zhang identity, which is a nontrivial relation between the size of the
-"truncated unions"  of a set family. It sharpens the Lubell-Yamamoto-Meshalkin inequality
+"truncated unions" of a set family. It sharpens the Lubell-Yamamoto-Meshalkin inequality
 `Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose`, by making explicit the correction
 term.
 
 For a set family `𝒜` over a ground set of size `n`, the Ahlswede-Zhang identity states that the sum
-of `|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|)` over all set `A` is exactly `1`. This implies the LYM
+of `|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|)` over all sets `A` is exactly `1`. This implies the LYM
 inequality since for an antichain `𝒜` and every `A ∈ 𝒜` we have
 `|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|) = 1 / n.choose |A|`.
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean b/Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
@@ -16,20 +16,20 @@ A graph is complete multipartite iff non-adjacency is transitive.
 
 ## Main declarations
 
-* `SimpleGraph.IsCompleteMultipartite`: predicate for a graph to be complete-multi-partite.
+* `SimpleGraph.IsCompleteMultipartite`: predicate for a graph to be complete multipartite.
 
 * `SimpleGraph.IsCompleteMultipartite.setoid`: the `Setoid` given by non-adjacency.
 
 * `SimpleGraph.IsCompleteMultipartite.iso`: the graph isomorphism from a graph that
   `IsCompleteMultipartite` to the corresponding `completeMultipartiteGraph`.
 
-* `SimpleGraph.IsPathGraph3Compl`: predicate for three vertices to be a witness to
-  non-complete-multi-partite-ness of a graph G. (The name refers to the fact that the three
+* `SimpleGraph.IsPathGraph3Compl`: predicate for three vertices to witness the
+  non-complete-multipartiteness of a graph `G`. (The name refers to the fact that the three
   vertices form the complement of `pathGraph 3`.)
 
-* See also: `Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean`
-  `colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree` a maximally `r + 1`- cliquefree graph
-  is `r`-colorable iff it is complete-multipartite.
+* See also: `Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean`.
+  The lemma `colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree` states that a maximally
+  `r + 1`-cliquefree graph is `r`-colorable iff it is complete multipartite.
 
 * `SimpleGraph.completeEquipartiteGraph`: the **complete equipartite graph** in parts of *equal*
   size such that two vertices are adjacent if and only if they are in different parts.

diff --git a/Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean b/Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
@@ -12,7 +12,7 @@ import Mathlib.Data.Fin.Parity
 /-!
 # Concrete colorings of common graphs
 
-This file defines colorings for some common graphs
+This file defines colorings for some common graphs.
 
 ## Main declarations
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -11,12 +11,12 @@ import Mathlib.Combinatorics.SimpleGraph.Subgraph
 
 This file introduces the concept of one simple graph containing a copy of another.
 
-For two simple graph `G` and `H`, a *copy* of `G` in `H` is a (not necessarily induced) subgraph of
+For two simple graphs `G` and `H`, a *copy* of `G` in `H` is a (not necessarily induced) subgraph of
 `H` isomorphic to `G`.
 
 If there exists a copy of `G` in `H`, we say that `H` *contains* `G`. This is equivalent to saying
-that there is an injective graph homomorphism `G → H` them (this is **not** the same as a graph
-embedding, as we do not require the subgraph to be induced).
+that there is an injective graph homomorphism `G → H` between them (this is **not** the same as a
+graph embedding, as we do not require the subgraph to be induced).
 
 If there exists an induced copy of `G` in `H`, we say that `H` *inducingly contains* `G`. This is
 equivalent to saying that there is a graph embedding `G ↪ H`.

diff --git a/Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean b/Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean
@@ -12,7 +12,7 @@ import Mathlib.Data.Nat.Choose.Cast
 /-!
 # Turán density
 
-This files defines the **Turán density** of a simple graph.
+This file defines the **Turán density** of a simple graph.
 
 ## Main definitions
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean b/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
@@ -110,8 +110,8 @@ private lemma IsNClique.insert_insert_erase (hs : G.IsNClique r (insert a s)) (h
 An `IsFiveWheelLike r k v w₁ w₂ s t` structure in `G` consists of vertices `v w₁ w₂` and `r`-sets
 `s` and `t` such that `{v, w₁, w₂}` induces the single edge `w₁w₂` (i.e. they form an
 `IsPathGraph3Compl`), `v, w₁, w₂ ∉ s ∪ t`, `s ∪ {v}, t ∪ {v}, s ∪ {w₁}, t ∪ {w₂}` are all
-`(r + 1)`- cliques and `#(s ∩ t) = k`. (If `G` is maximally `(r + 2)`-cliquefree and not complete
-multipartite then `G` will contain such a structure : see
+`(r + 1)`-cliques and `#(s ∩ t) = k`. (If `G` is maximally `(r + 2)`-clique-free and not complete
+multipartite then `G` will contain such a structure: see
 `exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite`.)
 -/
 @[grind]
@@ -357,7 +357,7 @@ lemma minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ [Fintype α]
     obtain ⟨_, _, hW⟩ := hw.exists_isFiveWheelLike_succ_of_not_adj_le_two hcf
       (by simpa [X] using hx) <| Nat.le_of_succ_le_succ h
     exact hm hW
-  -- Since `G` is `Kᵣ₊₂`- free and contains a `Wᵣ,ₖ` every vertex is not adjacent to at least one
+  -- Since `G` is `Kᵣ₊₂`-free and contains a `Wᵣ,ₖ`, every vertex is not adjacent to at least one
   -- wheel vertex.
   have one_le (x : α) : 1 ≤ #{z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬ G.Adj x z} :=
     let ⟨_, hz⟩ := hw.isNClique_fst_left.exists_not_adj_of_cliqueFree_succ hcf x