{ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddCommMonoid ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        (mul : {i j : ι} → A i → A j → A (i + j)) →
          (∀ {i j : ι} (a : A i), mul a 0 = 0) →
            (∀ {i j : ι} (b : A j), mul 0 b = 0) →
              (∀ {i j : ι} (a : A i) (b c : A j), mul a (b + c) = mul a b + mul a c) →
                (∀ {i j : ι} (a b : A i) (c : A j), mul (a + b) c = mul a c + mul b c) →
                  (one : A 0) →
                    (∀ (a : GradedMonoid A), 1 * a = a) →
                      (∀ (a : GradedMonoid A), a * 1 = a) →
                        (∀ (a b c : GradedMonoid A), a * b * c = a * (b * c)) →
                          (gnpow : (n : ℕ) → {i : ι} → A i → A (n • i)) →
                            autoParam (∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (gnpow 0 a.snd) = 1)
                                GradedMonoid.GMonoid.gnpow_zero'._autoParam →
                              autoParam
                                  (∀ (n : ℕ) (a : GradedMonoid A),
                                    GradedMonoid.mk (n.succ • a.fst) (gnpow n.succ a.snd) =
                                      ⟨n • a.fst, gnpow n a.snd⟩ * a)
                                  GradedMonoid.GMonoid.gnpow_succ'._autoParam →
                                (natCast : ℕ → A 0) →
                                  natCast 0 = 0 →
                                    (∀ (n : ℕ), natCast (n + 1) = natCast n + one) →
                                      (∀ (a b : GradedMonoid A), a * b = b * a) → DirectSum.GCommSemiring A