bump to nightly-2023-04-26-16

mathlib commit leanprover-community/mathlib@d2d964c

Mathbin/Algebra/Algebra/Basic.lean

@@ -1492,7 +1492,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.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)))
+  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.6573 : 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/Field/Defs.lean

@@ -211,7 +211,7 @@ theorem smul_def (a : ℚ) (x : K) : a • x = ↑a * x :=
 lean 3 declaration is
   forall (A : Type.{u1}) [_inst_2 : DivisionRing.{u1} A] (m : Rat), Eq.{succ u1} A (SMul.smul.{0, u1} Rat A (Rat.smulDivisionRing.{u1} A _inst_2) m (OfNat.ofNat.{u1} A 1 (OfNat.mk.{u1} A 1 (One.one.{u1} A (AddMonoidWithOne.toOne.{u1} A (AddGroupWithOne.toAddMonoidWithOne.{u1} A (AddCommGroupWithOne.toAddGroupWithOne.{u1} A (Ring.toAddCommGroupWithOne.{u1} A (DivisionRing.toRing.{u1} A _inst_2))))))))) ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Rat A (HasLiftT.mk.{1, succ u1} Rat A (CoeTCₓ.coe.{1, succ u1} Rat A (Rat.castCoe.{u1} A (DivisionRing.toHasRatCast.{u1} A _inst_2)))) m)
 but is expected to have type
-  forall {A : Type.{u1}} [_inst_2 : DivisionRing.{u1} A] [m : Algebra.{0, u1} Rat A Rat.commSemiring (DivisionSemiring.toSemiring.{u1} A (DivisionRing.toDivisionSemiring.{u1} A _inst_2))] (m_1 : Rat), Eq.{succ u1} A (SMul.smul.{0, u1} Rat A (Algebra.toSMul.{0, u1} Rat A Rat.commSemiring (DivisionSemiring.toSemiring.{u1} A (DivisionRing.toDivisionSemiring.{u1} A _inst_2)) m) m_1 (OfNat.ofNat.{u1} A 1 (One.toOfNat1.{u1} A (NonAssocRing.toOne.{u1} A (Ring.toNonAssocRing.{u1} A (DivisionRing.toRing.{u1} A _inst_2)))))) (Rat.cast.{u1} A (DivisionRing.toRatCast.{u1} A _inst_2) m_1)
+  forall (A : Type.{u1}) [_inst_2 : DivisionRing.{u1} A] (m : Rat), Eq.{succ u1} A (HSMul.hSMul.{0, u1, u1} Rat A A (instHSMul.{0, u1} Rat A (Rat.smulDivisionRing.{u1} A _inst_2)) m (OfNat.ofNat.{u1} A 1 (One.toOfNat1.{u1} A (NonAssocRing.toOne.{u1} A (Ring.toNonAssocRing.{u1} A (DivisionRing.toRing.{u1} A _inst_2)))))) (Rat.cast.{u1} A (DivisionRing.toRatCast.{u1} A _inst_2) m)
 Case conversion may be inaccurate. Consider using '#align rat.smul_one_eq_coe Rat.smul_one_eq_coeₓ'. -/
 @[simp]
 theorem smul_one_eq_coe (A : Type _) [DivisionRing A] (m : ℚ) : m • (1 : A) = ↑m := by