∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (deg : ι) (num den : ↥(𝒜 deg)) (den_mem : ↑den ∈ x) (deg_1 : ι) (num_1 den_1 : ↥(𝒜 deg_1)) (den_mem_1 : ↑den_1 ∈ x),
  ({ deg := deg, num := num, den := den, den_mem := den_mem } =
      { deg := deg_1, num := num_1, den := den_1, den_mem := den_mem_1 }) =
    (deg = deg_1 ∧ num ≍ num_1 ∧ den ≍ den_1)