-- Mathlib/Algebra/Colimit/Module.lean
@[simp] lemma map_id :
    map (fun _ ↦ AddMonoidHom.id _) (fun _ _ _ ↦ rfl) = AddMonoidHom.id (DirectLimit G f) :=
  DFunLike.ext _ _ <| by
    rintro ⟨x⟩; refine x.induction_on (by simp) (fun _ ↦ map_apply_of _ _) (by simp +contextual)

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 ι
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (map (fun x => AddMonoidHom.id (G x)) ⋯)
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) 0) =
    (AddMonoidHom.id (DirectLimit G f))
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) 0)

Tactic:
simp

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 ι
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ ∀ (x y : DirectSum ι fun i => G i),
    (map (fun x => AddMonoidHom.id (G x)) ⋯)
          (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) =
        (AddMonoidHom.id (DirectLimit G f))
          (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) →
      (map (fun x => AddMonoidHom.id (G x)) ⋯)
            (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) y) =
          (AddMonoidHom.id (DirectLimit G f))
            (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) y) →
        (map (fun x => AddMonoidHom.id (G x)) ⋯)
            (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid)
              (x + y)) =
          (AddMonoidHom.id (DirectLimit G f))
            (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 ι
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (map (fun x => AddMonoidHom.id (G x)) ⋯)
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) =
    (AddMonoidHom.id (DirectLimit G f))
      (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 _ ↦ map_apply_of _ _) (by simp +contextual)

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 ι
⊢ ∀ (x : DirectLimit G f), (map (fun x => AddMonoidHom.id (G x)) ⋯) x = (AddMonoidHom.id (DirectLimit G f)) 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 ι
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (map (fun x => AddMonoidHom.id (G x)) ⋯)
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) =
    (AddMonoidHom.id (DirectLimit G f))
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x)