-- Mathlib/Algebra/Colimit/Ring.lean
lemma map_comp (g₁ : (i : ι) → G i →+* G' i) (g₂ : (i : ι) → G' i →+* G'' i)
    (hg₁ : ∀ i j h, (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
    (hg₂ : ∀ i j h, (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)) :
    ((map g₂ hg₂).comp (map g₁ hg₁) :
      DirectLimit G (fun _ _ h ↦ f _ _ h) →+* DirectLimit G'' fun _ _ h ↦ f'' _ _ h) =
    (map (fun i ↦ (g₂ i).comp (g₁ i)) fun i j h ↦ by
      rw [RingHom.comp_assoc, hg₁ i, ← RingHom.comp_assoc, hg₂ i, RingHom.comp_assoc] :
      DirectLimit G (fun _ _ h ↦ f _ _ h) →+* DirectLimit G'' fun _ _ h ↦ f'' _ _ h) :=
  DFunLike.ext _ _ fun x ↦ by
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    refine x.induction_on (by simp) (fun _ ↦ ?_) (by simp+contextual) (by simp+contextual)
    rw [RingHom.comp_apply, quotientMk_of]
    simp_rw [map_apply_of]
    rfl

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
x : FreeCommRing ((i : ι) × G i)
⊢ ∀ (x y : FreeCommRing ((i : ι) × G i)),
    ((map g₂ hg₂).comp (map g₁ hg₁))
          ((Ideal.Quotient.mk
              (Ideal.span
                {a |
                  (∃ i j,
                      ∃ (H : i ≤ j),
                        ∃ x, FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) 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}))
            x) =
        (map (fun i => (g₂ i).comp (g₁ i)) ⋯)
          ((Ideal.Quotient.mk
              (Ideal.span
                {a |
                  (∃ i j,
                      ∃ (H : i ≤ j),
                        ∃ x, FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) 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}))
            x) →
      ((map g₂ hg₂).comp (map g₁ hg₁))
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j,
                        ∃ (H : i ≤ j),
                          ∃ x,
                            FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) 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}))
              y) =
          (map (fun i => (g₂ i).comp (g₁ i)) ⋯)
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j,
                        ∃ (H : i ≤ j),
                          ∃ x,
                            FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) 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}))
              y) →
        ((map g₂ hg₂).comp (map g₁ hg₁))
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j,
                        ∃ (H : i ≤ j),
                          ∃ x,
                            FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) 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}))
              (x * y)) =
          (map (fun i => (g₂ i).comp (g₁ i)) ⋯)
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j,
                        ∃ (H : i ≤ j),
                          ∃ x,
                            FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) 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}))
              (x * y))

Tactic:
simp+contextual

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
x : FreeCommRing ((i : ι) × G i)
⊢ ((map g₂ hg₂).comp (map g₁ hg₁))
      ((Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j,
                  ∃ (H : i ≤ j),
                    ∃ x, FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) 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)) =
    (map (fun i => (g₂ i).comp (g₁ i)) ⋯)
      ((Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j,
                  ∃ (H : i ≤ j),
                    ∃ x, FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) 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))

Tactic:
simp

Result:
no goals