{u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {motive_1 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e → Sort u} →
          {motive_2 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExProd BaseType sα e → Sort u} →
            {motive_3 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExSum BaseType sα e → Sort u} →
              {e : Q(«$α»)} →
                (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e) →
                  ({e : Q(«$α»)} → (id : ℕ) → motive_1 e (Mathlib.Tactic.Ring.Common.ExBase.atom id)) →
                    ({e : Q(«$α»)} →
                        (x : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e) →
                          motive_3 e x → motive_1 e (Mathlib.Tactic.Ring.Common.ExBase.sum x)) →
                      ({e : Q(«$α»)} →
                          (value : BaseType e) → motive_2 e (Mathlib.Tactic.Ring.Common.ExProd.const value)) →
                        ({x : Q(«$α»)} →
                            {e : Q(ℕ)} →
                              {b : Q(«$α»)} →
                                (a : Mathlib.Tactic.Ring.Common.ExBase BaseType sα x) →
                                  (a_1 : Mathlib.Tactic.Ring.Common.ExProdNat e) →
                                    (a_2 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα b) →
                                      motive_1 x a →
                                        motive_2 b a_2 →
                                          motive_2 q(«$x» ^ «$e» * «$b»)
                                            (Mathlib.Tactic.Ring.Common.ExProd.mul a a_1 a_2)) →
                          motive_3 q(0) Mathlib.Tactic.Ring.Common.ExSum.zero →
                            ({a b : Q(«$α»)} →
                                (a_1 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα a) →
                                  (a_2 : Mathlib.Tactic.Ring.Common.ExSum BaseType sα b) →
                                    motive_2 a a_1 →
                                      motive_3 b a_2 →
                                        motive_3 q(«$a» + «$b») (Mathlib.Tactic.Ring.Common.ExSum.add a_1 a_2)) →
                              motive_1 e t