output of set_option pp.all true

pp_all.lean

  @finset.sum.{0 ?l_1} nat (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3)
    (@add_comm_group.to_add_comm_monoid.{?l_1} (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) ?m_4)
    (finset.range (@has_add.add.{0} nat nat.has_add k (@has_one.one.{0} nat nat.has_one)))
    (λ (i : nat),
       @has_mul.mul.{?l_1} (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) ?m_5[i]
         (@has_pow.pow.{?l_1 0} (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) nat ?m_6[i]
            (@mv_polynomial.C.{?l_1 0} ?m_2 nat (λ (a b : nat), nat.decidable_eq a b) ?m_7[i] ?m_3
               (@coe.{1 ?l_1+1} nat ?m_2 ?m_8[i] (@nat.Prime.p _inst_1)))
            i)
         (@has_pow.pow.{?l_1 0} (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) nat ?m_9[i]
            (@mv_polynomial.X.{?l_1 0} ?m_2 nat (λ (a b : nat), nat.decidable_eq a b) ?m_10[i] ?m_3 i)
            (@has_pow.pow.{0 0} nat nat nat.has_pow (@nat.Prime.p _inst_1) (@has_sub.sub.{0} nat nat.has_sub k i))))

wants to be equal to

    (@finset.sum.{0 0} nat
       (@mv_polynomial.{0 0} nat rat
          (@comm_ring.to_comm_semiring.{0} rat
             (@nonzero_comm_ring.to_comm_ring.{0} rat
                (@integral_domain.to_nonzero_comm_ring.{0} rat
                   (@field.to_integral_domain.{0} rat
                      (@linear_ordered_field.to_field.{0} rat
                         (@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
                            rat.discrete_linear_ordered_field)))))))
       (@semiring.to_add_comm_monoid.{0}
          (@mv_polynomial.{0 0} nat rat
             (@comm_ring.to_comm_semiring.{0} rat
                (@nonzero_comm_ring.to_comm_ring.{0} rat
                   (@integral_domain.to_nonzero_comm_ring.{0} rat
                      (@field.to_integral_domain.{0} rat
                         (@linear_ordered_field.to_field.{0} rat
                            (@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
                               rat.discrete_linear_ordered_field)))))))
          (@ring.to_semiring.{0}
             (@mv_polynomial.{0 0} nat rat
                (@comm_ring.to_comm_semiring.{0} rat
                   (@nonzero_comm_ring.to_comm_ring.{0} rat
                      (@integral_domain.to_nonzero_comm_ring.{0} rat
                         (@field.to_integral_domain.{0} rat
                            (@linear_ordered_field.to_field.{0} rat
                               (@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
                                  rat.discrete_linear_ordered_field)))))))
             (@mv_polynomial.ring.{0 0} rat nat nat.decidable_eq rat.decidable_eq
                (@nonzero_comm_ring.to_comm_ring.{0} rat
                   (@integral_domain.to_nonzero_comm_ring.{0} rat
                      (@field.to_integral_domain.{0} rat
                         (@linear_ordered_field.to_field.{0} rat
                            (@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
                               rat.discrete_linear_ordered_field))))))))
       (finset.range (@has_add.add.{0} nat nat.has_add k (@has_one.one.{0} nat nat.has_one))) ...