diff --git a/Mathbin/Algebra/DirectSum/Finsupp.lean b/Mathbin/Algebra/DirectSum/Finsupp.lean
index e9acc7b634..768e09ef7f 100644
--- a/Mathbin/Algebra/DirectSum/Finsupp.lean
+++ b/Mathbin/Algebra/DirectSum/Finsupp.lean
@@ -29,29 +29,47 @@ open LinearMap Submodule
 
 variable {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M]
 
-section finsuppLequivDirectSum
+section finsuppLEquivDirectSum
 
 variable (R M) (ι : Type _) [DecidableEq ι]
 
+/- warning: finsupp_lequiv_direct_sum -> finsuppLEquivDirectSum is a dubious translation:
+lean 3 declaration is
+  forall (R : Type.{u1}) (M : Type.{u2}) [_inst_1 : Ring.{u1} R] [_inst_2 : AddCommGroup.{u2} M] [_inst_3 : Module.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)] (ι : Type.{u3}) [_inst_4 : DecidableEq.{succ u3} ι], LinearEquiv.{u1, u1, max u3 u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (finsuppLEquivDirectSum._proof_1.{u1} R _inst_1) (finsuppLEquivDirectSum._proof_2.{u1} R _inst_1) (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3) (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3))
+but is expected to have type
+  forall (R : Type.{u1}) (M : Type.{u2}) [_inst_1 : Ring.{u1} R] [_inst_2 : AddCommGroup.{u2} M] [_inst_3 : Module.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)] (ι : Type.{u3}) [_inst_4 : DecidableEq.{succ u3} ι], LinearEquiv.{u1, u1, max u2 u3, max u2 u3} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHomInvPair.ids.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (RingHomInvPair.ids.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (Finsupp.{u3, u2} ι M (NegZeroClass.toZero.{u2} M (SubNegZeroMonoid.toNegZeroClass.{u2} M (SubtractionMonoid.toSubNegZeroMonoid.{u2} M (SubtractionCommMonoid.toSubtractionMonoid.{u2} M (AddCommGroup.toDivisionAddCommMonoid.{u2} M _inst_2)))))) (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (instAddCommMonoidDirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))
+Case conversion may be inaccurate. Consider using '#align finsupp_lequiv_direct_sum finsuppLEquivDirectSumₓ'. -/
 /-- The finitely supported functions `ι →₀ M` are in linear equivalence with the direct sum of
 copies of M indexed by ι. -/
-def finsuppLequivDirectSum : (ι →₀ M) ≃ₗ[R] ⨁ i : ι, M :=
+def finsuppLEquivDirectSum : (ι →₀ M) ≃ₗ[R] ⨁ i : ι, M :=
   haveI : ∀ m : M, Decidable (m ≠ 0) := Classical.decPred _
   finsuppLequivDfinsupp R
-#align finsupp_lequiv_direct_sum finsuppLequivDirectSum
-
+#align finsupp_lequiv_direct_sum finsuppLEquivDirectSum
+
+/- warning: finsupp_lequiv_direct_sum_single -> finsuppLEquivDirectSum_single is a dubious translation:
+lean 3 declaration is
+  forall (R : Type.{u1}) (M : Type.{u2}) [_inst_1 : Ring.{u1} R] [_inst_2 : AddCommGroup.{u2} M] [_inst_3 : Module.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)] (ι : Type.{u3}) [_inst_4 : DecidableEq.{succ u3} ι] (i : ι) (m : M), Eq.{succ (max u3 u2)} (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (coeFn.{succ (max u3 u2), succ (max u3 u2)} (LinearEquiv.{u1, u1, max u3 u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (finsuppLEquivDirectSum._proof_1.{u1} R _inst_1) (finsuppLEquivDirectSum._proof_2.{u1} R _inst_1) (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3) (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3))) (fun (_x : LinearEquiv.{u1, u1, max u3 u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (finsuppLEquivDirectSum._proof_1.{u1} R _inst_1) (finsuppLEquivDirectSum._proof_2.{u1} R _inst_1) (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3) (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3))) => (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) -> (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2))) (LinearEquiv.hasCoeToFun.{u1, u1, max u3 u2, max u3 u2} R R (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3) (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (finsuppLEquivDirectSum._proof_1.{u1} R _inst_1) (finsuppLEquivDirectSum._proof_2.{u1} R _inst_1)) (finsuppLEquivDirectSum.{u1, u2, u3} R M _inst_1 _inst_2 _inst_3 ι (fun (a : ι) (b : ι) => _inst_4 a b)) (Finsupp.single.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2))))) i m)) (coeFn.{max (succ u2) (succ (max u3 u2)), max (succ u2) (succ (max u3 u2))} (LinearMap.{u1, u1, u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) M (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) _inst_3 (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3))) (fun (_x : LinearMap.{u1, u1, u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) M (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) _inst_3 (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3))) => M -> (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2))) (LinearMap.hasCoeToFun.{u1, u1, u2, max u3 u2} R R M (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) _inst_3 (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) (DirectSum.lof.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (a : ι) (b : ι) => _inst_4 a b) (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3) i) m)
+but is expected to have type
+  forall (R : Type.{u2}) (M : Type.{u3}) [_inst_1 : Ring.{u2} R] [_inst_2 : AddCommGroup.{u3} M] [_inst_3 : Module.{u2, u3} R M (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)] (ι : Type.{u1}) [_inst_4 : DecidableEq.{succ u1} ι] (i : ι) (m : M), Eq.{max (succ u3) (succ u1)} ((fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) => DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.single.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2))))) i m)) (FunLike.coe.{max (succ u3) (succ u1), max (succ u3) (succ u1), max (succ u3) (succ u1)} (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (fun (_x : Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) => (fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) => DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _x) (SMulHomClass.toFunLike.{max u3 u1, u2, max u3 u1, max u3 u1} (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (SMulZeroClass.toSMul.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (AddMonoid.toZero.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (AddCommMonoid.toAddMonoid.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)))) (DistribSMul.toSMulZeroClass.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (AddMonoid.toAddZeroClass.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (AddCommMonoid.toAddMonoid.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)))) (DistribMulAction.toDistribSMul.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2))) (Module.toDistribMulAction.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Ring.toSemiring.{u2} R _inst_1) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3))))) (SMulZeroClass.toSMul.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddMonoid.toZero.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddCommMonoid.toAddMonoid.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)))) (DistribSMul.toSMulZeroClass.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddMonoid.toAddZeroClass.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddCommMonoid.toAddMonoid.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)))) (DistribMulAction.toDistribSMul.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2))) (Module.toDistribMulAction.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)))))) (DistribMulActionHomClass.toSMulHomClass.{max u3 u1, u2, max u3 u1, max u3 u1} (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2))) (AddCommMonoid.toAddMonoid.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2))) (Module.toDistribMulAction.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Ring.toSemiring.{u2} R _inst_1) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3)) (Module.toDistribMulAction.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) (SemilinearMapClass.distribMulActionHomClass.{u2, max u3 u1, max u3 u1, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) (Ring.toSemiring.{u2} R _inst_1) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (SemilinearEquivClass.instSemilinearMapClass.{u2, u2, max u3 u1, max u3 u1, max u3 u1} R R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (LinearEquiv.instSemilinearEquivClassLinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1))))))) (finsuppLEquivDirectSum.{u2, u3, u1} R M _inst_1 _inst_2 _inst_3 ι (fun (a : ι) (b : ι) => _inst_4 a b)) (Finsupp.single.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2))))) i m)) (FunLike.coe.{max (succ u1) (succ u3), succ u3, max (succ u1) (succ u3)} (LinearMap.{u2, u2, u3, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) M (DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _inst_3 (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) M (fun (_x : M) => (fun (x._@.Mathlib.Algebra.Module.LinearMap._hyg.6190 : M) => DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _x) (LinearMap.instFunLikeLinearMap.{u2, u2, u3, max u1 u3} R R M (DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _inst_3 (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1)))) (DirectSum.lof.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (a : ι) (b : ι) => _inst_4 a b) (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3) i) m)
+Case conversion may be inaccurate. Consider using '#align finsupp_lequiv_direct_sum_single finsuppLEquivDirectSum_singleₓ'. -/
 @[simp]
-theorem finsuppLequivDirectSum_single (i : ι) (m : M) :
-    finsuppLequivDirectSum R M ι (Finsupp.single i m) = DirectSum.lof R ι _ i m :=
+theorem finsuppLEquivDirectSum_single (i : ι) (m : M) :
+    finsuppLEquivDirectSum R M ι (Finsupp.single i m) = DirectSum.lof R ι _ i m :=
   Finsupp.toDfinsupp_single i m
-#align finsupp_lequiv_direct_sum_single finsuppLequivDirectSum_single
-
+#align finsupp_lequiv_direct_sum_single finsuppLEquivDirectSum_single
+
+/- warning: finsupp_lequiv_direct_sum_symm_lof -> finsuppLEquivDirectSum_symm_lof is a dubious translation:
+lean 3 declaration is
+  forall (R : Type.{u1}) (M : Type.{u2}) [_inst_1 : Ring.{u1} R] [_inst_2 : AddCommGroup.{u2} M] [_inst_3 : Module.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)] (ι : Type.{u3}) [_inst_4 : DecidableEq.{succ u3} ι] (i : ι) (m : M), Eq.{max (succ u3) (succ u2)} (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (coeFn.{succ (max u3 u2), succ (max u3 u2)} (LinearEquiv.{u1, u1, max u3 u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (finsuppLEquivDirectSum._proof_2.{u1} R _inst_1) (finsuppLEquivDirectSum._proof_1.{u1} R _inst_1) (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3)) (fun (_x : LinearEquiv.{u1, u1, max u3 u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (finsuppLEquivDirectSum._proof_2.{u1} R _inst_1) (finsuppLEquivDirectSum._proof_1.{u1} R _inst_1) (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3)) => (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) -> (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2))))))) (LinearEquiv.hasCoeToFun.{u1, u1, max u3 u2, max u3 u2} R R (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (finsuppLEquivDirectSum._proof_2.{u1} R _inst_1) (finsuppLEquivDirectSum._proof_1.{u1} R _inst_1)) (LinearEquiv.symm.{u1, u1, max u3 u2, max u3 u2} R R (Finsupp.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2)))))) (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (Finsupp.addCommMonoid.{u3, u2} ι M (AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Finsupp.module.{u3, u2, u1} ι M R (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) _inst_3) (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (finsuppLEquivDirectSum._proof_1.{u1} R _inst_1) (finsuppLEquivDirectSum._proof_2.{u1} R _inst_1) (finsuppLEquivDirectSum.{u1, u2, u3} R M _inst_1 _inst_2 _inst_3 ι (fun (a : ι) (b : ι) => _inst_4 a b))) (coeFn.{max (succ u2) (succ (max u3 u2)), max (succ u2) (succ (max u3 u2))} (LinearMap.{u1, u1, u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) M (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) _inst_3 (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3))) (fun (_x : LinearMap.{u1, u1, u2, max u3 u2} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) M (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) _inst_3 (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3))) => M -> (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2))) (LinearMap.hasCoeToFun.{u1, u1, u2, max u3 u2} R R M (DirectSum.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (DirectSum.addCommMonoid.{u3, u2} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2)) _inst_3 (DirectSum.module.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) (DirectSum.lof.{u1, u3, u2} R (Ring.toSemiring.{u1} R _inst_1) ι (fun (a : ι) (b : ι) => _inst_4 a b) (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u2} M _inst_2) (fun (i : ι) => _inst_3) i) m)) (Finsupp.single.{u3, u2} ι M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_2))))) i m)
+but is expected to have type
+  forall (R : Type.{u2}) (M : Type.{u3}) [_inst_1 : Ring.{u2} R] [_inst_2 : AddCommGroup.{u3} M] [_inst_3 : Module.{u2, u3} R M (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)] (ι : Type.{u1}) [_inst_4 : DecidableEq.{succ u1} ι] (i : ι) (m : M), Eq.{max (succ u3) (succ u1)} ((fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) => Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (FunLike.coe.{max (succ u1) (succ u3), succ u3, max (succ u1) (succ u3)} (LinearMap.{u2, u2, u3, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) M (DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _inst_3 (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) M (fun (a : M) => (fun (x._@.Mathlib.Algebra.Module.LinearMap._hyg.6190 : M) => DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) a) (LinearMap.instFunLikeLinearMap.{u2, u2, u3, max u1 u3} R R M (DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _inst_3 (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1)))) (DirectSum.lof.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (a : ι) (b : ι) => _inst_4 a b) (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3) i) m)) (FunLike.coe.{max (succ u3) (succ u1), max (succ u3) (succ u1), max (succ u3) (succ u1)} (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3)) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (fun (_x : DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) => (fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) => Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) _x) (SMulHomClass.toFunLike.{max u3 u1, u2, max u3 u1, max u3 u1} (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3)) R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (SMulZeroClass.toSMul.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddMonoid.toZero.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddCommMonoid.toAddMonoid.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)))) (DistribSMul.toSMulZeroClass.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddMonoid.toAddZeroClass.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddCommMonoid.toAddMonoid.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)))) (DistribMulAction.toDistribSMul.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2))) (Module.toDistribMulAction.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)))))) (SMulZeroClass.toSMul.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (AddMonoid.toZero.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (AddCommMonoid.toAddMonoid.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)))) (DistribSMul.toSMulZeroClass.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (AddMonoid.toAddZeroClass.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (AddCommMonoid.toAddMonoid.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)))) (DistribMulAction.toDistribSMul.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2))) (Module.toDistribMulAction.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Ring.toSemiring.{u2} R _inst_1) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3))))) (DistribMulActionHomClass.toSMulHomClass.{max u3 u1, u2, max u3 u1, max u3 u1} (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3)) R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u3 u1} (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2))) (AddCommMonoid.toAddMonoid.{max u3 u1} (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2))) (Module.toDistribMulAction.{u2, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) (Module.toDistribMulAction.{u2, max u3 u1} R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Ring.toSemiring.{u2} R _inst_1) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3)) (SemilinearMapClass.distribMulActionHomClass.{u2, max u3 u1, max u3 u1, max u3 u1} R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3)) (Ring.toSemiring.{u2} R _inst_1) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (SemilinearEquivClass.instSemilinearMapClass.{u2, u2, max u3 u1, max u3 u1, max u3 u1} R R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (LinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3)) (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (LinearEquiv.instSemilinearEquivClassLinearEquiv.{u2, u2, max u3 u1, max u3 u1} R R (DirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (_i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1))))))) (LinearEquiv.symm.{u2, u2, max u3 u1, max u3 u1} R R (Finsupp.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2)))))) (DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (Finsupp.addCommMonoid.{u1, u3} ι M (AddCommGroup.toAddCommMonoid.{u3} M _inst_2)) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Finsupp.module.{u1, u3, u2} ι M R (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} M _inst_2) _inst_3) (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (RingHomInvPair.ids.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (finsuppLEquivDirectSum.{u2, u3, u1} R M _inst_1 _inst_2 _inst_3 ι (fun (a : ι) (b : ι) => _inst_4 a b))) (FunLike.coe.{max (succ u1) (succ u3), succ u3, max (succ u1) (succ u3)} (LinearMap.{u2, u2, u3, max u3 u1} R R (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1))) M (DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _inst_3 (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3))) M (fun (_x : M) => (fun (x._@.Mathlib.Algebra.Module.LinearMap._hyg.6190 : M) => DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _x) (LinearMap.instFunLikeLinearMap.{u2, u2, u3, max u1 u3} R R M (DirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) (Ring.toSemiring.{u2} R _inst_1) (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (instAddCommMonoidDirectSum.{u1, u3} ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2)) _inst_3 (DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3)) (RingHom.id.{u2} R (Semiring.toNonAssocSemiring.{u2} R (Ring.toSemiring.{u2} R _inst_1)))) (DirectSum.lof.{u2, u1, u3} R (Ring.toSemiring.{u2} R _inst_1) ι (fun (a : ι) (b : ι) => _inst_4 a b) (fun (i : ι) => M) (fun (i : ι) => AddCommGroup.toAddCommMonoid.{u3} ((fun (_i : ι) => M) i) _inst_2) (fun (i : ι) => _inst_3) i) m)) (Finsupp.single.{u1, u3} ι M (NegZeroClass.toZero.{u3} M (SubNegZeroMonoid.toNegZeroClass.{u3} M (SubtractionMonoid.toSubNegZeroMonoid.{u3} M (SubtractionCommMonoid.toSubtractionMonoid.{u3} M (AddCommGroup.toDivisionAddCommMonoid.{u3} M _inst_2))))) i m)
+Case conversion may be inaccurate. Consider using '#align finsupp_lequiv_direct_sum_symm_lof finsuppLEquivDirectSum_symm_lofₓ'. -/
 @[simp]
-theorem finsuppLequivDirectSum_symm_lof (i : ι) (m : M) :
-    (finsuppLequivDirectSum R M ι).symm (DirectSum.lof R ι _ i m) = Finsupp.single i m :=
+theorem finsuppLEquivDirectSum_symm_lof (i : ι) (m : M) :
+    (finsuppLEquivDirectSum R M ι).symm (DirectSum.lof R ι _ i m) = Finsupp.single i m :=
   letI : ∀ m : M, Decidable (m ≠ 0) := Classical.decPred _
   Dfinsupp.toFinsupp_single i m
-#align finsupp_lequiv_direct_sum_symm_lof finsuppLequivDirectSum_symm_lof
+#align finsupp_lequiv_direct_sum_symm_lof finsuppLEquivDirectSum_symm_lof
 
-end finsuppLequivDirectSum
+end finsuppLEquivDirectSum
 
diff --git a/Mathbin/LinearAlgebra/DirectSum/Finsupp.lean b/Mathbin/LinearAlgebra/DirectSum/Finsupp.lean
index ab6946a8b8..f5f407ca91 100644
--- a/Mathbin/LinearAlgebra/DirectSum/Finsupp.lean
+++ b/Mathbin/LinearAlgebra/DirectSum/Finsupp.lean
@@ -39,9 +39,9 @@ open TensorProduct Classical
 /-- The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N). -/
 def finsuppTensorFinsupp (R M N ι κ : Sort _) [CommRing R] [AddCommGroup M] [Module R M]
     [AddCommGroup N] [Module R N] : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ →₀ M ⊗[R] N :=
-  TensorProduct.congr (finsuppLequivDirectSum R M ι) (finsuppLequivDirectSum R N κ) ≪≫ₗ
+  TensorProduct.congr (finsuppLEquivDirectSum R M ι) (finsuppLEquivDirectSum R N κ) ≪≫ₗ
     ((TensorProduct.directSum R (fun _ : ι => M) fun _ : κ => N) ≪≫ₗ
-      (finsuppLequivDirectSum R (M ⊗[R] N) (ι × κ)).symm)
+      (finsuppLEquivDirectSum R (M ⊗[R] N) (ι × κ)).symm)
 #align finsupp_tensor_finsupp finsuppTensorFinsupp
 
 @[simp]
diff --git a/lake-manifest.json b/lake-manifest.json
index 193ebf93e0..98c2d4e79b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "693bed9121b174d067f8a4a8e35df5b602200a37",
+    "rev": "d34a07f2a36e4671efb78f17dd1ab012f111f008",
     "name": "lean3port",
-    "inputRev?": "693bed9121b174d067f8a4a8e35df5b602200a37"}},
+    "inputRev?": "d34a07f2a36e4671efb78f17dd1ab012f111f008"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "e3cd24829ee170492d251da5878e7dc98e52479b",
+    "rev": "7307cd34049d6ba8b5901766daabe441a8fcc08c",
     "name": "mathlib",
-    "inputRev?": "e3cd24829ee170492d251da5878e7dc98e52479b"}},
+    "inputRev?": "7307cd34049d6ba8b5901766daabe441a8fcc08c"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 2c0b9bd5f9..7c92f20c1d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-03-20-08"
+def tag : String := "nightly-2023-03-20-10"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"693bed9121b174d067f8a4a8e35df5b602200a37"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"d34a07f2a36e4671efb78f17dd1ab012f111f008"
 
 @[default_target]
 lean_lib Mathbin where