-- Mathlib/Algebra/Colimit/Module.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 f →+ DirectLimit G'' f'') =
    (map (fun i ↦ (g₂ i).comp (g₁ i)) fun i j h ↦ by
      rw [AddMonoidHom.comp_assoc, hg₁ i, ← AddMonoidHom.comp_assoc, hg₂ i,
        AddMonoidHom.comp_assoc] :
      DirectLimit G f →+ DirectLimit G'' f'') :=
  DFunLike.ext _ _ <| by
    rintro ⟨x⟩; refine x.induction_on (by simp) (fun _ _ ↦ ?_) (by simp +contextual)
    show map g₂ hg₂ (map g₁ hg₁ <| of _ _ _ _) = map _ _ (of _ _ _ _)
    simp_rw [map_apply_of]; rfl

Proof state:
ι : Type u_2
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (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 : DirectLimit G f), ((map g₂ hg₂).comp (map g₁ hg₁)) x = (map (fun i => (g₂ i).comp (g₁ i)) ⋯) x

Tactic:
rintro ⟨x⟩

Result:
case mk
ι : Type u_2
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (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✝ : DirectLimit G f
x : DirectSum ι G
⊢ ((map g₂ hg₂).comp (map g₁ hg₁))
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) =
    (map (fun i => (g₂ i).comp (g₁ i)) ⋯)
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x)

Proof state:
case mk
ι : Type u_2
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (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✝² : DirectLimit G f
x : DirectSum ι G
x✝¹ : ι
x✝ : G x✝¹
⊢ (of G'' f'' x✝¹) ((g₂ x✝¹) ((g₁ x✝¹) x✝)) = (of G'' f'' x✝¹) (((g₂ x✝¹).comp (g₁ x✝¹)) x✝)

Tactic:
rfl

Result:
no goals

Proof state:
case mk
ι : Type u_2
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (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✝² : DirectLimit G f
x : DirectSum ι G
x✝¹ : ι
x✝ : G x✝¹
⊢ ((map g₂ hg₂).comp (map g₁ hg₁))
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid)
        ((DirectSum.of G x✝¹) x✝)) =
    (map (fun i => (g₂ i).comp (g₁ i)) ⋯)
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid)
        ((DirectSum.of G x✝¹) x✝))

Tactic:
show map g₂ hg₂ (map g₁ hg₁ <| of _ _ _ _) = map _ _ (of _ _ _ _)

Result:
case mk
ι : Type u_2
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (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✝² : DirectLimit G f
x : DirectSum ι G
x✝¹ : ι
x✝ : G x✝¹
⊢ (map g₂ hg₂) ((map g₁ hg₁) ((of G f x✝¹) x✝)) = (map (fun i => (g₂ i).comp (g₁ i)) ⋯) ((of G f x✝¹) x✝)