{motive_3 :
    {u : Lean.Level} →
      {α : Q(Type u)} → (a : Q(CommSemiring «$α»)) → (e : Q(«$α»)) → Mathlib.Tactic.Ring.ExSum a e → Sort u} →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {a : Q(CommSemiring «$α»)} →
        {e : Q(«$α»)} →
          (t : Mathlib.Tactic.Ring.ExSum a e) →
            t.ctorIdx = 1 →
              ({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) →
                            motive_3 sα q(«$a» + «$b») (Mathlib.Tactic.Ring.ExSum.add a_1 a_2)) →
                motive_3 a e t