{A : Type u_1} →
  [inst : CommRing A] →
    {f g q : PowerSeries A} →
      {r : Polynomial A} →
        {I : Ideal A} →
          {motive : f.IsWeierstrassDivisionAt g q r I → Sort u} →
            (t : f.IsWeierstrassDivisionAt g q r I) →
              ((degree_lt : r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat) →
                  (eq_mul_add : f = g * q + ↑r) → motive ⋯) →
                motive t