-- Mathlib/Algebra/Colimit/Ring.lean
@[simp] lemma map_id :
    map (fun _ ↦ RingHom.id _) (fun _ _ _ ↦ rfl) = RingHom.id (DirectLimit G fun _ _ h ↦ f _ _ h) :=
  DFunLike.ext _ _ fun x ↦ by
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    refine x.induction_on (by simp) (fun _ ↦ ?_) (by simp+contextual) (by simp+contextual)
    rw [quotientMk_of, map_apply_of]; rfl

Proof state:
ι : Type u_1
inst✝¹ : Preorder ι
G : ι → Type u_2
inst✝ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
x : FreeCommRing ((i : ι) × G i)
⊢ ∀ (x y : FreeCommRing ((i : ι) × G i)),
    (map (fun x => RingHom.id (G x)) ⋯)
          ((Ideal.Quotient.mk
              (Ideal.span
                {a |
                  (∃ i j,
                      ∃ (H : i ≤ j),
                        ∃ x, FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                    (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                      (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                        ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
            x) =
        (RingHom.id (DirectLimit G fun x x_1 h => ⇑(f x x_1 h)))
          ((Ideal.Quotient.mk
              (Ideal.span
                {a |
                  (∃ i j,
                      ∃ (H : i ≤ j),
                        ∃ x, FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                    (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                      (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                        ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
            x) →
      (map (fun x => RingHom.id (G x)) ⋯)
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j,
                        ∃ (H : i ≤ j),
                          ∃ x,
                            FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                      (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                        (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                          ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
              y) =
          (RingHom.id (DirectLimit G fun x x_1 h => ⇑(f x x_1 h)))
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j,
                        ∃ (H : i ≤ j),
                          ∃ x,
                            FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                      (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                        (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                          ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
              y) →
        (map (fun x => RingHom.id (G x)) ⋯)
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j,
                        ∃ (H : i ≤ j),
                          ∃ x,
                            FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                      (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                        (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                          ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
              (x + y)) =
          (RingHom.id (DirectLimit G fun x x_1 h => ⇑(f x x_1 h)))
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j,
                        ∃ (H : i ≤ j),
                          ∃ x,
                            FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                      (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                        (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                          ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
              (x + y))

Tactic:
simp+contextual

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Preorder ι
G : ι → Type u_2
inst✝ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
x : DirectLimit G fun x x_1 h => ⇑(f x x_1 h)
⊢ (map (fun x => RingHom.id (G x)) ⋯) x = (RingHom.id (DirectLimit G fun x x_1 h => ⇑(f x x_1 h))) x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Result:
case intro
ι : Type u_1
inst✝¹ : Preorder ι
G : ι → Type u_2
inst✝ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
x : FreeCommRing ((i : ι) × G i)
⊢ (map (fun x => RingHom.id (G x)) ⋯)
      ((Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j,
                  ∃ (H : i ≤ j),
                    ∃ x, FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                  (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                    ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
        x) =
    (RingHom.id (DirectLimit G fun x x_1 h => ⇑(f x x_1 h)))
      ((Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j,
                  ∃ (H : i ≤ j),
                    ∃ x, FreeCommRing.of ⟨j, (fun x x_1 h => ⇑(f x x_1 h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                  (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                    ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
        x)