{motive_1 :
    {u : Lean.Level} →
      {α : Q(Type u)} → (a : Q(CommSemiring «$α»)) → (e : Q(«$α»)) → Mathlib.Tactic.Ring.ExBase a e → Sort u} →
  {motive_2 :
      {u : Lean.Level} →
        {α : Q(Type u)} → (a : Q(CommSemiring «$α»)) → (e : Q(«$α»)) → Mathlib.Tactic.Ring.ExProd a e → Sort u} →
    {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)} →
            {sα : Q(CommSemiring «$α»)} →
              {e : Q(«$α»)} → (id : ℕ) → motive_1 sα e (Mathlib.Tactic.Ring.ExBase.atom id)) →
        ({u : Lean.Level} →
            {α : Q(Type u)} →
              {sα : Q(CommSemiring «$α»)} →
                {e : Q(«$α»)} →
                  (x : Mathlib.Tactic.Ring.ExSum sα e) →
                    motive_3 sα e x → motive_1 sα e (Mathlib.Tactic.Ring.ExBase.sum x)) →
          ({u : Lean.Level} →
              {α : Q(Type u)} →
                {sα : Q(CommSemiring «$α»)} →
                  {e : Q(«$α»)} →
                    (value : ℚ) →
                      (hyp : Option Lean.Expr) → motive_2 sα e (Mathlib.Tactic.Ring.ExProd.const value hyp)) →
            ({u : Lean.Level} →
                {α : Q(Type u)} →
                  {sα : Q(CommSemiring «$α»)} →
                    {x : Q(«$α»)} →
                      {e : Q(ℕ)} →
                        {b : Q(«$α»)} →
                          (a : Mathlib.Tactic.Ring.ExBase sα x) →
                            (a_1 : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ e) →
                              (a_2 : Mathlib.Tactic.Ring.ExProd sα b) →
                                motive_1 sα x a →
                                  motive_2 Mathlib.Tactic.Ring.sℕ e a_1 →
                                    motive_2 sα b a_2 →
                                      motive_2 sα q(«$x» ^ «$e» * «$b») (Mathlib.Tactic.Ring.ExProd.mul a a_1 a_2)) →
              ({u : Lean.Level} →
                  {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → motive_3 sα q(0) Mathlib.Tactic.Ring.ExSum.zero) →
                ({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_2 sα a a_1 →
                                motive_3 sα b a_2 →
                                  motive_3 sα q(«$a» + «$b») (Mathlib.Tactic.Ring.ExSum.add a_1 a_2)) →
                  {u : Lean.Level} →
                    {α : Q(Type u)} →
                      {a : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → (t : Mathlib.Tactic.Ring.ExProd a e) → motive_2 a e t