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

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

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)
x✝ : (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}))
        (FreeCommRing.of 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}))
        (FreeCommRing.of x✝))

Proof state:
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)
x✝ : (i : ι) × G i
⊢ (of G (fun x x_1 h => ⇑(f x x_1 h)) x✝.fst) ((RingHom.id (G x✝.fst)) x✝.snd) =
    (RingHom.id (DirectLimit G fun x x_1 h => ⇑(f x x_1 h))) ((of G (fun x x_1 h => ⇑(f x x_1 h)) x✝.fst) x✝.snd)

Tactic:
rfl

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 : 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}))
        (-1)) =
    (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}))
        (-1))

Tactic:
simp

Result:
no goals