From 204d46abff45f969e34669c8437c8d745155831b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 12 May 2026 12:43:59 +0200 Subject: [PATCH] doc: add newlines to clarify paragraph breaks These are strictly speaking, required by markdown, and make it more clear to the reader that a new paragraph begins. --- Mathlib/CategoryTheory/Filtered/Basic.lean | 1 + Mathlib/CategoryTheory/Monoidal/Functor.lean | 1 + Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean | 1 + Mathlib/CategoryTheory/NatIso.lean | 1 + Mathlib/Geometry/Manifold/LocalDiffeomorph.lean | 1 + Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean | 3 +++ Mathlib/Tactic/ComputeDegree.lean | 2 ++ Mathlib/Tactic/MinImports.lean | 2 ++ Mathlib/Tactic/MoveAdd.lean | 1 + 9 files changed, 13 insertions(+) diff --git a/Mathlib/CategoryTheory/Filtered/Basic.lean b/Mathlib/CategoryTheory/Filtered/Basic.lean index c738f240fab86a..abc400bfb542aa 100644 --- a/Mathlib/CategoryTheory/Filtered/Basic.lean +++ b/Mathlib/CategoryTheory/Filtered/Basic.lean @@ -32,6 +32,7 @@ easier to describe than general colimits (and more often preserved by functors). In this file we show that any functor from a finite category to a filtered category admits a cocone: * `cocone_nonempty [FinCategory J] [IsFiltered C] (F : J ⥤ C) : Nonempty (Cocone F)` + More generally, for any finite collection of objects and morphisms between them in a filtered category (even if not closed under composition) there exists some object `Z` receiving maps from all of them, diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean index 761a8f95e61437..bf0182a0e0379c 100644 --- a/Mathlib/CategoryTheory/Monoidal/Functor.lean +++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean @@ -16,6 +16,7 @@ A lax monoidal functor `F` between monoidal categories `C` and `D` is a functor between the underlying categories equipped with morphisms * `ε : 𝟙_ D ⟶ F.obj (𝟙_ C)` (called the unit morphism) * `μ X Y : (F.obj X) ⊗ (F.obj Y) ⟶ F.obj (X ⊗ Y)` (called the tensorator, or strength). + satisfying various axioms. This is implemented as a typeclass `F.LaxMonoidal`. Similarly, we define the typeclass `F.OplaxMonoidal`. For these oplax monoidal functors, diff --git a/Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean index ac44adebbf460c..4984e6b96136ed 100644 --- a/Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean @@ -15,6 +15,7 @@ When `C` is a monoidal category, the limit functor `lim : (J ⥤ C) ⥤ C` is la i.e. there are morphisms * `(𝟙_ C) → limit (𝟙_ (J ⥤ C))` * `limit F ⊗ limit G ⟶ limit (F ⊗ G)` + satisfying the laws of a lax monoidal functor. ## TODO diff --git a/Mathlib/CategoryTheory/NatIso.lean b/Mathlib/CategoryTheory/NatIso.lean index abdff0d1354332..6737823ba25dc2 100644 --- a/Mathlib/CategoryTheory/NatIso.lean +++ b/Mathlib/CategoryTheory/NatIso.lean @@ -14,6 +14,7 @@ For the most part, natural isomorphisms are just another sort of isomorphism. We provide some special support for extracting components: * if `α : F ≅ G`, then `α.app X : F.obj X ≅ G.obj X`, + and building natural isomorphisms from components: * ``` NatIso.ofComponents diff --git a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean index 0ecf4a6ef50a94..95b2e6e2256aad 100644 --- a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean +++ b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean @@ -130,6 +130,7 @@ protected theorem mdifferentiableAt (hn : n ≠ 0) {x : M} (hx : x ∈ Φ.source such as * further continuity and differentiability lemmas * refl and trans instances; lemmas between them. + As this declaration is meant for internal use only, we keep it simple. -/ end PartialDiffeomorph end PartialDiffeomorph diff --git a/Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean b/Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean index 30c98b8acd43a8..3589e93ce409bf 100644 --- a/Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean +++ b/Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean @@ -206,12 +206,15 @@ The reason is that types are usually implicit arguments. For example This gets extra points for matching `1` - `Nat.succ.inj (n m : ℕ) (h : n.succ = m.succ) : n = m`. This gets extra points for matching `ℕ` + Clearly, `rfl` is better. + - If we rewrite `|(0 : ℝ)|`, we could find - `abs_zero : |(0 : α)| = 0` This gets extra points for matching `0` - `Real.norm_eq_abs : ∀ (r : ℝ), ‖r‖ = |r|` This gets extra points for matching `ℝ` + Clearly, `abs_zero` is better In both examples, matching the type (`ℕ` or `ℝ`) was not very important for how good diff --git a/Mathlib/Tactic/ComputeDegree.lean b/Mathlib/Tactic/ComputeDegree.lean index 2c9d8f7ef32791..bac62528904010 100644 --- a/Mathlib/Tactic/ComputeDegree.lean +++ b/Mathlib/Tactic/ComputeDegree.lean @@ -19,6 +19,7 @@ Using `compute_degree` when the goal is of one of the seven forms * `natDegree f = d`, * `degree f = d`, * `coeff f d = r`, if `d` is the degree of `f`, + tries to solve the goal. It may leave side-goals, in case it is not entirely successful. @@ -53,6 +54,7 @@ Assume that `f : R[X]` is a polynomial with coefficients in a semiring `R` and If the goal has the form `natDegree f < d`, then we convert it to two separate goals: * `natDegree f ≤ ?_`, on which we apply the following steps; * `?_ < d`; + where `?_` is a metavariable that `compute_degree` computes in its process. We proceed similarly for `degree f < d`. diff --git a/Mathlib/Tactic/MinImports.lean b/Mathlib/Tactic/MinImports.lean index 732ae93bb3ddda..96d4e88a0a62a2 100644 --- a/Mathlib/Tactic/MinImports.lean +++ b/Mathlib/Tactic/MinImports.lean @@ -194,6 +194,7 @@ declaration names that are implied by * the attributes of `cmd` (if there are any), * the identifiers contained in `cmd`, * if `cmd` adds a declaration `d` to the environment, then also all the module names implied by `d`. + The argument `id` is expected to be an identifier. It is used either for the internally generated name of a "nameless" `instance` or when parsing an identifier representing the name of a declaration. @@ -217,6 +218,7 @@ module names that are implied by * the attributes of `cmd` (if there are any), * the identifiers contained in `cmd`, * if `cmd` adds a declaration `d` to the environment, then also all the module names implied by `d`. + The argument `id` is expected to be an identifier. It is used either for the internally generated name of a "nameless" `instance` or when parsing an identifier representing the name of a declaration. diff --git a/Mathlib/Tactic/MoveAdd.lean b/Mathlib/Tactic/MoveAdd.lean index 9f50f97feb181a..345843b422d91b 100644 --- a/Mathlib/Tactic/MoveAdd.lean +++ b/Mathlib/Tactic/MoveAdd.lean @@ -379,6 +379,7 @@ def reorderAndSimp (mv : MVarId) (instr : List (Expr × Bool)) : * an array of `Expr × Bool × Syntax`, as in the output of `parseArrows`, * the `Name` `op` of a binary operation, * an `Expr`ession `tgt`. + It unifies each `Expr`ession appearing as a first factor of the array with the atoms for the operation `op` in the expression `tgt`, returning * the lists of pairs of a matched subexpression with the corresponding `Bool`ean;