{P : Sort u} →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {sα : Q(CommSemiring «$α»)} →
        {e : Q(«$α»)} →
          {x : Mathlib.Tactic.Ring.ExSum sα e} →
            {u' : Lean.Level} →
              {α' : Q(Type u')} →
                {sα' : Q(CommSemiring «$α'»)} →
                  {e' : Q(«$α'»)} →
                    {x' : Mathlib.Tactic.Ring.ExSum sα' e'} →
                      u = u' →
                        α = α' →
                          sα = sα' →
                            e = e' →
                              Mathlib.Tactic.Ring.ExBase.sum x ≍ Mathlib.Tactic.Ring.ExBase.sum x' →
                                (u = u' → α = α' → sα = sα' → e = e' → x ≍ x' → P) → P