no goals
R : Type u
inst✝⁵ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
P : Type u₁
inst✝² : AddCommGroup 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
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
F : DirectLimit G f →+ P
x✝ : DirectLimit G f
i j : ι
hij : i ≤ j
x : G i
⊢ ↑((fun i => AddMonoidHom.comp F (LinearMap.toAddMonoidHom (of G f i))) j) (↑(f i j hij) x) =
    ↑((fun i => AddMonoidHom.comp F (LinearMap.toAddMonoidHom (of G f i))) i) x
simp
no goals
R : Type u
inst✝⁵ : Ring R
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
P : Type u₁
inst✝² : AddCommGroup 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
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
F : DirectLimit G f →+ P
x✝ : DirectLimit G f
i : ι
x : G i
⊢ ↑F (↑(of G f i) x) =
    ↑(lift G f P (fun i => AddMonoidHom.comp F (LinearMap.toAddMonoidHom (of G f i)))
          (_ : ∀ (i j : ι) (hij : i ≤ j) (x : G i), ↑F (↑(of G f j) (↑(f i j hij) x)) = ↑F (↑(of G f i) x)))
      (↑(of G f i) x)
simp