-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
⊢ ∃ (i : ι) (x : G i),
    Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
      ((Ideal.Quotient.mk
              (Ideal.span
                {a : FreeCommRing ((i : ι) × G i) |
                  (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                        a) ∨
                    (∃ (i : ι),
                        HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                            (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                          a) ∨
                      (∃ (i : ι) (x : G i) (y : G i),
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                              (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                                FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                            a) ∨
                        ∃ (i : ι) (x : G i) (y : G i),
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                                FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                            a}) :
            (a : FreeCommRing ((i : ι) × G i)) →
              FreeCommRing ((i : ι) × G i) ⧸
                Ideal.span
                  {a : FreeCommRing ((i : ι) × G i) |
                    (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                        FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                      (∃ (i : ι), FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                        (∃ (i : ι) (x : G i) (y : G i),
                            FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                          ∃ (i : ι) (x : G i) (y : G i),
                            FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})
          z :
        HasQuotient.Quotient (FreeCommRing ((i : ι) × G i)) (B := Ideal (FreeCommRing ((i : ι) × G i)))
          (Ideal.span
            {a : FreeCommRing ((i : ι) × G i) |
              (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                  FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                    a) ∨
                (∃ (i : ι),
                    HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                        (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                      a) ∨
                  (∃ (i : ι) (x : G i) (y : G i),
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                          (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                        a) ∨
                    ∃ (i : ι) (x : G i) (y : G i),
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                        a}))
have refine_1 : ∀ (x y : FreeCommRing ((i : ι) × G i)),
  (∃ (i : ι) (x_1 : G i),
      Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) x_1 : DirectLimit G f)
        ((Ideal.Quotient.mk
                (Ideal.span
                  {a : FreeCommRing ((i : ι) × G i) |
                    (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                        FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                          a) ∨
                      (∃ (i : ι),
                          HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                              (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                            a) ∨
                        (∃ (i : ι) (x : G i) (y : G i),
                            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                                (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                                  FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                              a) ∨
                          ∃ (i : ι) (x : G i) (y : G i),
                            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                                FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                                  FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                              a}) :
              (a : FreeCommRing ((i : ι) × G i)) →
                FreeCommRing ((i : ι) × G i) ⧸
                  Ideal.span
                    {a : FreeCommRing ((i : ι) × G i) |
                      (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                          FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                        (∃ (i : ι), FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                          (∃ (i : ι) (x : G i) (y : G i),
                              FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                            ∃ (i : ι) (x : G i) (y : G i),
                              FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})
            x :
          HasQuotient.Quotient (FreeCommRing ((i : ι) × G i)) (B := Ideal (FreeCommRing ((i : ι) × G i)))
            (Ideal.span
              {a : FreeCommRing ((i : ι) × G i) |
                (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                    FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                        FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                      a) ∨
                  (∃ (i : ι),
                      HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                          (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                        a) ∨
                    (∃ (i : ι) (x : G i) (y : G i),
                        FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                            (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                          a) ∨
                      ∃ (i : ι) (x : G i) (y : G i),
                        FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                          a}))) →
    (∃ (i : ι) (x : G i),
        Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
          ((Ideal.Quotient.mk
                  (Ideal.span
                    {a : FreeCommRing ((i : ι) × G i) |
                      (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                            a) ∨
                        (∃ (i : ι),
                            HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                                (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                              a) ∨
                          (∃ (i : ι) (x : G i) (y : G i),
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                                  (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                                    FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                                a) ∨
                            ∃ (i : ι) (x : G i) (y : G i),
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                                  FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                                    FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                                a}) :
                (a : FreeCommRing ((i : ι) × G i)) →
                  FreeCommRing ((i : ι) × G i) ⧸
                    Ideal.span
                      {a : FreeCommRing ((i : ι) × G i) |
                        (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                            FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                          (∃ (i : ι), FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                            (∃ (i : ι) (x : G i) (y : G i),
                                FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                              ∃ (i : ι) (x : G i) (y : G i),
                                FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})
              y :
            HasQuotient.Quotient (FreeCommRing ((i : ι) × G i)) (B := Ideal (FreeCommRing ((i : ι) × G i)))
              (Ideal.span
                {a : FreeCommRing ((i : ι) × G i) |
                  (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                        a) ∨
                    (∃ (i : ι),
                        HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                            (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                          a) ∨
                      (∃ (i : ι) (x : G i) (y : G i),
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                              (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                                FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                            a) ∨
                        ∃ (i : ι) (x : G i) (y : G i),
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                                FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                            a}))) →
      ∃ (i : ι) (x_1 : G i),
        Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) x_1 : DirectLimit G f)
          ((Ideal.Quotient.mk
                  (Ideal.span
                    {a : FreeCommRing ((i : ι) × G i) |
                      (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                            a) ∨
                        (∃ (i : ι),
                            HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                                (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                              a) ∨
                          (∃ (i : ι) (x : G i) (y : G i),
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                                  (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                                    FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                                a) ∨
                            ∃ (i : ι) (x : G i) (y : G i),
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                                  FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                                    FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                                a}) :
                (a : FreeCommRing ((i : ι) × G i)) →
                  FreeCommRing ((i : ι) × G i) ⧸
                    Ideal.span
                      {a : FreeCommRing ((i : ι) × G i) |
                        (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                            FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                          (∃ (i : ι), FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                            (∃ (i : ι) (x : G i) (y : G i),
                                FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                              ∃ (i : ι) (x : G i) (y : G i),
                                FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})
              (x + y) :
            HasQuotient.Quotient (FreeCommRing ((i : ι) × G i)) (B := Ideal (FreeCommRing ((i : ι) × G i)))
              (Ideal.span
                {a : FreeCommRing ((i : ι) × G i) |
                  (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                        a) ∨
                    (∃ (i : ι),
                        HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                            (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                          a) ∨
                      (∃ (i : ι) (x : G i) (y : G i),
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                              (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                                FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                            a) ∨
                        ∃ (i : ι) (x : G i) (y : G i),
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                                FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                            a}))
Tactic: refine z.induction_on ⟨Classical.arbitrary ι, -1, by simp; rfl⟩ (fun ⟨i, x⟩ ↦ ⟨i, x, rfl⟩) ?_ ?_