-- Mathlib/Algebra/Colimit/Ring.lean
theorem lift_unique (F : DirectLimit G f →+* P) (x) :
    F x = lift G f P (fun i ↦ F.comp <| of G f i) (fun i j hij x ↦ by simp) 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
P : Type u_3
inst✝ : CommRing P
F : DirectLimit G f →+* P
x : FreeCommRing ((i : ι) × G i)
⊢ F
      ((Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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) =
    (lift G f P (fun i => F.comp (of G f i)) ⋯)
      ((Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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:
exact x.induction_on (by simp) (fun _ ↦ .symm <| lift_of ..)
  (by simp+contextual) (by 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
P : Type u_3
inst✝ : CommRing P
F : DirectLimit G f →+* P
x : FreeCommRing ((i : ι) × G i)
⊢ ∀ (x y : FreeCommRing ((i : ι) × G i)),
    F
          ((Ideal.Quotient.mk
              (Ideal.span
                {a |
                  (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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) =
        (lift G f P (fun i => F.comp (of G f i)) ⋯)
          ((Ideal.Quotient.mk
              (Ideal.span
                {a |
                  (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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) →
      F
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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) =
          (lift G f P (fun i => F.comp (of G f i)) ⋯)
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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) →
        F
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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)) =
          (lift G f P (fun i => F.comp (of G f i)) ⋯)
            ((Ideal.Quotient.mk
                (Ideal.span
                  {a |
                    (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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
P : Type u_3
inst✝ : CommRing 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
F : DirectLimit G f →+* P
x✝ : DirectLimit G f
i j : ι
hij : i ≤ j
x : G i
⊢ ((fun i => F.comp (of G f i)) j) (f i j hij x) = ((fun i => F.comp (of G f i)) i) x

Tactic:
simp

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
P : Type u_3
inst✝ : CommRing P
F : DirectLimit G f →+* P
x : FreeCommRing ((i : ι) × G i)
⊢ F
      ((Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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)) =
    (lift G f P (fun i => F.comp (of G f i)) ⋯)
      ((Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f 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