-- 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:
case intro
ι : 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✝ : (i : ι) × G i
⊢ (of G'' (fun x x_1 h => ⇑(f'' x x_1 h)) x✝.fst) ((g₂ x✝.fst) ((g₁ x✝.fst) x✝.snd)) =
    (of G'' (fun x x_1 h => ⇑(f'' x x_1 h)) x✝.fst) (((g₂ x✝.fst).comp (g₁ x✝.fst)) x✝.snd)

Tactic:
rfl

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
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ 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)
i j : ι
h : i ≤ j
⊢ ((fun i => (g₂ i).comp (g₁ i)) j).comp (f i j h) = (f'' i j h).comp ((fun i => (g₂ i).comp (g₁ i)) i)

Tactic:
rw [RingHom.comp_assoc, hg₁ i, ← RingHom.comp_assoc, hg₂ i, RingHom.comp_assoc]

Result:
no goals