…#27397)

…nity#27285)

`dist_pos` is already a simp lemma, so `dist_nonneg` should be too.

This PR adds a defeq test for multiple paths that convert rings in Mathlib's algebraic hierarchy to abelian groups in grind's hierarchy.
This defeq test used to fail before `leanprover/lean4:v4.22.0-rc3`.

…ng fork (leanprover-community#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

…ommunity#26169)

In order to construct a model category, we may sometimes have basically proven all the axioms with the exception of the left lifting property of cofibrations with respect to trivial fibrations. A trick by Joyal allows to obtain this lifting property under suitable assumptions, namely that cofibrations are stable under composition and cobase change. (The dual statement is also formalized.)

This will be used in the formalization of the model category structure on topological spaces, simplicial sets, simplicial presheaves, etc.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…ity#23547)

Let `P` and `P'` be morphism properties of schemes. We show some results to deduce
that `P` descends along `P'` from a codescent property of ring homomorphisms.



Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

…7396)

This PR deals with adaptation notes in Mathlib that have become irrelevant or easily fixable. The remainder are going to require actual thinking to fix.

…ences (leanprover-community#25943)

Given a commutative ring `k` and a group `G`, this PR shows that a short exact sequence of `k`-linear `G`-representations 
`0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` induces a short exact sequence of complexes
`0 ⟶ inhomogeneousChains X₁ ⟶ inhomogeneousChains X₂ ⟶ inhomogeneousChains X₃ ⟶ 0`.

Since the homology of `inhomogeneousChains Xᵢ` is the group homology of `Xᵢ`, this allows us to specialize API about long exact sequences to group homology.



Co-authored-by: 101damnations <101damnations@github.com>

We now have a `Defs` file defining `SignType` and basic instances, as well as a `Basic` file proving results about the sign function on a ring.

The files have not been changed beyond updating the module description.

…ut `mkPiAlgebra` (leanprover-community#27352)

Also swap the order of some lemmas to put the ones with weaker typeclass assumptions first.

…clarations (leanprover-community#27389)

These were introduced mostly as an adaptation for lean4#7717, but they seem to be unnecessary anymore. Since the changes were applied long ago, I can't see the build errors in the logs to figure out the exact issue. (I assume that they simply were not getting inferred.)

In addition to the now-unnecessary `norm_mul_self_le` field for `CStarAlgebra` introduced in those adaptation notes, we can also get rid of quite a few unnecessary `mul_comm` fields.

This was copied in leanprover-community#27386 to

https://github.com/leanprover-community/mathlib4/blob/d3c295b45d6f0bdb356f99ebe071016f2559eb73/Mathlib/Algebra/GroupWithZero/Action/Hom.lean#L19-L24

but I forgot to delete the original.

…anprover-community#27421)

As discussed [here](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/.E2.9C.94.20Maximum.20recursion.20error.20at.20simp.20tactic/with/530502013), I got an infinite simp loop where it repeatedly tried to apply `PullbackCone.π_app_left`. This was the definition from mathlib:

```
/-- The first projection of a pullback cone. -/
abbrev fst (t : PullbackCone f g) : t.pt ⟶ X :=
  t.π.app WalkingCospan.left
...
@[simp]
theorem π_app_left (c : PullbackCone f g) : c.π.app WalkingCospan.left = c.fst := rfl
```

Seems like it unfolded the abbrev to immedeately apply the theorem again. So I removed the simp tags, let's see if the build runs through.

…ty#26626)

Currently, `CompleteLattice` extends `Top` and `Bot`, and introduces `le_top` and `bot_le`. Finally, `CompleteLattice` introduces an instance of `BoundedOrder`. This PR makes `CompleteLattice` extend `BoundedOrder` directly instead.

…rover-community#26114)

This is part of leanprover-community#25140, and is the special case of Hahn embedding theorem applied to archimedean group.

Adds a `@[simp]` theorem `lift_symm_apply` and a regular theorem `coe_lift_symm`.

From Toric

…-community#27384)

…community#27409)

These match the Finsupp instances more closely.

)

Fix the module docstring to reflect the actual names of the dsimprocs

Add lemmas about `sub`/`neg` for `aeval`. These are already available for `eval` and `eval₂`.

… note "we should have a tactic to crush this" (leanprover-community#27372)

Remove:

```
  /- The below proof (due to Mario Carneiro, Johan Commelin, Bhavik Mehta, Jingting Wang) should
     not really be necessary: we should have a tactic to crush this. -/
```

We now have such a tactic! 🎉

Many other things can have bases.

…chimedean (leanprover-community#27436)

Thanks to the ongoing effort to get the Hahn Embedding theorem into Mathlib

…community#27360)

Adds lemmas for rdropWhile and rtakeWhile.

These lemmas were identified while doing work for Project Numina.




Co-authored-by: Bolton Bailey <bolton.bailey@gmail.com>

…ver-community#27405)

This bug in the `reorder` feature was found while developing `to_dual`. To fix it, we modify the `expand` function to not just eta-expand, but also to expand raw projections.

…orders are trivial (leanprover-community#27172)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

…community#27338)

The usual `smul_eq_mul` simp lemma runs into a diamond from two `SMul` instances on units of a `CommMonoid`: `Units.mulAction'.toSMul` and `Mul.toSMul`. This PR adds an extra simp lemma to cover this case.

…` using `grind` (leanprover-community#27770)

…`grind` (leanprover-community#27771)

…iff` using `grind` (leanprover-community#27772)

…ng `grind` (leanprover-community#27773)

…_pairs_eq` using `grind` (leanprover-community#27774)

…7793)

…leanprover-community#27784)

…smul_of_minpoly_isEisensteinAt` using `grind` (leanprover-community#27775)

…leanprover-community#27776)

…7797)

This PR updates the Mathlib dependencies.

One should instead use `(Module.Free.chooseBasis R M).repr`.