Sort u →
  {ι : Type u_1} →
    {A : Type u_2} →
      {σ : Type u_3} →
        [inst : CommRing A] →
          [inst_1 : SetLike σ A] →
            {𝒜 : ι → σ} →
              {x : Submonoid A} →
                HomogeneousLocalization.NumDenSameDeg 𝒜 x →
                  {ι' : Type u_1} →
                    {A' : Type u_2} →
                      {σ' : Type u_3} →
                        [inst' : CommRing A'] →
                          [inst'_1 : SetLike σ' A'] →
                            {𝒜' : ι' → σ'} → {x' : Submonoid A'} → HomogeneousLocalization.NumDenSameDeg 𝒜' x' → Sort u