…d` (#15951)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…nalyticGroupoid` (#10853)

1. Change the definition of `analyticGroupoid` to mean analytic everywhere including on the boundary, using the recently added `AnalyticWithinAt` def.
2. Define `AnalyticManifold` as a charted space compatible with `analyticGroupoid`. 

In finite dimensions `AnalyticManifold` is equivalent to `SmoothManifoldWithCorners`, so an alternative option would be to leave this out and prove the necessary correspondence via Osgood's theorem. However, we don't have Osgood's theorem yet, and it's nice to have a version that works arbitrarily.

Prove Beck's comonadicity theorem by dualizing everything in [CategoryTheory.Monad.Monadicity](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monad/Monadicity.html).

This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024.



Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com>

…16027)

From LeanAPAP

chore: Fix mistakes in user-facing error and trace messages

At least, until I fix a bug, reported both on [Mathlib](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/haveLet.20linter.20crashing.20under.20.60byAsSorry.60) and on projects depending on [Mathlib](https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/Outstanding.20tasks.2C.20version.202.2E0/near/464281461).

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

These paths refer to files and folders that used to exist but not anymore due to refactors such as [mathlib3#12929](leanprover-community/mathlib3#12929) and [mathlib3#8095](#8095).

For an `AddCommGroup` `A` and an integer `n`,
- Define `AddSubgroup.torsionBy A n` using `Submodule.torsionBy`;
- Define a scoped notation `A[n]`.

Additionally, for a natural number `n`,
- Equip `A[n]` with a `ZMod n`-module structure.

…ata.Int.Order` (#15152)

We swap out some bundled ordered algebra API calls for native `Nat` and `Int` ones. We also add one. This allows us to avoid needing bundled ordered algebra in this file and pushes its import further downstream. Since it touches `Init.Data.Int.Order`, we rename it `Data.Int.Order.Basic`. 



Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

This PR adds more API lemmas about the bicategory of categories `Cat`. These are added as `simp` is not able to use the corresponding `NatTrans` lemmas when working with 2-morphisms in the bicategory `Cat`.

Due to this some proofs in `CategoryTheory/Grothendieck` can be golfed.

…flat as a submodule (#15360)

A tweak to `linear_combination` so that when the default normalization tactic fails, the "red underlines" appear on the `linear_combination` call itself, rather than just on the "by" at the start of the proof.  For example, compare before/after on this example:
```lean
import Mathlib

example {a : ℤ} (h : a = 1) : a = 2 := by
  linear_combination h
```

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Propagating.20errors.20through.20Unhygienic.2Erun

This PR updates the Mathlib dependencies.

…6048)

Found by a linter in #10235
Mostly repeats @grunweg's  #15306 accidentally reverted by @semorrison's #15726

…lgebra` typeclasses (#14699)

Define a typeclass `Differential` of `CommRing`s with a chosen `Derivation`, a notation for that derivation, and a `DifferentialAlgebra` for `Algerba`s on differential rings whose `algebraMap` commutes with the derivation.



Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

…als (#14579)

so that printing the definitions shows `match … with` properly, and
meta code looking for matchers work.

Fixes an item on #1074

Similar lemmas about `pure` are already in the default `simp` set.

…#16024)

This is simply not simpler

From LeanAPAP

I need this to drop `[T2Space _]` assumptions here and there.

Define an `IsHomeomorph` predicate for maps between topological spaces to complement the existing bundled `Homeomorph` API.



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

... in finite dimensions.

This PR updates the Mathlib dependencies.

From LeanAPAP

…l Inner Product Space as Direct Sum of Simultaneous Eigenspaces of Commuting Symmetric Operators (#15012)

Introduced `Mathlib.Analysis.InnerProductSpace.Simultaneous.lean` as a receptacle for results concerning simultaneous eigenspace decomposition results for tuples of commuting symmetric operators on (finite-dimensional) Hilbert space. 

Includes decomposition of finite-dimensional Hilbert space as internal direct sum of simultaneous eigenspaces of a commuting pair of symmetric operators.

Co-Authored by: Jack Cheverton <jt18chev@siena.edu>

Co-Authored by: Samyak Dhar Tuladhar <sd10tula@siena.edu>



Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>

This PR updates the Mathlib dependencies.

…ady-to-merge label (#16335)

This should prevent cases where the bot repeatedly cancels bors batches as in #16286

This should fix [these errors](https://github.com/leanprover-community/mathlib4/actions/runs/10640763528/job/29500994383#step:1:36).

From LeanAPAP

Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>

All these lemmas have pretty generic names

#16268)

…age.IsContextFree` for consistency with #13554

… calculus has nonempty spectrum (#16343)

In particular, this gives us that the `ℝ`-spectrum of selfadjoint elements and the `ℝ≥0`-spectrum of nonnegative elements in a C⋆-algebra are nonempty.

It's better if the NIGHTLY_TESTING token is reserved for the nightly-testing-* branches.

This should also hopefully help with API limits.

…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.

…as (#16266)

`Quot.exact` ↦ `Quot.eqvGen_exact`
`Quot.EqvGen_sound` ↦ `Quot.eqvGen_sound`

… the reviewdog comments (#16365)

Cf. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/reviewdog/near/466505584)

…ofinite` (#14382)

Let `(Sᵢ)_{i : I}` be a family of finite sets indexed by a cofiltered category `I` and let `S` be
its limit in `Profinite`. Let `G` be a functor from `Profinite` to a category `C` and suppose that
`G` preserves the limit described above. Suppose further that the projection maps `S ⟶ Sᵢ` are
epimorphic for all `i`. Then `G.obj S` is isomorphic to a limit indexed by
`StructuredArrow S toProfinite` (see `Profinite.Extend.isLimitCone`).

We also provide the dual result for a functor of the form `G : Profiniteᵒᵖ ⥤ C`.

`fun_prop` was resynthesizing type class arguments the same way as  `simp` used to do. It seems to cause just troubles and seemingly no benefit so let's remove it from `fun_prop` too.

Currently, some style exceptions emitted by the `lint-style.py` script are not recognised by that same script. This can lead to confusing behaviour.
That said, all current exceptions should rather be fixed than excepted - so this is unlikely to be an issue in practice.