-- Mathlib/Algebra/Colimit/Module.lean
theorem lift_unique (F : DirectLimit G f →ₗ[R] P) (x) :
    F x = lift R ι G f (fun i ↦ F.comp <| of R ι G f i) (fun i j hij x ↦ by simp) x

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
x : DirectLimit G f
⊢ F x = (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) x

Tactic:
rcases x with ⟨x⟩

Result:
case mk
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ F (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) =
    (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x)

Proof state:
case mk
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ F (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) =
    (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).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✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ F (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) 0) =
    (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
F : DirectLimit G f →ₗ[R] P
x✝ : DirectLimit G f
i j : ι
hij : i ≤ j
x : G i
⊢ ((fun i => F ∘ₗ of R ι G f i) j) ((f i j hij) x) = ((fun i => F ∘ₗ of R ι G f i) i) x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ ∀ (x y : DirectSum ι fun i => G i),
    F (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) =
        (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) →
      F (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) y) =
          (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) y) →
        F (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) (x + y)) =
          (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) (x + y))

Tactic:
simp +contextual

Result:
no goals