-- Module: Mathlib.Algebra.Colimit.Ring
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
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
suffices :
  LE.le (α := 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})
    (Ideal.comap (F := FreeCommRing ((i : ι) × G i) →+* P)
      ((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⊥)
⊢ ∀ (a : FreeCommRing ((i : ι) × G i)),
    Membership.mem (γ := 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})
        a →
      Eq.{u_3 + 1} (α := P)
        (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
                (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
              (a : FreeCommRing ((i : ι) × G i)) → P)
            a :
          P)
        (0 : P)

Tactic:
suffices Ideal.span _ ≤
          Ideal.comap (FreeCommRing.lift fun x : Σ i : ι, G i ↦ g x.fst x.snd) ⊥ by
        intro x hx
        exact (mem_bot P).1 (this hx)