{P : Sort u} →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {sα : Q(CommSemiring «$α»)} →
        {a b : Q(«$α»)} →
          {a_1 : Mathlib.Tactic.Ring.ExProd sα a} →
            {a_2 : Mathlib.Tactic.Ring.ExSum sα b} →
              {u' : Lean.Level} →
                {α' : Q(Type u')} →
                  {sα' : Q(CommSemiring «$α'»)} →
                    {a' b' : Q(«$α'»)} →
                      {a'_1 : Mathlib.Tactic.Ring.ExProd sα' a'} →
                        {a'_2 : Mathlib.Tactic.Ring.ExSum sα' b'} →
                          u = u' →
                            α = α' →
                              sα = sα' →
                                q(«$a» + «$b») = q(«$a'» + «$b'») →
                                  Mathlib.Tactic.Ring.ExSum.add a_1 a_2 ≍ Mathlib.Tactic.Ring.ExSum.add a'_1 a'_2 →
                                    (u = u' → α = α' → sα = sα' → a = a' → b = b' → a_1 ≍ a'_1 → a_2 ≍ a'_2 → P) → P