leanprover-community · euprunin · Feb 20, 2025
diff --git a/Archive/Imo/Imo2024Q3.lean b/Archive/Imo/Imo2024Q3.lean
@@ -30,7 +30,7 @@ open scoped Finset
 namespace Imo2024Q3
 
 /-- The condition of the problem. Following usual Lean conventions, this is expressed with
-indices starting from 0, rather than from 1 as in the informal statment (but `N` remains as the
+indices starting from 0, rather than from 1 as in the informal statement (but `N` remains as the
 index of the last term for which `a n` is not defined in terms of previous terms). -/
 def Condition (a : ℕ → ℕ) (N : ℕ) : Prop :=
   (∀ i, 0 < a i) ∧ ∀ n, N < n → a n = #{i ∈ Finset.range n | a i = a (n - 1)}

diff --git a/Mathlib/Algebra/Azumaya/Matrix.lean b/Mathlib/Algebra/Azumaya/Matrix.lean
@@ -9,7 +9,7 @@ import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 /-!
 # Matrix algebra is an Azumaya algebra over R
 
-In this file we prove that finite dimesional matrix algebra `Matrix n n R` over `R`
+In this file we prove that finite dimensional matrix algebra `Matrix n n R` over `R`
 is an Azumaya algebra where `R` is a commutative ring.
 
 ## Main Results

diff --git a/Mathlib/Algebra/Module/SnakeLemma.lean b/Mathlib/Algebra/Module/SnakeLemma.lean
@@ -80,7 +80,7 @@ lemma SnakeLemma.eq_of_eq (x : K₃)
 
 /--
 **Snake Lemma**
-Supppose we have an exact commutative diagram
+Suppose we have an exact commutative diagram
 ```
                 K₃
                 |
@@ -124,7 +124,7 @@ lemma SnakeLemma.δ_eq (x : K₃) (y) (hy : f₂ y = ι₃ x) (z) (hz : g₁ z =
 
 include hι₂ in
 /--
-Supppose we have an exact commutative diagram
+Suppose we have an exact commutative diagram
 ```
         K₂ -F-→ K₃
         |       |
@@ -163,7 +163,7 @@ lemma SnakeLemma.exact_δ_right (F : K₂ →ₗ[R] K₃) (hF : f₂.comp ι₂
 
 include hπ₂ in
 /--
-Supppose we have an exact commutative diagram
+Suppose we have an exact commutative diagram
 ```
                 K₃
                 |
@@ -200,7 +200,7 @@ lemma SnakeLemma.exact_δ_left (G : C₁ →ₗ[R] C₂) (hF : G.comp π₁ = π
     rw [← G.comp_apply, hF, π₂.comp_apply, H₂, hπ₂.apply_apply_eq_zero]
 
 /--
-Supppose we have an exact commutative diagram
+Suppose we have an exact commutative diagram
 ```
                 K₃
                 |
@@ -232,7 +232,7 @@ lemma SnakeLemma.δ'_eq (hf₂ : Surjective f₂) (hg₁ : Injective g₁)
 
 include hι₂ in
 /--
-Supppose we have an exact commutative diagram
+Suppose we have an exact commutative diagram
 ```
         K₂ -F-→ K₃
         |       |
@@ -259,7 +259,7 @@ lemma SnakeLemma.exact_δ'_right (hf₂ : Surjective f₂) (hg₁ : Injective g
 
 include hπ₂ in
 /--
-Supppose we have an exact commutative diagram
+Suppose we have an exact commutative diagram
 ```
                 K₃
                 |

diff --git a/Mathlib/AlgebraicGeometry/IdealSheaf.lean b/Mathlib/AlgebraicGeometry/IdealSheaf.lean
@@ -37,7 +37,7 @@ We define ideal sheaves of schemes and provide various constructors for it.
 Ideal sheaves are not yet defined in this file as actual subsheaves of `𝒪ₓ`.
 Instead, for the ease of development and application,
 we define the structure `IdealSheafData` containing all necessary data to uniquely define an
-ideal sheaf. This should be refectored as a constructor for ideal sheaves once they are introduced
+ideal sheaf. This should be refactored as a constructor for ideal sheaves once they are introduced
 into mathlib.
 
 -/

diff --git a/Mathlib/Analysis/SpecialFunctions/Choose.lean b/Mathlib/Analysis/SpecialFunctions/Choose.lean
@@ -8,9 +8,9 @@ import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
 import Mathlib.Data.Nat.Cast.Field
 
 /-!
-# Binomial coefficents and factorial variants
+# Binomial coefficients and factorial variants
 
-This file proves asymptotic theorems for binomial coefficents and factorial variants.
+This file proves asymptotic theorems for binomial coefficients and factorial variants.
 
 ## Main statements
 

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean
@@ -12,7 +12,7 @@ import Mathlib.CategoryTheory.Subobject.Lattice
 # Subobjects in Grothendieck abelian categories
 
 We study the complete lattice of subjects of `X : C`
-when `C` is a Grothendieck abelian cateogry. In particular,
+when `C` is a Grothendieck abelian category. In particular,
 for a functor `F : J ⥤ MonoOver X` from a filtered category,
 we relate the colimit of `F` (computed in `C`) and the
 supremum of the subobjects corresponding to the objects

diff --git a/Mathlib/CategoryTheory/Category/ULift.lean b/Mathlib/CategoryTheory/Category/ULift.lean
@@ -121,13 +121,13 @@ instance ULiftHom.category : Category.{max v₂ v₁} (ULiftHom.{v₂} C) where
   id _ := ⟨𝟙 _⟩
   comp f g := ⟨f.down ≫ g.down⟩
 
-/-- One half of the quivalence between `C` and `ULiftHom C`. -/
+/-- One half of the equivalence between `C` and `ULiftHom C`. -/
 @[simps]
 def ULiftHom.up : C ⥤ ULiftHom C where
   obj := ULiftHom.objUp
   map f := ⟨f⟩
 
-/-- One half of the quivalence between `C` and `ULiftHom C`. -/
+/-- One half of the equivalence between `C` and `ULiftHom C`. -/
 @[simps]
 def ULiftHom.down : ULiftHom C ⥤ C where
   obj := ULiftHom.objDown

diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
@@ -85,7 +85,7 @@ theorem PreservesCoimage.hom_coimageImageComparison :
   simp [← Functor.map_comp, ← Iso.eq_inv_comp, ← cancel_epi (Abelian.coimage.π (F.map f)),
     ← cancel_mono (Abelian.image.ι (F.map f))]
 
-/-- If a functor preserves kernels and cokernels, it perserves coimage-image comparisons. -/
+/-- If a functor preserves kernels and cokernels, it preserves coimage-image comparisons. -/
 @[simps!]
 def PreservesCoimageImageComparison.iso :
     Arrow.mk (F.map (coimageImageComparison f)) ≅ Arrow.mk (coimageImageComparison (F.map f)) :=

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -229,7 +229,7 @@ end
 
 variable [SuccOrder J] [OrderBot J] [HasIterationOfShape J C]
 
-/-- The category of `j`th iterations of a succesor structure `Φ : SuccStruct C`.
+/-- The category of `j`th iterations of a successor structure `Φ : SuccStruct C`.
 An object consists of the data of all iterations of `Φ` for `i : J` such
 that `i ≤ j` (this is the field `F`). Such objects are
 equipped with data and properties which characterizes uniquely the iterations

diff --git a/Mathlib/Data/Matroid/Circuit.lean b/Mathlib/Data/Matroid/Circuit.lean
@@ -470,7 +470,7 @@ lemma IsCircuit.strong_elimination (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircu
 /-- The circuit elimination axiom : for any pair of distinct isCircuits `C₁, C₂` and any `e`,
 some circuit is contained in `(C₁ ∪ C₂) \ {e}`.
 
-This is one of the axioms when definining a finitary matroid via circuits;
+This is one of the axioms when defining a finitary matroid via circuits;
 as an axiom, it is usually stated with the extra assumption that `e ∈ C₁ ∩ C₂`. -/
 lemma IsCircuit.elimination (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircuit C₂) (h : C₁ ≠ C₂) (e : α) :
     ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C := by

diff --git a/Mathlib/FieldTheory/Differential/Liouville.lean b/Mathlib/FieldTheory/Differential/Liouville.lean
@@ -154,7 +154,7 @@ private local instance isLiouville_of_finiteDimensional_galois [FiniteDimensiona
     exists ι, inferInstance, c₀, ?_, u₀, v₀
     · -- We need to prove that all `c₀` are constants.
       -- This is true because they are the division of a constant by
-      -- a natural nubmer (which is also constant)
+      -- a natural number (which is also constant)
       intro x
       simp [c₀, Derivation.leibniz_div, hc]
     · -- Proving that this works is mostly straightforward algebraic manipulation,

diff --git a/Mathlib/GroupTheory/MonoidLocalization/Basic.lean b/Mathlib/GroupTheory/MonoidLocalization/Basic.lean
@@ -952,7 +952,7 @@ of the induced maps equals the map of localizations induced by `l ∘ g`."]
 theorem map_map {A : Type*} [CommMonoid A] {U : Submonoid A} {R} [CommMonoid R]
     (j : LocalizationMap U R) {l : P →* A} (hl : ∀ w : T, l w ∈ U) (x) :
     k.map hl j (f.map hy k x) = f.map (fun x ↦ show l.comp g x ∈ U from hl ⟨g x, hy x⟩) j x := by
-  -- Porting note: need to specifiy `k` explicitly
+  -- Porting note: need to specify `k` explicitly
   rw [← f.map_comp_map (k := k) hy j hl]
   simp only [MonoidHom.coe_comp, comp_apply]
 

diff --git a/Mathlib/Topology/CWComplex/Classical/Basic.lean b/Mathlib/Topology/CWComplex/Classical/Basic.lean
@@ -66,7 +66,7 @@ class RelCWComplex.{u} {X : Type u} [TopologicalSpace X] (C : Set X) (D : outPar
   This map is a bijection when restricting to `ball 0 1`, where we consider `(Fin n → ℝ)`
   endowed with the maximum metric. -/
   map (n : ℕ) (i : cell n) : PartialEquiv (Fin n → ℝ) X
-  /-- The source of every charactersitic map of dimension `n` is
+  /-- The source of every characteristic map of dimension `n` is
   `(ball 0 1 : Set (Fin n → ℝ))`. -/
   source_eq (n : ℕ) (i : cell n) : (map n i).source = ball 0 1
   /-- The characteristic maps are continuous when restricting to `closedBall 0 1`. -/

diff --git a/Mathlib/Topology/Category/CompHausLike/Basic.lean b/Mathlib/Topology/Category/CompHausLike/Basic.lean
@@ -128,7 +128,7 @@ section
 variable {X} {Y : Type u} [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [HasProp P Y]
 variable {Z : Type u} [TopologicalSpace Z] [CompactSpace Z] [T2Space Z] [HasProp P Z]
 
-/-- Typecheck a continous map as a morphism in the category `CompHausLike P`. -/
+/-- Typecheck a continuous map as a morphism in the category `CompHausLike P`. -/
 abbrev ofHom (f : C(X, Y)) : of P X ⟶ of P Y := ConcreteCategory.ofHom f
 
 @[simp] lemma hom_ofHom (f : C(X, Y)) : ConcreteCategory.hom (ofHom P f) = f := rfl

diff --git a/Mathlib/Util/PPOptions.lean b/Mathlib/Util/PPOptions.lean
@@ -14,7 +14,7 @@ namespace Mathlib
 open Lean
 
 /--
-The `pp.mathlib.binderPredicates` option is used to contol whether mathlib pretty printers
+The `pp.mathlib.binderPredicates` option is used to control whether mathlib pretty printers
 should use binder predicate notation (such as `∀ x < 2, p x`).
 -/
 register_option pp.mathlib.binderPredicates : Bool := {