-- Mathlib/Algebra/Colimit/Module.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:
ι : 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 ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ F (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) 0) =
    (lift G f P (fun i => F.comp (of G f i)) ⋯)
      (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 ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ ∀ (x y : DirectSum ι fun i => G i),
    F (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) =
        (lift G f P (fun i => F.comp (of G f i)) ⋯)
          (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) →
      F (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) y) =
          (lift G f P (fun i => F.comp (of G f i)) ⋯)
            (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) y) →
        F (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) (x + y)) =
          (lift G f P (fun i => F.comp (of G f i)) ⋯)
            (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 ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ F (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) =
    (lift G f P (fun i => F.comp (of G f i)) ⋯)
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x)

Tactic:
exact x.induction_on (by simp) (fun _ _ ↦ .symm <| lift_of ..) (by simp +contextual)

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
ι : 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 ι
P : Type u_4
inst✝ : AddCommMonoid 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_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝¹ : DecidableEq ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
x : DirectLimit G f
⊢ F x = (lift G f P (fun i => F.comp (of G f i)) ⋯) x

Tactic:
rcases x with ⟨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 ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ F (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x) =
    (lift G f P (fun i => F.comp (of G f i)) ⋯)
      (Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv fun i j hij => (f i j hij).toNatLinearMap)).toSetoid) x)