∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : (i : ι) → CommRing (G i)]
  (f : (i j : ι) → i ≤ j → G i → G j) (i : ι),
  (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (FreeCommRing.of ⟨i, 1⟩) =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      1