{u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      (a₁ _a₂ _b₂ : Q(«$α»)) →
        (motive : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) q(«$a₁» + «$_a₂» + «$_b₂») → Sort u_1) →
          (__discr : Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExSum sα) q(«$a₁» + «$_a₂» + «$_b₂»)) →
            ((_c : Q(«$α»)) →
                (vc : Mathlib.Tactic.Ring.ExSum sα _c) →
                  (pc : Q(«$a₁» + «$_a₂» + «$_b₂» = «$_c»)) → motive { expr := _c, val := vc, proof := pc }) →
              motive __discr