bump to nightly-2023-04-23-03

mathlib commit leanprover-community/mathlib@7e281de

Mathbin/Algebra/Algebra/Basic.lean

@@ -1503,7 +1503,7 @@ theorem coe_restrictScalars (f : M →ₗ[A] N) : ((f : M →ₗ[R] N) : M → N
 lean 3 declaration is
   forall (R : Type.{u1}) (M : Type.{u2}) (A : Type.{u3}) [_inst_12 : CommSemiring.{u1} R] [_inst_13 : AddCommMonoid.{u2} M] [_inst_14 : Module.{u1, u2} R M (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13] [_inst_15 : CommRing.{u3} A] [_inst_16 : Algebra.{u1, u3} R A _inst_12 (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15))], LinearMap.{u3, u3, max u2 u3, max u2 u3} A A (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15)) (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15)) (RingHom.id.{u3} A (Semiring.toNonAssocSemiring.{u3} A (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15)))) (LinearMap.{u1, u1, u2, u3} R R (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12))) M A _inst_13 (AddCommGroup.toAddCommMonoid.{u3} A (NonUnitalNonAssocRing.toAddCommGroup.{u3} A (NonAssocRing.toNonUnitalNonAssocRing.{u3} A (Ring.toNonAssocRing.{u3} A (CommRing.toRing.{u3} A _inst_15))))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15)) _inst_16)) (M -> A) (LinearMap.addCommMonoid.{u1, u1, u2, u3} R R M A (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13 (AddCommGroup.toAddCommMonoid.{u3} A (NonUnitalNonAssocRing.toAddCommGroup.{u3} A (NonAssocRing.toNonUnitalNonAssocRing.{u3} A (Ring.toNonAssocRing.{u3} A (CommRing.toRing.{u3} A _inst_15))))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15)) _inst_16) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12)))) (Pi.addCommMonoid.{u2, u3} M (fun (ᾰ : M) => A) (fun (i : M) => AddCommGroup.toAddCommMonoid.{u3} A (NonUnitalNonAssocRing.toAddCommGroup.{u3} A (NonAssocRing.toNonUnitalNonAssocRing.{u3} A (Ring.toNonAssocRing.{u3} A (CommRing.toRing.{u3} A _inst_15)))))) (LinearMap.module.{u1, u1, u3, u2, u3} R R A M A (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13 (AddCommGroup.toAddCommMonoid.{u3} A (NonUnitalNonAssocRing.toAddCommGroup.{u3} A (NonAssocRing.toNonUnitalNonAssocRing.{u3} A (Ring.toNonAssocRing.{u3} A (CommRing.toRing.{u3} A _inst_15))))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15)) _inst_16) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12))) (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15)) (Semiring.toModule.{u3} A (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15))) (LinearMap.ltoFun._proof_1.{u1, u3} R A _inst_12 _inst_15 _inst_16)) (Pi.Function.module.{u2, u3, u3} M A A (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15)) (AddCommGroup.toAddCommMonoid.{u3} A (NonUnitalNonAssocRing.toAddCommGroup.{u3} A (NonAssocRing.toNonUnitalNonAssocRing.{u3} A (Ring.toNonAssocRing.{u3} A (CommRing.toRing.{u3} A _inst_15))))) (Semiring.toModule.{u3} A (Ring.toSemiring.{u3} A (CommRing.toRing.{u3} A _inst_15))))
 but is expected to have type
-  forall (R : Type.{u1}) (M : Type.{u2}) (A : Type.{u3}) [_inst_12 : CommSemiring.{u1} R] [_inst_13 : AddCommMonoid.{u2} M] [_inst_14 : Module.{u1, u2} R M (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13] [_inst_15 : CommSemiring.{u3} A] [_inst_16 : Algebra.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15)], LinearMap.{u3, u3, max u3 u2, max u2 u3} A A (CommSemiring.toSemiring.{u3} A _inst_15) (CommSemiring.toSemiring.{u3} A _inst_15) (RingHom.id.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15))) (LinearMap.{u1, u1, u2, u3} R R (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12))) M A _inst_13 (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16)) (M -> A) (LinearMap.addCommMonoid.{u1, u1, u2, u3} R R M A (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13 (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12)))) (Pi.addCommMonoid.{u2, u3} M (fun (ᾰ : M) => A) (fun (i : M) => NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15))))) (LinearMap.instModuleLinearMapAddCommMonoid.{u1, u1, u3, u2, u3} R R A M A (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13 (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12))) (CommSemiring.toSemiring.{u3} A _inst_15) (Semiring.toModule.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)) (IsScalarTower.to_smulCommClass.{u1, u3, u3} R _inst_12 A (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16 A (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) (Semiring.toModule.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)) (Algebra.toModule.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16) (IsScalarTower.right.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16))) (Pi.module.{u2, u3, u3} M (fun (a._@.Mathlib.Algebra.Algebra.Basic._hyg.6632 : M) => A) A (CommSemiring.toSemiring.{u3} A _inst_15) (fun (i : M) => NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) (fun (i : M) => Semiring.toModule.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))
+  forall (R : Type.{u1}) (M : Type.{u2}) (A : Type.{u3}) [_inst_12 : CommSemiring.{u1} R] [_inst_13 : AddCommMonoid.{u2} M] [_inst_14 : Module.{u1, u2} R M (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13] [_inst_15 : CommSemiring.{u3} A] [_inst_16 : Algebra.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15)], LinearMap.{u3, u3, max u3 u2, max u2 u3} A A (CommSemiring.toSemiring.{u3} A _inst_15) (CommSemiring.toSemiring.{u3} A _inst_15) (RingHom.id.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15))) (LinearMap.{u1, u1, u2, u3} R R (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12))) M A _inst_13 (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16)) (M -> A) (LinearMap.addCommMonoid.{u1, u1, u2, u3} R R M A (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13 (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12)))) (Pi.addCommMonoid.{u2, u3} M (fun (ᾰ : M) => A) (fun (i : M) => NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15))))) (LinearMap.instModuleLinearMapAddCommMonoid.{u1, u1, u3, u2, u3} R R A M A (CommSemiring.toSemiring.{u1} R _inst_12) (CommSemiring.toSemiring.{u1} R _inst_12) _inst_13 (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) _inst_14 (Algebra.toModule.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_12))) (CommSemiring.toSemiring.{u3} A _inst_15) (Semiring.toModule.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)) (IsScalarTower.to_smulCommClass.{u1, u3, u3} R _inst_12 A (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16 A (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) (Semiring.toModule.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)) (Algebra.toModule.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16) (IsScalarTower.right.{u1, u3} R A _inst_12 (CommSemiring.toSemiring.{u3} A _inst_15) _inst_16))) (Pi.module.{u2, u3, u3} M (fun (a._@.Mathlib.Algebra.Algebra.Basic._hyg.6634 : M) => A) A (CommSemiring.toSemiring.{u3} A _inst_15) (fun (i : M) => NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} A (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} A (Semiring.toNonAssocSemiring.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))) (fun (i : M) => Semiring.toModule.{u3} A (CommSemiring.toSemiring.{u3} A _inst_15)))
 Case conversion may be inaccurate. Consider using '#align linear_map.lto_fun LinearMap.ltoFunₓ'. -/
 /-- `A`-linearly coerce a `R`-linear map from `M` to `A` to a function, given an algebra `A` over
 a commutative semiring `R` and `M` a module over `R`. -/

Mathbin/Algebra/MonoidAlgebra/Ideal.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module algebra.monoid_algebra.ideal
-! leanprover-community/mathlib commit 72c366d0475675f1309d3027d3d7d47ee4423951
+! leanprover-community/mathlib commit 4f81bc21e32048db7344b7867946e992cf5f68cc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.RingTheory.Ideal.Basic
 
 /-!
 # Lemmas about ideals of `monoid_algebra` and `add_monoid_algebra`
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 

Mathbin/Algebra/RingQuot.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.ring_quot
-! leanprover-community/mathlib commit e5820f6c8fcf1b75bcd7738ae4da1c5896191f72
+! leanprover-community/mathlib commit 4f81bc21e32048db7344b7867946e992cf5f68cc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.RingTheory.Ideal.Quotient
 /-!
 # Quotients of non-commutative rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Unfortunately, ideals have only been developed in the commutative case as `ideal`,
 and it's not immediately clear how one should formalise ideals in the non-commutative case.
 
@@ -753,7 +756,7 @@ private irreducible_def star' : RingQuot r → RingQuot r
 
 /- warning: ring_quot.star'_quot -> RingQuot.star'_quot is a dubious translation:
 lean 3 declaration is
-  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] (r : R -> R -> Prop) [_inst_6 : StarRing.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)] (hr : forall (a : R) (b : R), (r a b) -> (r (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarAddMonoid.toHasInvolutiveStar.{u1} R (AddCommMonoid.toAddMonoid.{u1} R (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) a) (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarAddMonoid.toHasInvolutiveStar.{u1} R (AddCommMonoid.toAddMonoid.{u1} R (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) b))) {a : R}, Eq.{succ u1} (RingQuot.{u1} R _inst_1 r) (_Private.2632819077.star'.{u1} R _inst_1 r _inst_6 hr (RingQuot.mk.{u1} R _inst_1 r (Quot.mk.{succ u1} R (RingQuot.Rel.{u1} R _inst_1 r) a))) (RingQuot.mk.{u1} R _inst_1 r (Quot.mk.{succ u1} R (RingQuot.Rel.{u1} R _inst_1 r) (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarAddMonoid.toHasInvolutiveStar.{u1} R (AddCommMonoid.toAddMonoid.{u1} R (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) a)))
+  forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] (r : R -> R -> Prop) [_inst_6 : StarRing.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)] (hr : forall (a : R) (b : R), (r a b) -> (r (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarAddMonoid.toHasInvolutiveStar.{u1} R (AddCommMonoid.toAddMonoid.{u1} R (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) a) (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarAddMonoid.toHasInvolutiveStar.{u1} R (AddCommMonoid.toAddMonoid.{u1} R (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) b))) {a : R}, Eq.{succ u1} (RingQuot.{u1} R _inst_1 r) (_Private.4149469211.star'.{u1} R _inst_1 r _inst_6 hr (RingQuot.mk.{u1} R _inst_1 r (Quot.mk.{succ u1} R (RingQuot.Rel.{u1} R _inst_1 r) a))) (RingQuot.mk.{u1} R _inst_1 r (Quot.mk.{succ u1} R (RingQuot.Rel.{u1} R _inst_1 r) (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarAddMonoid.toHasInvolutiveStar.{u1} R (AddCommMonoid.toAddMonoid.{u1} R (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) a)))
 but is expected to have type
   forall {R : Type.{u1}} [_inst_1 : Semiring.{u1} R] (r : R -> R -> Prop) [_inst_6 : StarRing.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1)] (hr : forall (a : R) (b : R), (r a b) -> (r (Star.star.{u1} R (InvolutiveStar.toStar.{u1} R (StarAddMonoid.toInvolutiveStar.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) a) (Star.star.{u1} R (InvolutiveStar.toStar.{u1} R (StarAddMonoid.toInvolutiveStar.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) b))) {a : R}, Eq.{succ u1} (RingQuot.{u1} R _inst_1 r) (_private.Mathlib.Algebra.RingQuot.0.RingQuot.star'.{u1} R _inst_1 r _inst_6 hr (RingQuot.mk.{u1} R _inst_1 r (Quot.mk.{succ u1} R (RingQuot.Rel.{u1} R _inst_1 r) a))) (RingQuot.mk.{u1} R _inst_1 r (Quot.mk.{succ u1} R (RingQuot.Rel.{u1} R _inst_1 r) (Star.star.{u1} R (InvolutiveStar.toStar.{u1} R (StarAddMonoid.toInvolutiveStar.{u1} R (AddMonoidWithOne.toAddMonoid.{u1} R (AddCommMonoidWithOne.toAddMonoidWithOne.{u1} R (NonAssocSemiring.toAddCommMonoidWithOne.{u1} R (Semiring.toNonAssocSemiring.{u1} R _inst_1)))) (StarRing.toStarAddMonoid.{u1} R (Semiring.toNonUnitalSemiring.{u1} R _inst_1) _inst_6))) a)))
 Case conversion may be inaccurate. Consider using '#align ring_quot.star'_quot RingQuot.star'_quotₓ'. -/

Mathbin/AlgebraicTopology/DoldKan/Decomposition.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 
 ! This file was ported from Lean 3 source module algebraic_topology.dold_kan.decomposition
-! leanprover-community/mathlib commit 9af20344b24ef1801b599d296aaed8b9fffdc360
+! leanprover-community/mathlib commit 4f81bc21e32048db7344b7867946e992cf5f68cc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.AlgebraicTopology.DoldKan.PInfty
 
 # Decomposition of the Q endomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we obtain a lemma `decomposition_Q` which expresses
 explicitly the projection `(Q q).f (n+1) : X _[n+1] ⟶ X _[n+1]`
 (`X : simplicial_object C` with `C` a preadditive category) as

Mathbin/AlgebraicTopology/DoldKan/Degeneracies.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 
 ! This file was ported from Lean 3 source module algebraic_topology.dold_kan.degeneracies
-! leanprover-community/mathlib commit ec1c7d810034d4202b0dd239112d1792be9f6fdc
+! leanprover-community/mathlib commit 4f81bc21e32048db7344b7867946e992cf5f68cc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Tactic.FinCases
 
 # Behaviour of P_infty with respect to degeneracies
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For any `X : simplicial_object C` where `C` is an abelian category,
 the projector `P_infty : K[X] ⟶ K[X]` is supposed to be the projection
 on the normalized subcomplex, parallel to the degenerate subcomplex, i.e.

Mathbin/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean

@@ -62,7 +62,7 @@ def equivalence : Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ)
     symm
     change 𝟙 _ = α.hom ≫ β.hom
     rw [← iso.inv_comp_eq, comp_id, ← comp_id β.hom, ← iso.inv_comp_eq]
-    exact AlgebraicTopology.DoldKan.identity_n₂_objectwise P
+    exact AlgebraicTopology.DoldKan.identity_N₂_objectwise P
 #align category_theory.preadditive.dold_kan.equivalence CategoryTheory.Preadditive.DoldKan.equivalence
 
 end DoldKan