[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
j : J
⊢ AddCommGroup ((F ⋙ forget (ModuleCat R)).obj j)
[PROOFSTEP]
change AddCommGroup (F.obj j)
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
j : J
⊢ AddCommGroup ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
j : J
⊢ Module R ((F ⋙ forget (ModuleCat R)).obj j)
[PROOFSTEP]
change Module R (F.obj j)
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
j : J
⊢ Module R ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
src✝ : AddSubgroup
  ((j : J) → ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat).obj j)) :=
  AddGroupCat.sectionsAddSubgroup (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat)
r : R
s : (j : J) → ↑(F.obj j)
sh :
  s ∈
    {
          toAddSubsemigroup :=
            { carrier := Functor.sections (F ⋙ forget (ModuleCat R)),
              add_mem' :=
                (_ : ∀ {a b : (j : J) → ↑(F.obj j)}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier) },
          zero_mem' :=
            (_ :
              ∀ {j j' : J} (f : j ⟶ j'),
                ((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                        forget AddGroupCat).map
                    f (OfNat.ofNat 0 j) =
                  OfNat.ofNat 0 j') }.toAddSubsemigroup.carrier
j j' : J
f : j ⟶ j'
⊢ (F ⋙ forget (ModuleCat R)).map f ((r • s) j) = (r • s) j'
[PROOFSTEP]
simp only [forget_map, Functor.comp_map, Pi.smul_apply, map_smul]
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
src✝ : AddSubgroup
  ((j : J) → ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat).obj j)) :=
  AddGroupCat.sectionsAddSubgroup (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat)
r : R
s : (j : J) → ↑(F.obj j)
sh :
  s ∈
    {
          toAddSubsemigroup :=
            { carrier := Functor.sections (F ⋙ forget (ModuleCat R)),
              add_mem' :=
                (_ : ∀ {a b : (j : J) → ↑(F.obj j)}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier) },
          zero_mem' :=
            (_ :
              ∀ {j j' : J} (f : j ⟶ j'),
                ((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat) ⋙
                        forget AddGroupCat).map
                    f (OfNat.ofNat 0 j) =
                  OfNat.ofNat 0 j') }.toAddSubsemigroup.carrier
j j' : J
f : j ⟶ j'
⊢ r • ↑(F.map f) (s j) = r • s j'
[PROOFSTEP]
dsimp [Functor.sections] at sh 
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
src✝ : AddSubgroup
  ((j : J) → ↑((F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat).obj j)) :=
  AddGroupCat.sectionsAddSubgroup (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat ⋙ forget₂ AddCommGroupCat AddGroupCat)
r : R
s : (j : J) → ↑(F.obj j)
sh : s ∈ {u | ∀ {j j' : J} (f : j ⟶ j'), ↑(F.map f) (u j) = u j'}
j j' : J
f : j ⟶ j'
⊢ r • ↑(F.map f) (s j) = r • s j'
[PROOFSTEP]
rw [sh f]
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
⊢ AddCommMonoid { x // x ∈ sectionsSubmodule F }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
⊢ AddCommGroup { x // x ∈ sectionsSubmodule F }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
⊢ Module R { x // x ∈ sectionsSubmodule F }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
⊢ IsLimit (limitCone F)
[PROOFSTEP]
refine'
  IsLimit.ofFaithful (forget (ModuleCat R)) (Types.limitConeIsLimit.{v, w} _)
    (fun s => ⟨⟨(Types.limitConeIsLimit.{v, w} _).lift ((forget (ModuleCat R)).mapCone s), _⟩, _⟩) (fun s => rfl)
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
⊢ ∀ (x y : ↑s.pt),
    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) (x + y) =
      IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) x +
        IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) y
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
⊢ ∀ (r : R) (x : ↑s.pt),
    AddHom.toFun
        { toFun := IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
          map_add' := ?refine'_1 }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          {
            toFun :=
              IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
            map_add' := ?refine'_1 }
          x
[PROOFSTEP]
all_goals
  intros
  dsimp [Types.limitConeIsLimit]
  simp
  rfl
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
⊢ ∀ (x y : ↑s.pt),
    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) (x + y) =
      IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) x +
        IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
x✝ y✝ : ↑s.pt
⊢ IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) (x✝ + y✝) =
    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) x✝ +
      IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) y✝
[PROOFSTEP]
dsimp [Types.limitConeIsLimit]
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
x✝ y✝ : ↑s.pt
⊢ { val := fun j => ↑(NatTrans.app s.π j) (x✝ + y✝),
      property :=
        (_ :
          ∀ {j j' : J} (f : j ⟶ j'),
            (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) (x✝ + y✝) =
              NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' (x✝ + y✝)) } =
    { val := fun j => ↑(NatTrans.app s.π j) x✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) x✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' x✝) } +
      { val := fun j => ↑(NatTrans.app s.π j) y✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) y✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' y✝) }
[PROOFSTEP]
simp
[GOAL]
case refine'_1
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
x✝ y✝ : ↑s.pt
⊢ { val := fun j => ↑(NatTrans.app s.π j) x✝ + ↑(NatTrans.app s.π j) y✝,
      property :=
        (_ :
          (fun x => x ∈ Functor.sections (F ⋙ forget (ModuleCat R))) fun j =>
            ↑(NatTrans.app s.π j) x✝ + ↑(NatTrans.app s.π j) y✝) } =
    { val := fun j => ↑(NatTrans.app s.π j) x✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) x✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' x✝) } +
      { val := fun j => ↑(NatTrans.app s.π j) y✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) y✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' y✝) }
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
⊢ ∀ (r : R) (x : ↑s.pt),
    AddHom.toFun
        { toFun := IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
          map_add' :=
            (_ :
              ∀ (x y : ↑s.pt),
                IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                    (x + y) =
                  IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      x +
                    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      y) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          {
            toFun :=
              IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
            map_add' :=
              (_ :
                ∀ (x y : ↑s.pt),
                  IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      (x + y) =
                    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                        x +
                      IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R)))
                        ((forget (ModuleCat R)).mapCone s) y) }
          x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
r✝ : R
x✝ : ↑s.pt
⊢ AddHom.toFun
      { toFun := IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
        map_add' :=
          (_ :
            ∀ (x y : ↑s.pt),
              IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                  (x + y) =
                IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s) x +
                  IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                    y) }
      (r✝ • x✝) =
    ↑(RingHom.id R) r✝ •
      AddHom.toFun
        { toFun := IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s),
          map_add' :=
            (_ :
              ∀ (x y : ↑s.pt),
                IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                    (x + y) =
                  IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      x +
                    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget (ModuleCat R))) ((forget (ModuleCat R)).mapCone s)
                      y) }
        x✝
[PROOFSTEP]
dsimp [Types.limitConeIsLimit]
[GOAL]
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
r✝ : R
x✝ : ↑s.pt
⊢ { val := fun j => ↑(NatTrans.app s.π j) (r✝ • x✝),
      property :=
        (_ :
          ∀ {j j' : J} (f : j ⟶ j'),
            (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) (r✝ • x✝) =
              NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' (r✝ • x✝)) } =
    r✝ •
      { val := fun j => ↑(NatTrans.app s.π j) x✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) x✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' x✝) }
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ModuleCatMax R
s : Cone F
r✝ : R
x✝ : ↑s.pt
⊢ { val := fun j => r✝ • ↑(NatTrans.app s.π j) x✝,
      property :=
        (_ : (fun x => x ∈ Functor.sections (F ⋙ forget (ModuleCat R))) fun j => r✝ • ↑(NatTrans.app s.π j) x✝) } =
    r✝ •
      { val := fun j => ↑(NatTrans.app s.π j) x✝,
        property :=
          (_ :
            ∀ {j j' : J} (f : j ⟶ j'),
              (NatTrans.app ((forget (ModuleCat R)).mapCone s).π j ≫ (F ⋙ forget (ModuleCat R)).map f) x✝ =
                NatTrans.app ((forget (ModuleCat R)).mapCone s).π j' x✝) }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
i : ι
⊢ { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (𝟙 i) =
    𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
i : ι
⊢ ∀ (x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)),
    ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (𝟙 i)) x =
      ↑(𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)) x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
i : ι
x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)
⊢ ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (𝟙 i)) x =
    ↑(𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj i)) x
[PROOFSTEP]
apply Module.DirectedSystem.map_self
[GOAL]
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
⊢ { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (hij ≫ hjk) =
    { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hij ≫
      { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hjk
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
⊢ ∀ (x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj X✝)),
    ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (hij ≫ hjk)) x =
      ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hij ≫
            { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hjk)
        x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj X✝)
⊢ ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (hij ≫ hjk)) x =
    ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hij ≫
          { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hjk)
      x
[PROOFSTEP]
symm
[GOAL]
case h
R : Type u
inst✝⁵ : Ring R
J : Type v
inst✝⁴ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h => ↑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.obj X✝)
⊢ ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hij ≫
          { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map hjk)
      x =
    ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y (_ : X ≤ Y) }.map (hij ≫ hjk)) x
[PROOFSTEP]
apply Module.DirectedSystem.map_map
[GOAL]
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝ : DecidableEq ι
x✝¹ x✝ : ι
hij : x✝¹ ⟶ x✝
⊢ (directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝ =
    DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝ : DecidableEq ι
x✝¹ x✝ : ι
hij : x✝¹ ⟶ x✝
⊢ ∀ (x : ↑((directLimitDiagram G f).obj x✝¹)),
    ↑((directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝) x =
      ↑(DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij) x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝ : DecidableEq ι
x✝¹ x✝ : ι
hij : x✝¹ ⟶ x✝
x : ↑((directLimitDiagram G f).obj x✝¹)
⊢ ↑((directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝) x =
    ↑(DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij) x
[PROOFSTEP]
exact DirectLimit.of_f
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
rw [← s.w (homOfLE h)]
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑((directLimitDiagram G f).map (homOfLE h) ≫ NatTrans.app s.ι j) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
⊢ NatTrans.app (directLimitCocone G f).ι i ≫
      (fun s =>
          DirectLimit.lift R ι G f s.ι.app
            (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
        s =
    NatTrans.app s.ι i
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
⊢ ∀ (x : ↑((directLimitDiagram G f).obj i)),
    ↑(NatTrans.app (directLimitCocone G f).ι i ≫
            (fun s =>
                DirectLimit.lift R ι G f s.ι.app
                  (_ :
                    ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
              s)
        x =
      ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
x : ↑((directLimitDiagram G f).obj i)
⊢ ↑(NatTrans.app (directLimitCocone G f).ι i ≫
          (fun s =>
              DirectLimit.lift R ι G f s.ι.app
                (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
            s)
      x =
    ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
dsimp only [directLimitCocone, CategoryStruct.comp]
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
x : ↑((directLimitDiagram G f).obj i)
⊢ ↑(LinearMap.comp
          (DirectLimit.lift R ι G f s.ι.app
            (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
          (DirectLimit.of R ι G f i))
      x =
    ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
rw [LinearMap.comp_apply]
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
i : ι
x : ↑((directLimitDiagram G f).obj i)
⊢ ↑(DirectLimit.lift R ι G f s.ι.app
          (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
      (↑(DirectLimit.of R ι G f i) x) =
    ↑(NatTrans.app s.ι i) x
[PROOFSTEP]
apply DirectLimit.lift_of
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun s =>
        DirectLimit.lift R ι G f s.ι.app
          (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
      s
[PROOFSTEP]
have : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i) :=
  by
  funext i
  rw [← h]
  rfl
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
⊢ s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
[PROOFSTEP]
funext i
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
i : ι
⊢ NatTrans.app s.ι i = LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
[PROOFSTEP]
rw [← h]
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
i : ι
⊢ NatTrans.app (directLimitCocone G f).ι i ≫ m =
    LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
this : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
⊢ m =
    (fun s =>
        DirectLimit.lift R ι G f s.ι.app
          (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
      s
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
this : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
⊢ ∀ (x : ↑(directLimitCocone G f).pt),
    ↑m x =
      ↑((fun s =>
              DirectLimit.lift R ι G f s.ι.app
                (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
            s)
        x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
this : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
x : ↑(directLimitCocone G f).pt
⊢ ↑m x =
    ↑((fun s =>
            DirectLimit.lift R ι G f s.ι.app
              (_ : ∀ (i j : ι) (h : i ≤ j) (x : G i), ↑(NatTrans.app s.ι j) (↑(f i j h) x) = ↑(NatTrans.app s.ι i) x))
          s)
      x
[PROOFSTEP]
simp only [this]
[GOAL]
case h
R : Type u
inst✝⁸ : Ring R
J : Type v
inst✝⁷ : SmallCategory J
ι : Type v
dec_ι : DecidableEq ι
inst✝⁶ : Preorder ι
G : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DirectedSystem G fun i j h => ↑(f i j h)
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (directLimitCocone G f).ι j ≫ m = NatTrans.app s.ι j
this : s.ι.app = fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)
x : ↑(directLimitCocone G f).pt
⊢ ↑m x =
    ↑(DirectLimit.lift R ι G f (fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i))
          (_ :
            ∀ (i j : ι) (hij : i ≤ j) (x : G i),
              ↑((fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)) j)
                  (↑(f i j hij) x) =
                ↑((fun i => LinearMap.comp m (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)) i) x))
      x
[PROOFSTEP]
apply Module.DirectLimit.lift_unique
