bump to nightly-2023-05-24-01

mathlib commit leanprover-community/mathlib@75e7fca

Mathbin/Algebra/Algebra/Basic.lean

@@ -1508,7 +1508,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)) (Algebra.to_smulCommClass.{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.6659 : 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)) (Algebra.to_smulCommClass.{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.6660 : 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/Analysis/Normed/Field/Basic.lean

@@ -917,7 +917,7 @@ theorem nndist_inv_inv₀ {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) :
 lean 3 declaration is
   forall {α : Type.{u1}} [_inst_1 : NormedDivisionRing.{u1} α] {a : α}, (Ne.{succ u1} α a (OfNat.ofNat.{u1} α 0 (OfNat.mk.{u1} α 0 (Zero.zero.{u1} α (MulZeroClass.toHasZero.{u1} α (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} α (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} α (NonAssocRing.toNonUnitalNonAssocRing.{u1} α (Ring.toNonAssocRing.{u1} α (NormedRing.toRing.{u1} α (NormedDivisionRing.toNormedRing.{u1} α _inst_1))))))))))) -> (Filter.Tendsto.{u1, u1} α α (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (Distrib.toHasMul.{u1} α (Ring.toDistrib.{u1} α (NormedRing.toRing.{u1} α (NormedDivisionRing.toNormedRing.{u1} α _inst_1))))) a) (Filter.comap.{u1, 0} α Real (Norm.norm.{u1} α (NormedDivisionRing.toHasNorm.{u1} α _inst_1)) (Filter.atTop.{0} Real Real.preorder)) (Filter.comap.{u1, 0} α Real (Norm.norm.{u1} α (NormedDivisionRing.toHasNorm.{u1} α _inst_1)) (Filter.atTop.{0} Real Real.preorder)))
 but is expected to have type
-  forall {α : Type.{u1}} [_inst_1 : NormedDivisionRing.{u1} α] {a : α}, (Ne.{succ u1} α a (OfNat.ofNat.{u1} α 0 (Zero.toOfNat0.{u1} α (MonoidWithZero.toZero.{u1} α (Semiring.toMonoidWithZero.{u1} α (DivisionSemiring.toSemiring.{u1} α (DivisionRing.toDivisionSemiring.{u1} α (NormedDivisionRing.toDivisionRing.{u1} α _inst_1)))))))) -> (Filter.Tendsto.{u1, u1} α α ((fun (x._@.Mathlib.Analysis.Normed.Field.Basic._hyg.5143 : α) (x._@.Mathlib.Analysis.Normed.Field.Basic._hyg.5145 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (NonUnitalNonAssocRing.toMul.{u1} α (NonAssocRing.toNonUnitalNonAssocRing.{u1} α (Ring.toNonAssocRing.{u1} α (NormedRing.toRing.{u1} α (NormedDivisionRing.toNormedRing.{u1} α _inst_1)))))) x._@.Mathlib.Analysis.Normed.Field.Basic._hyg.5143 x._@.Mathlib.Analysis.Normed.Field.Basic._hyg.5145) a) (Filter.comap.{u1, 0} α Real (Norm.norm.{u1} α (NormedDivisionRing.toNorm.{u1} α _inst_1)) (Filter.atTop.{0} Real Real.instPreorderReal)) (Filter.comap.{u1, 0} α Real (Norm.norm.{u1} α (NormedDivisionRing.toNorm.{u1} α _inst_1)) (Filter.atTop.{0} Real Real.instPreorderReal)))
+  forall {α : Type.{u1}} [_inst_1 : NormedDivisionRing.{u1} α] {a : α}, (Ne.{succ u1} α a (OfNat.ofNat.{u1} α 0 (Zero.toOfNat0.{u1} α (MonoidWithZero.toZero.{u1} α (Semiring.toMonoidWithZero.{u1} α (DivisionSemiring.toSemiring.{u1} α (DivisionRing.toDivisionSemiring.{u1} α (NormedDivisionRing.toDivisionRing.{u1} α _inst_1)))))))) -> (Filter.Tendsto.{u1, u1} α α ((fun (x._@.Mathlib.Analysis.Normed.Field.Basic._hyg.5145 : α) (x._@.Mathlib.Analysis.Normed.Field.Basic._hyg.5147 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (NonUnitalNonAssocRing.toMul.{u1} α (NonAssocRing.toNonUnitalNonAssocRing.{u1} α (Ring.toNonAssocRing.{u1} α (NormedRing.toRing.{u1} α (NormedDivisionRing.toNormedRing.{u1} α _inst_1)))))) x._@.Mathlib.Analysis.Normed.Field.Basic._hyg.5145 x._@.Mathlib.Analysis.Normed.Field.Basic._hyg.5147) a) (Filter.comap.{u1, 0} α Real (Norm.norm.{u1} α (NormedDivisionRing.toNorm.{u1} α _inst_1)) (Filter.atTop.{0} Real Real.instPreorderReal)) (Filter.comap.{u1, 0} α Real (Norm.norm.{u1} α (NormedDivisionRing.toNorm.{u1} α _inst_1)) (Filter.atTop.{0} Real Real.instPreorderReal)))
 Case conversion may be inaccurate. Consider using '#align filter.tendsto_mul_left_cobounded Filter.tendsto_mul_left_coboundedₓ'. -/
 /-- Multiplication on the left by a nonzero element of a normed division ring tends to infinity at
 infinity. TODO: use `bornology.cobounded` instead of `filter.comap has_norm.norm filter.at_top`. -/

Mathbin/GroupTheory/GroupAction/Defs.lean

@@ -609,7 +609,7 @@ theorem one_smul (b : α) : (1 : M) • b = b :=
 lean 3 declaration is
   forall (M : Type.{u1}) {α : Type.{u2}} [_inst_1 : Monoid.{u1} M] [_inst_2 : MulAction.{u1, u2} M α _inst_1], Eq.{succ u2} (α -> α) (SMul.smul.{u1, u2} M α (MulAction.toHasSmul.{u1, u2} M α _inst_1 _inst_2) (OfNat.ofNat.{u1} M 1 (OfNat.mk.{u1} M 1 (One.one.{u1} M (MulOneClass.toHasOne.{u1} M (Monoid.toMulOneClass.{u1} M _inst_1)))))) (id.{succ u2} α)
 but is expected to have type
-  forall (M : Type.{u1}) {α : Type.{u2}} [_inst_1 : Monoid.{u1} M] [_inst_2 : MulAction.{u1, u2} M α _inst_1], Eq.{succ u2} (α -> α) ((fun (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2723 : M) (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2725 : α) => HSMul.hSMul.{u1, u2, u2} M α α (instHSMul.{u1, u2} M α (MulAction.toSMul.{u1, u2} M α _inst_1 _inst_2)) x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2723 x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2725) (OfNat.ofNat.{u1} M 1 (One.toOfNat1.{u1} M (Monoid.toOne.{u1} M _inst_1)))) (id.{succ u2} α)
+  forall (M : Type.{u1}) {α : Type.{u2}} [_inst_1 : Monoid.{u1} M] [_inst_2 : MulAction.{u1, u2} M α _inst_1], Eq.{succ u2} (α -> α) ((fun (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2721 : M) (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2723 : α) => HSMul.hSMul.{u1, u2, u2} M α α (instHSMul.{u1, u2} M α (MulAction.toSMul.{u1, u2} M α _inst_1 _inst_2)) x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2721 x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2723) (OfNat.ofNat.{u1} M 1 (One.toOfNat1.{u1} M (Monoid.toOne.{u1} M _inst_1)))) (id.{succ u2} α)
 Case conversion may be inaccurate. Consider using '#align one_smul_eq_id one_smul_eq_idₓ'. -/
 /-- `has_smul` version of `one_mul_eq_id` -/
 @[to_additive "`has_vadd` version of `zero_add_eq_id`"]
@@ -622,7 +622,7 @@ theorem one_smul_eq_id : ((· • ·) (1 : M) : α → α) = id :=
 lean 3 declaration is
   forall (M : Type.{u1}) {α : Type.{u2}} [_inst_1 : Monoid.{u1} M] [_inst_2 : MulAction.{u1, u2} M α _inst_1] (a₁ : M) (a₂ : M), Eq.{succ u2} (α -> α) (Function.comp.{succ u2, succ u2, succ u2} α α α (SMul.smul.{u1, u2} M α (MulAction.toHasSmul.{u1, u2} M α _inst_1 _inst_2) a₁) (SMul.smul.{u1, u2} M α (MulAction.toHasSmul.{u1, u2} M α _inst_1 _inst_2) a₂)) (SMul.smul.{u1, u2} M α (MulAction.toHasSmul.{u1, u2} M α _inst_1 _inst_2) (HMul.hMul.{u1, u1, u1} M M M (instHMul.{u1} M (MulOneClass.toHasMul.{u1} M (Monoid.toMulOneClass.{u1} M _inst_1))) a₁ a₂))
 but is expected to have type
-  forall (M : Type.{u1}) {α : Type.{u2}} [_inst_1 : Monoid.{u1} M] [_inst_2 : MulAction.{u1, u2} M α _inst_1] (a₁ : M) (a₂ : M), Eq.{succ u2} (α -> α) (Function.comp.{succ u2, succ u2, succ u2} α α α ((fun (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2775 : M) (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2777 : α) => HSMul.hSMul.{u1, u2, u2} M α α (instHSMul.{u1, u2} M α (MulAction.toSMul.{u1, u2} M α _inst_1 _inst_2)) x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2775 x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2777) a₁) ((fun (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2792 : M) (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2794 : α) => HSMul.hSMul.{u1, u2, u2} M α α (instHSMul.{u1, u2} M α (MulAction.toSMul.{u1, u2} M α _inst_1 _inst_2)) x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2792 x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2794) a₂)) ((fun (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2815 : M) (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2817 : α) => HSMul.hSMul.{u1, u2, u2} M α α (instHSMul.{u1, u2} M α (MulAction.toSMul.{u1, u2} M α _inst_1 _inst_2)) x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2815 x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2817) (HMul.hMul.{u1, u1, u1} M M M (instHMul.{u1} M (MulOneClass.toMul.{u1} M (Monoid.toMulOneClass.{u1} M _inst_1))) a₁ a₂))
+  forall (M : Type.{u1}) {α : Type.{u2}} [_inst_1 : Monoid.{u1} M] [_inst_2 : MulAction.{u1, u2} M α _inst_1] (a₁ : M) (a₂ : M), Eq.{succ u2} (α -> α) (Function.comp.{succ u2, succ u2, succ u2} α α α ((fun (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2773 : M) (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2775 : α) => HSMul.hSMul.{u1, u2, u2} M α α (instHSMul.{u1, u2} M α (MulAction.toSMul.{u1, u2} M α _inst_1 _inst_2)) x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2773 x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2775) a₁) ((fun (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2790 : M) (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2792 : α) => HSMul.hSMul.{u1, u2, u2} M α α (instHSMul.{u1, u2} M α (MulAction.toSMul.{u1, u2} M α _inst_1 _inst_2)) x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2790 x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2792) a₂)) ((fun (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2813 : M) (x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2815 : α) => HSMul.hSMul.{u1, u2, u2} M α α (instHSMul.{u1, u2} M α (MulAction.toSMul.{u1, u2} M α _inst_1 _inst_2)) x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2813 x._@.Mathlib.GroupTheory.GroupAction.Defs._hyg.2815) (HMul.hMul.{u1, u1, u1} M M M (instHMul.{u1} M (MulOneClass.toMul.{u1} M (Monoid.toMulOneClass.{u1} M _inst_1))) a₁ a₂))
 Case conversion may be inaccurate. Consider using '#align comp_smul_left comp_smul_leftₓ'. -/
 /-- `has_smul` version of `comp_mul_left` -/
 @[to_additive "`has_vadd` version of `comp_add_left`"]

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "7604bbe6944d30582d374b1d32f598b8012feb84",
+    "rev": "4bebd17001718a0d149d2afb156b9b4892572445",
     "name": "lean3port",
-    "inputRev?": "7604bbe6944d30582d374b1d32f598b8012feb84"}},
+    "inputRev?": "4bebd17001718a0d149d2afb156b9b4892572445"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "6c2856ce1a52452b6ddb2d32b0f8cf51b2537225",
+    "rev": "598588dbb2339dc229f1a5b06c398dfdbd3718db",
     "name": "mathlib",
-    "inputRev?": "6c2856ce1a52452b6ddb2d32b0f8cf51b2537225"}},
+    "inputRev?": "598588dbb2339dc229f1a5b06c398dfdbd3718db"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,