bump to nightly-2023-04-14-00

mathlib commit leanprover-community/mathlib@347636a

Mathbin/Algebra/Hom/Equiv/Basic.lean

@@ -155,7 +155,7 @@ instance (priority := 100) [MulOneClass M] [MulOneClass N] [MulEquivClass F M N]
 lean 3 declaration is
   forall (F : Type.{u1}) {α : Type.{u2}} {β : Type.{u3}} [_inst_1 : MulZeroOneClass.{u2} α] [_inst_2 : MulZeroOneClass.{u3} β] [_inst_3 : MulEquivClass.{u1, u2, u3} F α β (MulZeroClass.toHasMul.{u2} α (MulZeroOneClass.toMulZeroClass.{u2} α _inst_1)) (MulZeroClass.toHasMul.{u3} β (MulZeroOneClass.toMulZeroClass.{u3} β _inst_2))], MonoidWithZeroHomClass.{u1, u2, u3} F α β _inst_1 _inst_2
 but is expected to have type
-  forall (F : Type.{u1}) {α : Type.{u2}} {β : Type.{u3}} {_inst_1 : MulZeroOneClass.{u2} α} {_inst_2 : MulZeroOneClass.{u3} β} [_inst_3 : MulEquivClass.{u1, u2, u3} F α β (MulZeroClass.toMul.{u2} α (MulZeroOneClass.toMulZeroClass.{u2} α _inst_1)) (MulZeroClass.toMul.{u3} β (MulZeroOneClass.toMulZeroClass.{u3} β _inst_2))], MonoidWithZeroHomClass.{u1, u2, u3} F α β _inst_1 _inst_2
+  forall (F : Type.{u1}) {α : Type.{u2}} {β : Type.{u3}} [_inst_1 : MulZeroOneClass.{u2} α] [_inst_2 : MulZeroOneClass.{u3} β] [_inst_3 : MulEquivClass.{u1, u2, u3} F α β (MulZeroClass.toMul.{u2} α (MulZeroOneClass.toMulZeroClass.{u2} α _inst_1)) (MulZeroClass.toMul.{u3} β (MulZeroOneClass.toMulZeroClass.{u3} β _inst_2))], MonoidWithZeroHomClass.{u1, u2, u3} F α β _inst_1 _inst_2
 Case conversion may be inaccurate. Consider using '#align mul_equiv_class.to_monoid_with_zero_hom_class MulEquivClass.toMonoidWithZeroHomClassₓ'. -/
 -- See note [lower instance priority]
 instance (priority := 100) toMonoidWithZeroHomClass {α β : Type _} [MulZeroOneClass α]

Mathbin/Algebra/Module/LinearMap.lean

@@ -195,7 +195,7 @@ include i
 lean 3 declaration is
   forall {R : Type.{u1}} {S : Type.{u2}} {M : Type.{u3}} {M₃ : Type.{u4}} {F : Type.{u5}} [_inst_1 : Semiring.{u1} R] [_inst_2 : Semiring.{u2} S] [_inst_3 : AddCommMonoid.{u3} M] [_inst_6 : AddCommMonoid.{u4} M₃] [_inst_10 : Module.{u1, u3} R M _inst_1 _inst_3] [_inst_12 : Module.{u2, u4} S M₃ _inst_2 _inst_6] {σ : RingHom.{u1, u2} R S (Semiring.toNonAssocSemiring.{u1} R _inst_1) (Semiring.toNonAssocSemiring.{u2} S _inst_2)} (f : F) [i : SemilinearMapClass.{u5, u1, u2, u3, u4} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12] {σ' : RingHom.{u2, u1} S R (Semiring.toNonAssocSemiring.{u2} S _inst_2) (Semiring.toNonAssocSemiring.{u1} R _inst_1)} [_inst_13 : RingHomInvPair.{u1, u2} R S _inst_1 _inst_2 σ σ'] (c : S) (x : M), Eq.{succ u4} M₃ (SMul.smul.{u2, u4} S M₃ (SMulZeroClass.toHasSmul.{u2, u4} S M₃ (AddZeroClass.toHasZero.{u4} M₃ (AddMonoid.toAddZeroClass.{u4} M₃ (AddCommMonoid.toAddMonoid.{u4} M₃ _inst_6))) (SMulWithZero.toSmulZeroClass.{u2, u4} S M₃ (MulZeroClass.toHasZero.{u2} S (MulZeroOneClass.toMulZeroClass.{u2} S (MonoidWithZero.toMulZeroOneClass.{u2} S (Semiring.toMonoidWithZero.{u2} S _inst_2)))) (AddZeroClass.toHasZero.{u4} M₃ (AddMonoid.toAddZeroClass.{u4} M₃ (AddCommMonoid.toAddMonoid.{u4} M₃ _inst_6))) (MulActionWithZero.toSMulWithZero.{u2, u4} S M₃ (Semiring.toMonoidWithZero.{u2} S _inst_2) (AddZeroClass.toHasZero.{u4} M₃ (AddMonoid.toAddZeroClass.{u4} M₃ (AddCommMonoid.toAddMonoid.{u4} M₃ _inst_6))) (Module.toMulActionWithZero.{u2, u4} S M₃ _inst_2 _inst_6 _inst_12)))) c (coeFn.{succ u5, max (succ u3) (succ u4)} F (fun (_x : F) => M -> M₃) (FunLike.hasCoeToFun.{succ u5, succ u3, succ u4} F M (fun (_x : M) => M₃) (AddHomClass.toFunLike.{u5, u3, u4} F M M₃ (AddZeroClass.toHasAdd.{u3} M (AddMonoid.toAddZeroClass.{u3} M (AddCommMonoid.toAddMonoid.{u3} M _inst_3))) (AddZeroClass.toHasAdd.{u4} M₃ (AddMonoid.toAddZeroClass.{u4} M₃ (AddCommMonoid.toAddMonoid.{u4} M₃ _inst_6))) (SemilinearMapClass.toAddHomClass.{u5, u1, u2, u3, u4} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12 i))) f x)) (coeFn.{succ u5, max (succ u3) (succ u4)} F (fun (_x : F) => M -> M₃) (FunLike.hasCoeToFun.{succ u5, succ u3, succ u4} F M (fun (_x : M) => M₃) (AddHomClass.toFunLike.{u5, u3, u4} F M M₃ (AddZeroClass.toHasAdd.{u3} M (AddMonoid.toAddZeroClass.{u3} M (AddCommMonoid.toAddMonoid.{u3} M _inst_3))) (AddZeroClass.toHasAdd.{u4} M₃ (AddMonoid.toAddZeroClass.{u4} M₃ (AddCommMonoid.toAddMonoid.{u4} M₃ _inst_6))) (SemilinearMapClass.toAddHomClass.{u5, u1, u2, u3, u4} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12 i))) f (SMul.smul.{u1, u3} R M (SMulZeroClass.toHasSmul.{u1, u3} R M (AddZeroClass.toHasZero.{u3} M (AddMonoid.toAddZeroClass.{u3} M (AddCommMonoid.toAddMonoid.{u3} M _inst_3))) (SMulWithZero.toSmulZeroClass.{u1, u3} R M (MulZeroClass.toHasZero.{u1} R (MulZeroOneClass.toMulZeroClass.{u1} R (MonoidWithZero.toMulZeroOneClass.{u1} R (Semiring.toMonoidWithZero.{u1} R _inst_1)))) (AddZeroClass.toHasZero.{u3} M (AddMonoid.toAddZeroClass.{u3} M (AddCommMonoid.toAddMonoid.{u3} M _inst_3))) (MulActionWithZero.toSMulWithZero.{u1, u3} R M (Semiring.toMonoidWithZero.{u1} R _inst_1) (AddZeroClass.toHasZero.{u3} M (AddMonoid.toAddZeroClass.{u3} M (AddCommMonoid.toAddMonoid.{u3} M _inst_3))) (Module.toMulActionWithZero.{u1, u3} R M _inst_1 _inst_3 _inst_10)))) (coeFn.{max (succ u2) (succ u1), max (succ u2) (succ u1)} (RingHom.{u2, u1} S R (Semiring.toNonAssocSemiring.{u2} S _inst_2) (Semiring.toNonAssocSemiring.{u1} R _inst_1)) (fun (_x : RingHom.{u2, u1} S R (Semiring.toNonAssocSemiring.{u2} S _inst_2) (Semiring.toNonAssocSemiring.{u1} R _inst_1)) => S -> R) (RingHom.hasCoeToFun.{u2, u1} S R (Semiring.toNonAssocSemiring.{u2} S _inst_2) (Semiring.toNonAssocSemiring.{u1} R _inst_1)) σ' c) x))
 but is expected to have type
-  forall {R : Type.{u4}} {S : Type.{u5}} {M : Type.{u1}} {M₃ : Type.{u3}} {F : Type.{u2}} {_inst_1 : Semiring.{u4} R} {_inst_2 : Semiring.{u5} S} {_inst_3 : AddCommMonoid.{u1} M} {_inst_6 : AddCommMonoid.{u3} M₃} {_inst_10 : Module.{u4, u1} R M _inst_1 _inst_3} {_inst_12 : Module.{u5, u3} S M₃ _inst_2 _inst_6} {σ : RingHom.{u4, u5} R S (Semiring.toNonAssocSemiring.{u4} R _inst_1) (Semiring.toNonAssocSemiring.{u5} S _inst_2)} (f : F) [i : SemilinearMapClass.{u2, u4, u5, u1, u3} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12] {σ' : RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)} [_inst_13 : RingHomInvPair.{u4, u5} R S _inst_1 _inst_2 σ σ'] (c : S) (x : M), Eq.{succ u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (HSMul.hSMul.{u5, u3, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (instHSMul.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (SMulZeroClass.toSMul.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (AddMonoid.toZero.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (AddCommMonoid.toAddMonoid.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) _inst_6)) (SMulWithZero.toSMulZeroClass.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (MonoidWithZero.toZero.{u5} S (Semiring.toMonoidWithZero.{u5} S _inst_2)) (AddMonoid.toZero.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (AddCommMonoid.toAddMonoid.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) _inst_6)) (MulActionWithZero.toSMulWithZero.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (Semiring.toMonoidWithZero.{u5} S _inst_2) (AddMonoid.toZero.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (AddCommMonoid.toAddMonoid.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) _inst_6)) (Module.toMulActionWithZero.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) _inst_2 _inst_6 _inst_12))))) c (FunLike.coe.{succ u2, succ u1, succ u3} F M (fun (_x : M) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) _x) (AddHomClass.toFunLike.{u2, u1, u3} F M M₃ (AddZeroClass.toAdd.{u1} M (AddMonoid.toAddZeroClass.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3))) (AddZeroClass.toAdd.{u3} M₃ (AddMonoid.toAddZeroClass.{u3} M₃ (AddCommMonoid.toAddMonoid.{u3} M₃ _inst_6))) (SemilinearMapClass.toAddHomClass.{u2, u4, u5, u1, u3} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12 i)) f x)) (FunLike.coe.{succ u2, succ u1, succ u3} F M (fun (_x : M) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) _x) (AddHomClass.toFunLike.{u2, u1, u3} F M M₃ (AddZeroClass.toAdd.{u1} M (AddMonoid.toAddZeroClass.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3))) (AddZeroClass.toAdd.{u3} M₃ (AddMonoid.toAddZeroClass.{u3} M₃ (AddCommMonoid.toAddMonoid.{u3} M₃ _inst_6))) (SemilinearMapClass.toAddHomClass.{u2, u4, u5, u1, u3} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12 i)) f (HSMul.hSMul.{u4, u1, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M M (instHSMul.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M (SMulZeroClass.toSMul.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M (AddMonoid.toZero.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3)) (SMulWithZero.toSMulZeroClass.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M (MonoidWithZero.toZero.{u4} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) (Semiring.toMonoidWithZero.{u4} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) _inst_1)) (AddMonoid.toZero.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3)) (MulActionWithZero.toSMulWithZero.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M (Semiring.toMonoidWithZero.{u4} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) _inst_1) (AddMonoid.toZero.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3)) (Module.toMulActionWithZero.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M _inst_1 _inst_3 _inst_10))))) (FunLike.coe.{max (succ u4) (succ u5), succ u5, succ u4} (RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)) S (fun (_x : S) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) _x) (MulHomClass.toFunLike.{max u4 u5, u5, u4} (RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)) S R (NonUnitalNonAssocSemiring.toMul.{u5} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u5} S (Semiring.toNonAssocSemiring.{u5} S _inst_2))) (NonUnitalNonAssocSemiring.toMul.{u4} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u4} R (Semiring.toNonAssocSemiring.{u4} R _inst_1))) (NonUnitalRingHomClass.toMulHomClass.{max u4 u5, u5, u4} (RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)) S R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u5} S (Semiring.toNonAssocSemiring.{u5} S _inst_2)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u4} R (Semiring.toNonAssocSemiring.{u4} R _inst_1)) (RingHomClass.toNonUnitalRingHomClass.{max u4 u5, u5, u4} (RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)) S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1) (RingHom.instRingHomClassRingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1))))) σ' c) x))
+  forall {R : Type.{u4}} {S : Type.{u5}} {M : Type.{u1}} {M₃ : Type.{u3}} {F : Type.{u2}} [_inst_1 : Semiring.{u4} R] [_inst_2 : Semiring.{u5} S] [_inst_3 : AddCommMonoid.{u1} M] [_inst_6 : AddCommMonoid.{u3} M₃] [_inst_10 : Module.{u4, u1} R M _inst_1 _inst_3] [_inst_12 : Module.{u5, u3} S M₃ _inst_2 _inst_6] {σ : RingHom.{u4, u5} R S (Semiring.toNonAssocSemiring.{u4} R _inst_1) (Semiring.toNonAssocSemiring.{u5} S _inst_2)} (f : F) [i : SemilinearMapClass.{u2, u4, u5, u1, u3} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12] {σ' : RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)} [_inst_13 : RingHomInvPair.{u4, u5} R S _inst_1 _inst_2 σ σ'] (c : S) (x : M), Eq.{succ u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (HSMul.hSMul.{u5, u3, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (instHSMul.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (SMulZeroClass.toSMul.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (AddMonoid.toZero.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (AddCommMonoid.toAddMonoid.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) _inst_6)) (SMulWithZero.toSMulZeroClass.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (MonoidWithZero.toZero.{u5} S (Semiring.toMonoidWithZero.{u5} S _inst_2)) (AddMonoid.toZero.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (AddCommMonoid.toAddMonoid.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) _inst_6)) (MulActionWithZero.toSMulWithZero.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (Semiring.toMonoidWithZero.{u5} S _inst_2) (AddMonoid.toZero.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) (AddCommMonoid.toAddMonoid.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) _inst_6)) (Module.toMulActionWithZero.{u5, u3} S ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) x) _inst_2 _inst_6 _inst_12))))) c (FunLike.coe.{succ u2, succ u1, succ u3} F M (fun (_x : M) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) _x) (AddHomClass.toFunLike.{u2, u1, u3} F M M₃ (AddZeroClass.toAdd.{u1} M (AddMonoid.toAddZeroClass.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3))) (AddZeroClass.toAdd.{u3} M₃ (AddMonoid.toAddZeroClass.{u3} M₃ (AddCommMonoid.toAddMonoid.{u3} M₃ _inst_6))) (SemilinearMapClass.toAddHomClass.{u2, u4, u5, u1, u3} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12 i)) f x)) (FunLike.coe.{succ u2, succ u1, succ u3} F M (fun (_x : M) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.403 : M) => M₃) _x) (AddHomClass.toFunLike.{u2, u1, u3} F M M₃ (AddZeroClass.toAdd.{u1} M (AddMonoid.toAddZeroClass.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3))) (AddZeroClass.toAdd.{u3} M₃ (AddMonoid.toAddZeroClass.{u3} M₃ (AddCommMonoid.toAddMonoid.{u3} M₃ _inst_6))) (SemilinearMapClass.toAddHomClass.{u2, u4, u5, u1, u3} F R S _inst_1 _inst_2 σ M M₃ _inst_3 _inst_6 _inst_10 _inst_12 i)) f (HSMul.hSMul.{u4, u1, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M M (instHSMul.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M (SMulZeroClass.toSMul.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M (AddMonoid.toZero.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3)) (SMulWithZero.toSMulZeroClass.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M (MonoidWithZero.toZero.{u4} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) (Semiring.toMonoidWithZero.{u4} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) _inst_1)) (AddMonoid.toZero.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3)) (MulActionWithZero.toSMulWithZero.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M (Semiring.toMonoidWithZero.{u4} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) _inst_1) (AddMonoid.toZero.{u1} M (AddCommMonoid.toAddMonoid.{u1} M _inst_3)) (Module.toMulActionWithZero.{u4, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) c) M _inst_1 _inst_3 _inst_10))))) (FunLike.coe.{max (succ u4) (succ u5), succ u5, succ u4} (RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)) S (fun (_x : S) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : S) => R) _x) (MulHomClass.toFunLike.{max u4 u5, u5, u4} (RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)) S R (NonUnitalNonAssocSemiring.toMul.{u5} S (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u5} S (Semiring.toNonAssocSemiring.{u5} S _inst_2))) (NonUnitalNonAssocSemiring.toMul.{u4} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u4} R (Semiring.toNonAssocSemiring.{u4} R _inst_1))) (NonUnitalRingHomClass.toMulHomClass.{max u4 u5, u5, u4} (RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)) S R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u5} S (Semiring.toNonAssocSemiring.{u5} S _inst_2)) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u4} R (Semiring.toNonAssocSemiring.{u4} R _inst_1)) (RingHomClass.toNonUnitalRingHomClass.{max u4 u5, u5, u4} (RingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1)) S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1) (RingHom.instRingHomClassRingHom.{u5, u4} S R (Semiring.toNonAssocSemiring.{u5} S _inst_2) (Semiring.toNonAssocSemiring.{u4} R _inst_1))))) σ' c) x))
 Case conversion may be inaccurate. Consider using '#align semilinear_map_class.map_smul_inv SemilinearMapClass.map_smul_invₓ'. -/
 theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
     c • f x = f (σ' c • x) := by simp