-- 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:
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)

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

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₂).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✝))

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : 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 ι
P : Type u_4
inst✝² : AddCommMonoid 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
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)
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 [AddMonoidHom.comp_assoc, hg₁ i, ← AddMonoidHom.comp_assoc, hg₂ i,
  AddMonoidHom.comp_assoc]

Result:
no goals

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
x : DirectSum ι G
⊢ ∀ (x y : DirectSum ι fun i => G i),
    ((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) →
      ((map g₂ hg₂).comp (map g₁ hg₁))
            (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) y) =
          (map (fun i => (g₂ i).comp (g₁ i)) ⋯)
            (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) y) →
        ((map g₂ hg₂).comp (map g₁ hg₁))
            (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid)
              (x + y)) =
          (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 + y))

Tactic:
simp +contextual

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₂) ((map g₁ hg₁) ((of G f x✝¹) x✝)) = (map (fun i => (g₂ i).comp (g₁ i)) ⋯) ((of G f x✝¹) x✝)

Tactic:
simp_rw [map_apply_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✝¹
⊢ (of G'' f'' x✝¹) ((g₂ x✝¹) ((g₁ x✝¹) x✝)) = (of G'' f'' x✝¹) (((g₂ x✝¹).comp (g₁ x✝¹)) x✝)

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
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) 0) =
    (map (fun i => (g₂ i).comp (g₁ i)) ⋯)
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) 0)

Tactic:
simp

Result:
no goals