{u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        (b b_1 : Q(«$α»)) →
          (motive : Mathlib.Tactic.Ring.Common.Overlap bt sα q(«$b» + «$b_1») → Sort u_1) →
            (__do_lift : Mathlib.Tactic.Ring.Common.Overlap bt sα q(«$b» + «$b_1»)) →
              ((p : Q(Mathlib.Meta.NormNum.IsNat («$b» + «$b_1») 0)) →
                  motive (Mathlib.Tactic.Ring.Common.Overlap.zero p)) →
                ((expr : Q(«$α»)) →
                    (vc : Mathlib.Tactic.Ring.Common.ExProd bt sα expr) →
                      (p : Q(«$b» + «$b_1» = «$expr»)) →
                        motive (Mathlib.Tactic.Ring.Common.Overlap.nonzero { expr := expr, val := vc, proof := p })) →
                  motive __do_lift