∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {f : A} {d : ι} (hf : f ∈ 𝒜 d) (x : HomogeneousLocalization.Away 𝒜 f),
  ∃ n a, ∃ (ha : a ∈ 𝒜 (n • d)), HomogeneousLocalization.Away.mk 𝒜 hf n a ha = x