-- 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:
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 y : DirectSum ι fun i => G i),
    (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) →
      (map g₂ hg₂ ∘ₗ map g₁ hg₁) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) y) =
          (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) y) →
        (map g₂ hg₂ ∘ₗ map g₁ hg₁) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) (x + y)) =
          (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) (x + y))

Tactic:
simp +contextual

Result:
no goals

Proof state:
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
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] 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)
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
i j : ι
h : i ≤ j
⊢ (fun i => g₂ i ∘ₗ g₁ i) j ∘ₗ f i j h = f'' i j h ∘ₗ (fun i => g₂ i ∘ₗ g₁ i) i

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

Result:
no goals

Proof state:
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), (map g₂ hg₂ ∘ₗ map g₁ hg₁) x = (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) x

Tactic:
rintro ⟨x⟩

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
⊢ (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)

Proof state:
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) 0) =
    (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) 0)

Tactic:
simp

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₁) ((of R ι G f x✝¹) x✝)) = (map (fun i => g₂ i ∘ₗ g₁ i) ⋯) ((of R ι G f x✝¹) x✝)

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