-- Mathlib/Algebra/Colimit/Module.lean
lemma map_comp (g₁ : (i : ι) → G i →ₗ[R] G' i) (g₂ : (i : ι) → G' i →ₗ[R] G'' i)
    (hg₁ : ∀ i j h, g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i)
    (hg₂ : ∀ i j h, g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i) :
    (map g₂ hg₂ ∘ₗ map g₁ hg₁ :
      DirectLimit G f →ₗ[R] DirectLimit G'' f'') =
    (map (fun i ↦ g₂ i ∘ₗ g₁ i) fun i j h ↦ by
        rw [LinearMap.comp_assoc, hg₁ i, ← LinearMap.comp_assoc, hg₂ i, LinearMap.comp_assoc] :
      DirectLimit G f →ₗ[R] 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:
case mk
R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (map g₂ hg₂ ∘ₗ map g₁ hg₁) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) =
    (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x)

Tactic:
refine x.induction_on (by simp) (fun _ _ ↦ ?_) (by simp +contextual)

Result:
case mk
R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
x✝² : DirectLimit G f
x : DirectSum ι G
x✝¹ : ι
x✝ : G x✝¹
⊢ (map g₂ hg₂ ∘ₗ map g₁ hg₁) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) ((DirectSum.of G x✝¹) x✝)) =
    (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) ((DirectSum.of G x✝¹) x✝))

Proof state:
case mk
R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
x✝² : DirectLimit G f
x : DirectSum ι G
x✝¹ : ι
x✝ : G x✝¹
⊢ (of R ι G'' f'' x✝¹) ((g₂ x✝¹) ((g₁ x✝¹) x✝)) = (of R ι G'' f'' x✝¹) ((g₂ x✝¹ ∘ₗ g₁ x✝¹) x✝)

Tactic:
rfl

Result:
no goals

Proof state:
case mk
R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
x✝² : DirectLimit G f
x : DirectSum ι G
x✝¹ : ι
x✝ : G x✝¹
⊢ (map g₂ hg₂ ∘ₗ map g₁ hg₁) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) ((DirectSum.of G x✝¹) x✝)) =
    (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) ((DirectSum.of G x✝¹) x✝))

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

Result:
case mk
R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
x✝² : DirectLimit G f
x : DirectSum ι G
x✝¹ : ι
x✝ : G x✝¹
⊢ (map g₂ hg₂) ((map g₁ hg₁) ((of R ι G f x✝¹) x✝)) = (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) ((of R ι G f x✝¹) x✝)