is_scalar_tower term involved in a typeclass search: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Tracing.20time.20of.20type.20class.20inference/near/240020943

term.txt

@is_scalar_tower 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
  (@smul_with_zero.to_has_scalar 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
     (@mul_zero_class.to_has_zero 𝕜
        (@mul_zero_one_class.to_mul_zero_class 𝕜
           (@monoid_with_zero.to_mul_zero_one_class 𝕜
              (@semiring.to_monoid_with_zero 𝕜
                 (@comm_semiring.to_semiring 𝕜
                    (@comm_ring.to_comm_semiring 𝕜
                       (@semi_normed_comm_ring.to_comm_ring 𝕜
                          (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                             (@normed_field.to_normed_comm_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))))
     (@add_zero_class.to_has_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
        (@add_monoid.to_add_zero_class C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@add_comm_monoid.to_add_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@semiring.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@comm_semiring.to_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@comm_ring.to_comm_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                       (@smooth_map_comm_ring 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                          (@normed_ring.to_normed_group 𝕜
                             (@normed_comm_ring.to_normed_ring 𝕜
                                (@normed_field.to_normed_comm_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                          (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                          H
                          _inst_4
                          I
                          𝕜
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_group.to_pseudo_metric_space 𝕜
                                   (@normed_group.to_semi_normed_group 𝕜
                                      (@normed_ring.to_normed_group 𝕜
                                         (@normed_comm_ring.to_normed_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                          𝓘(𝕜, 𝕜)
                          M
                          _inst_5
                          _inst_6
                          𝕜
                          (@semi_normed_comm_ring.to_comm_ring 𝕜
                             (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                (@normed_field.to_normed_comm_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                   (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                      (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                          (@charted_space_self 𝕜
                             (@uniform_space.to_topological_space 𝕜
                                (@metric_space.to_uniform_space' 𝕜
                                   (@semi_normed_group.to_pseudo_metric_space 𝕜
                                      (@normed_group.to_semi_normed_group 𝕜
                                         (@normed_ring.to_normed_group 𝕜
                                            (@normed_comm_ring.to_normed_ring 𝕜
                                               (@normed_field.to_normed_comm_ring 𝕜
                                                  (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                          _)))))))
     (@mul_action_with_zero.to_smul_with_zero 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
        (@semiring.to_monoid_with_zero 𝕜
           (@comm_semiring.to_semiring 𝕜
              (@comm_ring.to_comm_semiring 𝕜
                 (@semi_normed_comm_ring.to_comm_ring 𝕜
                    (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                       (@normed_field.to_normed_comm_ring 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
        (@add_zero_class.to_has_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@add_monoid.to_add_zero_class C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@add_comm_monoid.to_add_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@semiring.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@comm_semiring.to_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                       (@comm_ring.to_comm_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                          (@smooth_map_comm_ring 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                             (@normed_ring.to_normed_group 𝕜
                                (@normed_comm_ring.to_normed_ring 𝕜
                                   (@normed_field.to_normed_comm_ring 𝕜
                                      (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                             (@normed_field.to_normed_space 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                             H
                             _inst_4
                             I
                             𝕜
                             (@uniform_space.to_topological_space 𝕜
                                (@metric_space.to_uniform_space' 𝕜
                                   (@semi_normed_group.to_pseudo_metric_space 𝕜
                                      (@normed_group.to_semi_normed_group 𝕜
                                         (@normed_ring.to_normed_group 𝕜
                                            (@normed_comm_ring.to_normed_ring 𝕜
                                               (@normed_field.to_normed_comm_ring 𝕜
                                                  (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                             𝓘(𝕜, 𝕜)
                             M
                             _inst_5
                             _inst_6
                             𝕜
                             (@semi_normed_comm_ring.to_comm_ring 𝕜
                                (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                   (@normed_field.to_normed_comm_ring 𝕜
                                      (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                             (@uniform_space.to_topological_space 𝕜
                                (@metric_space.to_uniform_space' 𝕜
                                   (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                      (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                         (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                             (@charted_space_self 𝕜
                                (@uniform_space.to_topological_space 𝕜
                                   (@metric_space.to_uniform_space' 𝕜
                                      (@semi_normed_group.to_pseudo_metric_space 𝕜
                                         (@normed_group.to_semi_normed_group 𝕜
                                            (@normed_ring.to_normed_group 𝕜
                                               (@normed_comm_ring.to_normed_ring 𝕜
                                                  (@normed_field.to_normed_comm_ring 𝕜
                                                     (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                             _)))))))
        (@module.to_mul_action_with_zero 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@comm_semiring.to_semiring 𝕜
              (@comm_ring.to_comm_semiring 𝕜
                 (@semi_normed_comm_ring.to_comm_ring 𝕜
                    (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                       (@normed_field.to_normed_comm_ring 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
           (@semiring.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@comm_semiring.to_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@comm_ring.to_comm_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@smooth_map_comm_ring 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                       (@normed_ring.to_normed_group 𝕜
                          (@normed_comm_ring.to_normed_ring 𝕜
                             (@normed_field.to_normed_comm_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                       (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                       H
                       _inst_4
                       I
                       𝕜
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_group.to_pseudo_metric_space 𝕜
                                (@normed_group.to_semi_normed_group 𝕜
                                   (@normed_ring.to_normed_group 𝕜
                                      (@normed_comm_ring.to_normed_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                       𝓘(𝕜, 𝕜)
                       M
                       _inst_5
                       _inst_6
                       𝕜
                       (@semi_normed_comm_ring.to_comm_ring 𝕜
                          (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                             (@normed_field.to_normed_comm_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                   (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                       (@charted_space_self 𝕜
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_group.to_pseudo_metric_space 𝕜
                                   (@normed_group.to_semi_normed_group 𝕜
                                      (@normed_ring.to_normed_group 𝕜
                                         (@normed_comm_ring.to_normed_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                       _))))
           (@algebra.to_module 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@comm_ring.to_comm_semiring 𝕜
                 (@semi_normed_comm_ring.to_comm_ring 𝕜
                    (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                       (@normed_field.to_normed_comm_ring 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))
              (@comm_semiring.to_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@comm_ring.to_comm_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@smooth_map_comm_ring 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                       (@normed_ring.to_normed_group 𝕜
                          (@normed_comm_ring.to_normed_ring 𝕜
                             (@normed_field.to_normed_comm_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                       (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                       H
                       _inst_4
                       I
                       𝕜
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_group.to_pseudo_metric_space 𝕜
                                (@normed_group.to_semi_normed_group 𝕜
                                   (@normed_ring.to_normed_group 𝕜
                                      (@normed_comm_ring.to_normed_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                       𝓘(𝕜, 𝕜)
                       M
                       _inst_5
                       _inst_6
                       𝕜
                       (@semi_normed_comm_ring.to_comm_ring 𝕜
                          (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                             (@normed_field.to_normed_comm_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                   (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                       (@charted_space_self 𝕜
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_group.to_pseudo_metric_space 𝕜
                                   (@normed_group.to_semi_normed_group 𝕜
                                      (@normed_ring.to_normed_group 𝕜
                                         (@normed_comm_ring.to_normed_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                       _)))
              (@times_cont_mdiff_map.algebra 𝕜 _inst_1 E _inst_2 _inst_3 H _inst_4 I M _inst_5 _inst_6 𝕜
                 (@normed_comm_ring.to_normed_ring 𝕜
                    (@normed_field.to_normed_comm_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))
                 (@normed_algebra.id 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                 _)))))
  (@smul_with_zero.to_has_scalar C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
     (@mul_zero_class.to_has_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
        (@mul_zero_one_class.to_mul_zero_class C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@monoid_with_zero.to_mul_zero_one_class C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@semiring.to_monoid_with_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@comm_semiring.to_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@comm_ring.to_comm_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                       (@smooth_map_comm_ring 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                          (@normed_ring.to_normed_group 𝕜
                             (@normed_comm_ring.to_normed_ring 𝕜
                                (@normed_field.to_normed_comm_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                          (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                          H
                          _inst_4
                          I
                          𝕜
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_group.to_pseudo_metric_space 𝕜
                                   (@normed_group.to_semi_normed_group 𝕜
                                      (@normed_ring.to_normed_group 𝕜
                                         (@normed_comm_ring.to_normed_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                          𝓘(𝕜, 𝕜)
                          M
                          _inst_5
                          _inst_6
                          𝕜
                          (@semi_normed_comm_ring.to_comm_ring 𝕜
                             (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                (@normed_field.to_normed_comm_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                   (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                      (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                          (@charted_space_self 𝕜
                             (@uniform_space.to_topological_space 𝕜
                                (@metric_space.to_uniform_space' 𝕜
                                   (@semi_normed_group.to_pseudo_metric_space 𝕜
                                      (@normed_group.to_semi_normed_group 𝕜
                                         (@normed_ring.to_normed_group 𝕜
                                            (@normed_comm_ring.to_normed_ring 𝕜
                                               (@normed_field.to_normed_comm_ring 𝕜
                                                  (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                          _)))))))
     (@add_zero_class.to_has_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
        (@add_monoid.to_add_zero_class C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@add_comm_monoid.to_add_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@add_cancel_comm_monoid.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@add_comm_group.to_cancel_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@smooth_map_add_comm_group 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                       (@normed_ring.to_normed_group 𝕜
                          (@normed_comm_ring.to_normed_ring 𝕜
                             (@normed_field.to_normed_comm_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                       (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                       H
                       _inst_4
                       I
                       𝕜
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_group.to_pseudo_metric_space 𝕜
                                (@normed_group.to_semi_normed_group 𝕜
                                   (@normed_ring.to_normed_group 𝕜
                                      (@normed_comm_ring.to_normed_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                       𝓘(𝕜, 𝕜)
                       M
                       _inst_5
                       _inst_6
                       𝕜
                       (@lie_ring.to_add_comm_group 𝕜
                          (@lie_ring.of_associative_ring 𝕜
                             (@normed_ring.to_ring 𝕜
                                (@normed_comm_ring.to_normed_ring 𝕜
                                   (@normed_field.to_normed_comm_ring 𝕜
                                      (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                   (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                       (@charted_space_self 𝕜
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_group.to_pseudo_metric_space 𝕜
                                   (@normed_group.to_semi_normed_group 𝕜
                                      (@normed_ring.to_normed_group 𝕜
                                         (@normed_comm_ring.to_normed_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                       _))))))
     (@mul_action_with_zero.to_smul_with_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
        C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
        (@semiring.to_monoid_with_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@comm_semiring.to_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@comm_ring.to_comm_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@smooth_map_comm_ring 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                    (@normed_ring.to_normed_group 𝕜
                       (@normed_comm_ring.to_normed_ring 𝕜
                          (@normed_field.to_normed_comm_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                    (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                    H
                    _inst_4
                    I
                    𝕜
                    (@uniform_space.to_topological_space 𝕜
                       (@metric_space.to_uniform_space' 𝕜
                          (@semi_normed_group.to_pseudo_metric_space 𝕜
                             (@normed_group.to_semi_normed_group 𝕜
                                (@normed_ring.to_normed_group 𝕜
                                   (@normed_comm_ring.to_normed_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                    𝓘(𝕜, 𝕜)
                    M
                    _inst_5
                    _inst_6
                    𝕜
                    (@semi_normed_comm_ring.to_comm_ring 𝕜
                       (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                          (@normed_field.to_normed_comm_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                    (@uniform_space.to_topological_space 𝕜
                       (@metric_space.to_uniform_space' 𝕜
                          (@semi_normed_ring.to_pseudo_metric_space 𝕜
                             (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                   (@normed_field.to_normed_comm_ring 𝕜
                                      (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                    (@charted_space_self 𝕜
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_group.to_pseudo_metric_space 𝕜
                                (@normed_group.to_semi_normed_group 𝕜
                                   (@normed_ring.to_normed_group 𝕜
                                      (@normed_comm_ring.to_normed_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                    _))))
        (@add_zero_class.to_has_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@add_monoid.to_add_zero_class C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@add_comm_monoid.to_add_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@add_cancel_comm_monoid.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@add_comm_group.to_cancel_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                       (@smooth_map_add_comm_group 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                          (@normed_ring.to_normed_group 𝕜
                             (@normed_comm_ring.to_normed_ring 𝕜
                                (@normed_field.to_normed_comm_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                          (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                          H
                          _inst_4
                          I
                          𝕜
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_group.to_pseudo_metric_space 𝕜
                                   (@normed_group.to_semi_normed_group 𝕜
                                      (@normed_ring.to_normed_group 𝕜
                                         (@normed_comm_ring.to_normed_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                          𝓘(𝕜, 𝕜)
                          M
                          _inst_5
                          _inst_6
                          𝕜
                          (@lie_ring.to_add_comm_group 𝕜
                             (@lie_ring.of_associative_ring 𝕜
                                (@normed_ring.to_ring 𝕜
                                   (@normed_comm_ring.to_normed_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                   (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                      (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                          (@charted_space_self 𝕜
                             (@uniform_space.to_topological_space 𝕜
                                (@metric_space.to_uniform_space' 𝕜
                                   (@semi_normed_group.to_pseudo_metric_space 𝕜
                                      (@normed_group.to_semi_normed_group 𝕜
                                         (@normed_ring.to_normed_group 𝕜
                                            (@normed_comm_ring.to_normed_ring 𝕜
                                               (@normed_field.to_normed_comm_ring 𝕜
                                                  (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                          _))))))
        (@module.to_mul_action_with_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@comm_semiring.to_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@comm_ring.to_comm_semiring C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@smooth_map_comm_ring 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                    (@normed_ring.to_normed_group 𝕜
                       (@normed_comm_ring.to_normed_ring 𝕜
                          (@normed_field.to_normed_comm_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                    (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                    H
                    _inst_4
                    I
                    𝕜
                    (@uniform_space.to_topological_space 𝕜
                       (@metric_space.to_uniform_space' 𝕜
                          (@semi_normed_group.to_pseudo_metric_space 𝕜
                             (@normed_group.to_semi_normed_group 𝕜
                                (@normed_ring.to_normed_group 𝕜
                                   (@normed_comm_ring.to_normed_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                    𝓘(𝕜, 𝕜)
                    M
                    _inst_5
                    _inst_6
                    𝕜
                    (@semi_normed_comm_ring.to_comm_ring 𝕜
                       (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                          (@normed_field.to_normed_comm_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                    (@uniform_space.to_topological_space 𝕜
                       (@metric_space.to_uniform_space' 𝕜
                          (@semi_normed_ring.to_pseudo_metric_space 𝕜
                             (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                   (@normed_field.to_normed_comm_ring 𝕜
                                      (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                    (@charted_space_self 𝕜
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_group.to_pseudo_metric_space 𝕜
                                (@normed_group.to_semi_normed_group 𝕜
                                   (@normed_ring.to_normed_group 𝕜
                                      (@normed_comm_ring.to_normed_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                    _)))
           (@add_cancel_comm_monoid.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@add_comm_group.to_cancel_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@smooth_map_add_comm_group 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                    (@normed_ring.to_normed_group 𝕜
                       (@normed_comm_ring.to_normed_ring 𝕜
                          (@normed_field.to_normed_comm_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                    (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                    H
                    _inst_4
                    I
                    𝕜
                    (@uniform_space.to_topological_space 𝕜
                       (@metric_space.to_uniform_space' 𝕜
                          (@semi_normed_group.to_pseudo_metric_space 𝕜
                             (@normed_group.to_semi_normed_group 𝕜
                                (@normed_ring.to_normed_group 𝕜
                                   (@normed_comm_ring.to_normed_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                    𝓘(𝕜, 𝕜)
                    M
                    _inst_5
                    _inst_6
                    𝕜
                    (@lie_ring.to_add_comm_group 𝕜
                       (@lie_ring.of_associative_ring 𝕜
                          (@normed_ring.to_ring 𝕜
                             (@normed_comm_ring.to_normed_ring 𝕜
                                (@normed_field.to_normed_comm_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
                    (@uniform_space.to_topological_space 𝕜
                       (@metric_space.to_uniform_space' 𝕜
                          (@semi_normed_ring.to_pseudo_metric_space 𝕜
                             (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                   (@normed_field.to_normed_comm_ring 𝕜
                                      (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                    (@charted_space_self 𝕜
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_group.to_pseudo_metric_space 𝕜
                                (@normed_group.to_semi_normed_group 𝕜
                                   (@normed_ring.to_normed_group 𝕜
                                      (@normed_comm_ring.to_normed_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                    _)))
           (@smooth_map_module' 𝕜 _inst_1 E _inst_2 _inst_3 H _inst_4 I M _inst_5 _inst_6 𝕜
              (@normed_ring.to_normed_group 𝕜
                 (@normed_comm_ring.to_normed_ring 𝕜
                    (@normed_field.to_normed_comm_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
              (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
  (@smul_with_zero.to_has_scalar 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
     (@mul_zero_class.to_has_zero 𝕜
        (@mul_zero_one_class.to_mul_zero_class 𝕜
           (@monoid_with_zero.to_mul_zero_one_class 𝕜
              (@semiring.to_monoid_with_zero 𝕜
                 (@comm_semiring.to_semiring 𝕜
                    (@comm_ring.to_comm_semiring 𝕜
                       (@semi_normed_comm_ring.to_comm_ring 𝕜
                          (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                             (@normed_field.to_normed_comm_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))))
     (@add_zero_class.to_has_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
        (@add_monoid.to_add_zero_class C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@add_comm_monoid.to_add_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@add_cancel_comm_monoid.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@add_comm_group.to_cancel_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@smooth_map_add_comm_group 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                       (@normed_ring.to_normed_group 𝕜
                          (@normed_comm_ring.to_normed_ring 𝕜
                             (@normed_field.to_normed_comm_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                       (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                       H
                       _inst_4
                       I
                       𝕜
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_group.to_pseudo_metric_space 𝕜
                                (@normed_group.to_semi_normed_group 𝕜
                                   (@normed_ring.to_normed_group 𝕜
                                      (@normed_comm_ring.to_normed_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                       𝓘(𝕜, 𝕜)
                       M
                       _inst_5
                       _inst_6
                       𝕜
                       (@lie_ring.to_add_comm_group 𝕜
                          (@lie_ring.of_associative_ring 𝕜
                             (@normed_ring.to_ring 𝕜
                                (@normed_comm_ring.to_normed_ring 𝕜
                                   (@normed_field.to_normed_comm_ring 𝕜
                                      (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                   (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                       (@charted_space_self 𝕜
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_group.to_pseudo_metric_space 𝕜
                                   (@normed_group.to_semi_normed_group 𝕜
                                      (@normed_ring.to_normed_group 𝕜
                                         (@normed_comm_ring.to_normed_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                       _))))))
     (@mul_action_with_zero.to_smul_with_zero 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
        (@semiring.to_monoid_with_zero 𝕜
           (@comm_semiring.to_semiring 𝕜
              (@comm_ring.to_comm_semiring 𝕜
                 (@semi_normed_comm_ring.to_comm_ring 𝕜
                    (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                       (@normed_field.to_normed_comm_ring 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
        (@add_zero_class.to_has_zero C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@add_monoid.to_add_zero_class C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@add_comm_monoid.to_add_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@add_cancel_comm_monoid.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                    (@add_comm_group.to_cancel_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                       (@smooth_map_add_comm_group 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                          (@normed_ring.to_normed_group 𝕜
                             (@normed_comm_ring.to_normed_ring 𝕜
                                (@normed_field.to_normed_comm_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                          (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                          H
                          _inst_4
                          I
                          𝕜
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_group.to_pseudo_metric_space 𝕜
                                   (@normed_group.to_semi_normed_group 𝕜
                                      (@normed_ring.to_normed_group 𝕜
                                         (@normed_comm_ring.to_normed_ring 𝕜
                                            (@normed_field.to_normed_comm_ring 𝕜
                                               (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                          𝓘(𝕜, 𝕜)
                          M
                          _inst_5
                          _inst_6
                          𝕜
                          (@lie_ring.to_add_comm_group 𝕜
                             (@lie_ring.of_associative_ring 𝕜
                                (@normed_ring.to_ring 𝕜
                                   (@normed_comm_ring.to_normed_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
                          (@uniform_space.to_topological_space 𝕜
                             (@metric_space.to_uniform_space' 𝕜
                                (@semi_normed_ring.to_pseudo_metric_space 𝕜
                                   (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                      (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                          (@charted_space_self 𝕜
                             (@uniform_space.to_topological_space 𝕜
                                (@metric_space.to_uniform_space' 𝕜
                                   (@semi_normed_group.to_pseudo_metric_space 𝕜
                                      (@normed_group.to_semi_normed_group 𝕜
                                         (@normed_ring.to_normed_group 𝕜
                                            (@normed_comm_ring.to_normed_ring 𝕜
                                               (@normed_field.to_normed_comm_ring 𝕜
                                                  (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                          _))))))
        (@module.to_mul_action_with_zero 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
           (@comm_semiring.to_semiring 𝕜
              (@comm_ring.to_comm_semiring 𝕜
                 (@semi_normed_comm_ring.to_comm_ring 𝕜
                    (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                       (@normed_field.to_normed_comm_ring 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
           (@add_cancel_comm_monoid.to_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
              (@add_comm_group.to_cancel_add_comm_monoid C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
                 (@smooth_map_add_comm_group 𝕜 _inst_1 E _inst_2 _inst_3 𝕜
                    (@normed_ring.to_normed_group 𝕜
                       (@normed_comm_ring.to_normed_ring 𝕜
                          (@normed_field.to_normed_comm_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
                    (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))
                    H
                    _inst_4
                    I
                    𝕜
                    (@uniform_space.to_topological_space 𝕜
                       (@metric_space.to_uniform_space' 𝕜
                          (@semi_normed_group.to_pseudo_metric_space 𝕜
                             (@normed_group.to_semi_normed_group 𝕜
                                (@normed_ring.to_normed_group 𝕜
                                   (@normed_comm_ring.to_normed_ring 𝕜
                                      (@normed_field.to_normed_comm_ring 𝕜
                                         (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))))
                    𝓘(𝕜, 𝕜)
                    M
                    _inst_5
                    _inst_6
                    𝕜
                    (@lie_ring.to_add_comm_group 𝕜
                       (@lie_ring.of_associative_ring 𝕜
                          (@normed_ring.to_ring 𝕜
                             (@normed_comm_ring.to_normed_ring 𝕜
                                (@normed_field.to_normed_comm_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))
                    (@uniform_space.to_topological_space 𝕜
                       (@metric_space.to_uniform_space' 𝕜
                          (@semi_normed_ring.to_pseudo_metric_space 𝕜
                             (@semi_normed_comm_ring.to_semi_normed_ring 𝕜
                                (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
                                   (@normed_field.to_normed_comm_ring 𝕜
                                      (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))
                    (@charted_space_self 𝕜
                       (@uniform_space.to_topological_space 𝕜
                          (@metric_space.to_uniform_space' 𝕜
                             (@semi_normed_group.to_pseudo_metric_space 𝕜
                                (@normed_group.to_semi_normed_group 𝕜
                                   (@normed_ring.to_normed_group 𝕜
                                      (@normed_comm_ring.to_normed_ring 𝕜
                                         (@normed_field.to_normed_comm_ring 𝕜
                                            (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1)))))))))
                    _)))
           (@smooth_map_module 𝕜 _inst_1 E _inst_2 _inst_3 H _inst_4 I M _inst_5 _inst_6 𝕜
              (@normed_ring.to_normed_group 𝕜
                 (@normed_comm_ring.to_normed_ring 𝕜
                    (@normed_field.to_normed_comm_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))
              (@normed_field.to_normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_1))))))