{ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddMonoid ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        {motive : DirectSum.GSemiring A → Sort u} →
          (t : DirectSum.GSemiring A) →
            ([toGNonUnitalNonAssocSemiring : DirectSum.GNonUnitalNonAssocSemiring A] →
                [toGOne : GradedMonoid.GOne A] →
                  (one_mul : ∀ (a : GradedMonoid A), 1 * a = a) →
                    (mul_one : ∀ (a : GradedMonoid A), a * 1 = a) →
                      (mul_assoc : ∀ (a b c : GradedMonoid A), a * b * c = a * (b * c)) →
                        (gnpow : (n : ℕ) → {i : ι} → A i → A (n • i)) →
                          (gnpow_zero' : ∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (gnpow 0 a.snd) = 1) →
                            (gnpow_succ' :
                                ∀ (n : ℕ) (a : GradedMonoid A),
                                  GradedMonoid.mk (n.succ • a.fst) (gnpow n.succ a.snd) =
                                    ⟨n • a.fst, gnpow n a.snd⟩ * a) →
                              (natCast : ℕ → A 0) →
                                (natCast_zero : natCast 0 = 0) →
                                  (natCast_succ : ∀ (n : ℕ), natCast (n + 1) = natCast n + GradedMonoid.GOne.one) →
                                    motive
                                      { toGNonUnitalNonAssocSemiring := toGNonUnitalNonAssocSemiring, toGOne := toGOne,
                                        one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc, gnpow := gnpow,
                                        gnpow_zero' := gnpow_zero', gnpow_succ' := gnpow_succ', natCast := natCast,
                                        natCast_zero := natCast_zero, natCast_succ := natCast_succ }) →
              motive t