[GOAL]
G H : AddCommGroupCat
⊢ ∀ ⦃X Y : Discrete WalkingPair⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete WalkingPair)).obj (of (↑G × ↑H))).map f ≫
        (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H))
          Y =
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H)) X ≫
        (pair G H).map f
[PROOFSTEP]
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟨⟩⟩⟩
[GOAL]
case mk.left.mk.left.up.up.refl
G H : AddCommGroupCat
⊢ ((Functor.const (Discrete WalkingPair)).obj (of (↑G × ↑H))).map
        { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } } ≫
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H))
        { as := WalkingPair.left } =
    (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H))
        { as := WalkingPair.left } ≫
      (pair G H).map { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } }
[PROOFSTEP]
rfl
[GOAL]
case mk.right.mk.right.up.up.refl
G H : AddCommGroupCat
⊢ ((Functor.const (Discrete WalkingPair)).obj (of (↑G × ↑H))).map
        { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } } ≫
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H))
        { as := WalkingPair.right } =
    (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H))
        { as := WalkingPair.right } ≫
      (pair G H).map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } }
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
⊢ ∀ (s : Cone (pair G H)) (j : Discrete WalkingPair),
    (fun s =>
            AddMonoidHom.prod (NatTrans.app s.π { as := WalkingPair.left })
              (NatTrans.app s.π { as := WalkingPair.right }))
          s ≫
        NatTrans.app
          { pt := of (↑G × ↑H),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j =>
                    WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H) }.π
          j =
      NatTrans.app s.π j
[PROOFSTEP]
rintro s (⟨⟩ | ⟨⟩)
[GOAL]
case mk.left
G H : AddCommGroupCat
s : Cone (pair G H)
⊢ (fun s =>
          AddMonoidHom.prod (NatTrans.app s.π { as := WalkingPair.left })
            (NatTrans.app s.π { as := WalkingPair.right }))
        s ≫
      NatTrans.app
        { pt := of (↑G × ↑H),
            π :=
              NatTrans.mk fun j =>
                Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H) }.π
        { as := WalkingPair.left } =
    NatTrans.app s.π { as := WalkingPair.left }
[PROOFSTEP]
rfl
[GOAL]
case mk.right
G H : AddCommGroupCat
s : Cone (pair G H)
⊢ (fun s =>
          AddMonoidHom.prod (NatTrans.app s.π { as := WalkingPair.left })
            (NatTrans.app s.π { as := WalkingPair.right }))
        s ≫
      NatTrans.app
        { pt := of (↑G × ↑H),
            π :=
              NatTrans.mk fun j =>
                Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H) }.π
        { as := WalkingPair.right } =
    NatTrans.app s.π { as := WalkingPair.right }
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
s : Cone (pair G H)
m :
  s.pt ⟶
    { pt := of (↑G × ↑H),
        π :=
          NatTrans.mk fun j =>
            Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        NatTrans.app
          { pt := of (↑G × ↑H),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j =>
                    WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H) }.π
          j =
      NatTrans.app s.π j
⊢ m =
    (fun s =>
        AddMonoidHom.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
      s
[PROOFSTEP]
simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]
[GOAL]
G H : AddCommGroupCat
s : Cone (pair G H)
m :
  s.pt ⟶
    { pt := of (↑G × ↑H),
        π :=
          NatTrans.mk fun j =>
            Discrete.casesOn j fun j => WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        NatTrans.app
          { pt := of (↑G × ↑H),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j =>
                    WalkingPair.casesOn j (AddMonoidHom.fst ↑G ↑H) (AddMonoidHom.snd ↑G ↑H) }.π
          j =
      NatTrans.app s.π j
⊢ m = AddMonoidHom.prod (m ≫ AddMonoidHom.fst ↑G ↑H) (m ≫ AddMonoidHom.snd ↑G ↑H)
[PROOFSTEP]
rfl
[GOAL]
J : Type w
f : J → AddCommGroupCat
s : Fan f
⊢ (fun x j => ↑(NatTrans.app s.π { as := j }) x) 0 = 0
[PROOFSTEP]
simp only [Functor.const_obj_obj, map_zero]
[GOAL]
J : Type w
f : J → AddCommGroupCat
s : Fan f
⊢ (fun j => 0) = 0
[PROOFSTEP]
rfl
[GOAL]
J : Type w
f : J → AddCommGroupCat
s : Fan f
x y : ↑s.pt
⊢ ZeroHom.toFun
      { toFun := fun x j => ↑(NatTrans.app s.π { as := j }) x,
        map_zero' := (_ : (fun x j => ↑(NatTrans.app s.π { as := j }) x) 0 = 0) }
      (x + y) =
    ZeroHom.toFun
        { toFun := fun x j => ↑(NatTrans.app s.π { as := j }) x,
          map_zero' := (_ : (fun x j => ↑(NatTrans.app s.π { as := j }) x) 0 = 0) }
        x +
      ZeroHom.toFun
        { toFun := fun x j => ↑(NatTrans.app s.π { as := j }) x,
          map_zero' := (_ : (fun x j => ↑(NatTrans.app s.π { as := j }) x) 0 = 0) }
        y
[PROOFSTEP]
simp only [Functor.const_obj_obj, map_add]
[GOAL]
J : Type w
f : J → AddCommGroupCat
s : Fan f
x y : ↑s.pt
⊢ (fun j => ↑(NatTrans.app s.π { as := j }) x + ↑(NatTrans.app s.π { as := j }) y) =
    (fun j => ↑(NatTrans.app s.π { as := j }) x) + fun j => ↑(NatTrans.app s.π { as := j }) y
[PROOFSTEP]
rfl
[GOAL]
J : Type w
f : J → AddCommGroupCat
s : Cone (Discrete.functor f)
m :
  s.pt ⟶ { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.π
          j =
      NatTrans.app s.π j
⊢ m = lift f s
[PROOFSTEP]
ext x
[GOAL]
case w
J : Type w
f : J → AddCommGroupCat
s : Cone (Discrete.functor f)
m :
  s.pt ⟶ { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.π
          j =
      NatTrans.app s.π j
x : ↑s.pt
⊢ ↑m x = ↑(lift f s) x
[PROOFSTEP]
funext j
[GOAL]
case w.h
J : Type w
f : J → AddCommGroupCat
s : Cone (Discrete.functor f)
m :
  s.pt ⟶ { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.π
          j =
      NatTrans.app s.π j
x : ↑s.pt
j : J
⊢ ↑m x j = ↑(lift f s) x j
[PROOFSTEP]
exact congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩)


[GOAL]
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
⊢ AddHom.toFun
      { toFun := ↑f,
        map_add' :=
          (_ :
            ∀ (a b : ↑A),
              ↑(let_fun this := f;
                    this)
                  (a + b) =
                ↑(let_fun this := f;
                      this)
                    a +
                  ↑(let_fun this := f;
                      this)
                    b) }
      (n • x) =
    ↑(RingHom.id ℤ) n •
      AddHom.toFun
        { toFun := ↑f,
          map_add' :=
            (_ :
              ∀ (a b : ↑A),
                ↑(let_fun this := f;
                      this)
                    (a + b) =
                  ↑(let_fun this := f;
                        this)
                      a +
                    ↑(let_fun this := f;
                        this)
                      b) }
        x
[PROOFSTEP]
convert AddMonoidHom.map_zsmul (show A.carrier →+ B.carrier from f) x n
[GOAL]
case h.e'_2.h.e'_1.h.e'_4.h.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
⊢ SMulZeroClass.toSMul = SubNegMonoid.SMulInt
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.e'_4.h.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
⊢ SMulZeroClass.toSMul = SubNegMonoid.SMulInt
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h.e'_1.h.e'_4.h.e'_3.smul.h.h
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
x✝¹ : ℤ
x✝ : ↑A
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
[PROOFSTEP]
apply int_smul_eq_zsmul
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.smul.h.h
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGroupCat).obj B
n : ℤ
x : ↑A
x✝¹ : (fun x => ℤ) n
x✝ : ↑B
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
[PROOFSTEP]
apply int_smul_eq_zsmul


[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case h
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * (b✝ + c✝)) x✝ = (a✝ * b✝ + a✝ * c✝) x✝
[PROOFSTEP]
exact mul_add _ _ _
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case h
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ ((a✝ + b✝) * c✝) x✝ = (a✝ * c✝ + b✝ * c✝) x✝
[PROOFSTEP]
exact add_mul _ _ _


[GOAL]
⊢ ConcreteCategory BoolRingCat
[PROOFSTEP]
dsimp [BoolRingCat]
[GOAL]
⊢ ConcreteCategory (Bundled BooleanRing)
[PROOFSTEP]
infer_instance
  -- Porting note: disabled `simps`
  --   Invalid simp lemma BoolRingCat.hasForgetToCommRing_forget₂_obj_str_add.
  --   The given definition is not a constructor application:
  --     inferInstance.1
  -- @[simps]
[GOAL]
α β : BoolRingCat
e : ↑α ≃+* ↑β
⊢ ↑e ≫ ↑(RingEquiv.symm e) = 𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : BoolRingCat
e : ↑α ≃+* ↑β
x✝ : (forget BoolRingCat).obj α
⊢ ↑(↑e ≫ ↑(RingEquiv.symm e)) x✝ = ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : BoolRingCat
e : ↑α ≃+* ↑β
⊢ ↑(RingEquiv.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : BoolRingCat
e : ↑α ≃+* ↑β
x✝ : (forget BoolRingCat).obj β
⊢ ↑(↑(RingEquiv.symm e) ≫ ↑e) x✝ = ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hf : LinearMap.ker f = ⊥
⊢ Function.Injective ↑f
[PROOFSTEP]
convert LinearMap.ker_eq_bot.1 hf
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [epi_iff_range_eq_top, LinearMap.range_eq_top]
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi ((forget (ModuleCat R)).map f)
[PROOFSTEP]
erw [CategoryTheory.epi_iff_surjective, ← epi_iff_surjective]
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi f
[PROOFSTEP]
exact hf
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono ((forget (ModuleCat R)).map f)
[PROOFSTEP]
erw [CategoryTheory.mono_iff_injective, ← mono_iff_injective]
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono f
[PROOFSTEP]
exact hf


[GOAL]
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
j : Discrete ι
⊢ (fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s ≫ NatTrans.app (productCone Z).π j =
    NatTrans.app s.π j
[PROOFSTEP]
cases j
[GOAL]
case mk
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
as✝ : ι
⊢ (fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s ≫ NatTrans.app (productCone Z).π { as := as✝ } =
    NatTrans.app s.π { as := as✝ }
[PROOFSTEP]
aesop
[GOAL]
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ NatTrans.app (productCone Z).π j = NatTrans.app s.π j
⊢ m = (fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ NatTrans.app (productCone Z).π j = NatTrans.app s.π j
x : ↑s.pt
⊢ ↑m x = ↑((fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s) x
[PROOFSTEP]
funext i
[GOAL]
case h.h
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ NatTrans.app (productCone Z).π j = NatTrans.app s.π j
x : ↑s.pt
i : ι
⊢ ↑m x i = ↑((fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s) x i
[PROOFSTEP]
exact LinearMap.congr_fun (w ⟨i⟩) x


[GOAL]
G : GroupCat
inst✝ : Subsingleton ↑G
⊢ IsZero G
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : G ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.w
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : G ⟶ X
x : ↑G
⊢ ↑f x = ↑default x
[PROOFSTEP]
have : x = 1 := Subsingleton.elim _ _
[GOAL]
case refine'_1.w
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ ↑f x = ↑default x
[PROOFSTEP]
rw [this, map_one, map_one]
[GOAL]
case refine'_2
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : X ⟶ G
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : X ⟶ G
x✝ : ↑X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
G : CommGroupCat
inst✝ : Subsingleton ↑G
⊢ IsZero G
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : G ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.w
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : G ⟶ X
x : ↑G
⊢ ↑f x = ↑default x
[PROOFSTEP]
have : x = 1 := Subsingleton.elim _ _
[GOAL]
case refine'_1.w
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ ↑f x = ↑default x
[PROOFSTEP]
rw [this, map_one, map_one]
[GOAL]
case refine'_2
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : X ⟶ G
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : X ⟶ G
x✝ : ↑X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
apply Subsingleton.elim


[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
⊢ coconeFun F j 0 = 0
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
⊢ Setoid.r (Prequotient.of j 0) zero
[PROOFSTEP]
apply Relation.zero
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
⊢ ∀ (x y : ↑(F.obj j)),
    ZeroHom.toFun
        { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) }
        (x + y) =
      ZeroHom.toFun
          { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) }
          x +
        ZeroHom.toFun
          { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) } y
[PROOFSTEP]
intros
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ ZeroHom.toFun
      { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) }
      (x✝ + y✝) =
    ZeroHom.toFun
        { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) }
        x✝ +
      ZeroHom.toFun
        { toFun := coconeFun F j, map_zero' := (_ : Quot.mk Setoid.r (Prequotient.of j 0) = Quot.mk Setoid.r zero) } y✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j (x✝ + y✝)) (add (Prequotient.of j x✝) (Prequotient.of j y✝))
[PROOFSTEP]
apply Relation.add
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case w.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
[PROOFSTEP]
apply Relation.map
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(coconeMorphism F j) x
[PROOFSTEP]
rw [← cocone_naturality F f]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(F.map f ≫ coconeMorphism F j') x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
⊢ ColimitType F → ↑s.pt
[PROOFSTEP]
fapply Quot.lift
[GOAL]
case f
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
⊢ Prequotient F → ↑s.pt
[PROOFSTEP]
exact descFunLift F s
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), Setoid.r a b → descFunLift F s a = descFunLift F s b
[PROOFSTEP]
intro x y r
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction r with
| refl => rfl
| symm _ _ _ r_ih => exact r_ih.symm
| trans _ _ _ _ _ r_ih_h r_ih_k => exact Eq.trans r_ih_h r_ih_k
| map j j' f x => simpa only [descFunLift, Functor.const_obj_obj] using FunLike.congr_fun (s.ι.naturality f) x
| zero => simp
| neg => simp
| add => simp
| neg_1 _ _ _ r_ih => dsimp; rw [r_ih]
| add_1 _ _ _ _ r_ih => dsimp; rw [r_ih]
| add_2 _ _ _ _ r_ih => dsimp; rw [r_ih]
| zero_add => dsimp; rw [zero_add]
| add_zero => dsimp; rw [add_zero]
| add_left_neg => dsimp; rw [add_left_neg]
| add_comm => dsimp; rw [add_comm]
| add_assoc => dsimp; rw [add_assoc]
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction r with
| refl => rfl
| symm _ _ _ r_ih => exact r_ih.symm
| trans _ _ _ _ _ r_ih_h r_ih_k => exact Eq.trans r_ih_h r_ih_k
| map j j' f x => simpa only [descFunLift, Functor.const_obj_obj] using FunLike.congr_fun (s.ι.naturality f) x
| zero => simp
| neg => simp
| add => simp
| neg_1 _ _ _ r_ih => dsimp; rw [r_ih]
| add_1 _ _ _ _ r_ih => dsimp; rw [r_ih]
| add_2 _ _ _ _ r_ih => dsimp; rw [r_ih]
| zero_add => dsimp; rw [zero_add]
| add_zero => dsimp; rw [add_zero]
| add_left_neg => dsimp; rw [add_left_neg]
| add_comm => dsimp; rw [add_comm]
| add_assoc => dsimp; rw [add_assoc]
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]

| refl => rfl
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rfl
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
r_ih : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]

| symm _ _ _ r_ih => exact r_ih.symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
r_ih : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]
exact r_ih.symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
r_ih_h : descFunLift F s x✝² = descFunLift F s y✝
r_ih_k : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]

| trans _ _ _ _ _ r_ih_h r_ih_k => exact Eq.trans r_ih_h r_ih_k
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
r_ih_h : descFunLift F s x✝² = descFunLift F s y✝
r_ih_k : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]
exact Eq.trans r_ih_h r_ih_k
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' (↑(F.map f) x)) = descFunLift F s (Prequotient.of j x)
[PROOFSTEP]

| map j j' f x => simpa only [descFunLift, Functor.const_obj_obj] using FunLike.congr_fun (s.ι.naturality f) x
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' (↑(F.map f) x)) = descFunLift F s (Prequotient.of j x)
[PROOFSTEP]
simpa only [descFunLift, Functor.const_obj_obj] using FunLike.congr_fun (s.ι.naturality f) x
[GOAL]
case a.zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
⊢ descFunLift F s (Prequotient.of j✝ 0) = descFunLift F s zero
[PROOFSTEP]

| zero => simp
[GOAL]
case a.zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
⊢ descFunLift F s (Prequotient.of j✝ 0) = descFunLift F s zero
[PROOFSTEP]
simp
[GOAL]
case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (-x✝)) = descFunLift F s (neg (Prequotient.of j✝ x✝))
[PROOFSTEP]

| neg => simp
[GOAL]
case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (-x✝)) = descFunLift F s (neg (Prequotient.of j✝ x✝))
[PROOFSTEP]
simp
[GOAL]
case a.add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ y✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (x✝ + y✝)) = descFunLift F s (add (Prequotient.of j✝ x✝) (Prequotient.of j✝ y✝))
[PROOFSTEP]

| add => simp
[GOAL]
case a.add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : Prequotient F
j✝ : J
x✝ y✝ : ↑(F.obj j✝)
⊢ descFunLift F s (Prequotient.of j✝ (x✝ + y✝)) = descFunLift F s (add (Prequotient.of j✝ x✝) (Prequotient.of j✝ y✝))
[PROOFSTEP]
simp
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (neg x✝¹) = descFunLift F s (neg x'✝)
[PROOFSTEP]

| neg_1 _ _ _ r_ih => dsimp; rw [r_ih]
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (neg x✝¹) = descFunLift F s (neg x'✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ -descFunLift F s x✝¹ = -descFunLift F s x'✝
[PROOFSTEP]
rw [r_ih]
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (add x✝¹ y✝) = descFunLift F s (add x'✝ y✝)
[PROOFSTEP]

| add_1 _ _ _ _ r_ih => dsimp; rw [r_ih]
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (add x✝¹ y✝) = descFunLift F s (add x'✝ y✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
r_ih : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s x✝¹ + descFunLift F s y✝ = descFunLift F s x'✝ + descFunLift F s y✝
[PROOFSTEP]
rw [r_ih]
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
r_ih : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s (add x✝¹ y✝) = descFunLift F s (add x✝¹ y'✝)
[PROOFSTEP]

| add_2 _ _ _ _ r_ih => dsimp; rw [r_ih]
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
r_ih : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s (add x✝¹ y✝) = descFunLift F s (add x✝¹ y'✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
r_ih : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s x✝¹ + descFunLift F s y✝ = descFunLift F s x✝¹ + descFunLift F s y'✝
[PROOFSTEP]
rw [r_ih]
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add zero x✝) = descFunLift F s x✝
[PROOFSTEP]

| zero_add => dsimp; rw [zero_add]
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add zero x✝) = descFunLift F s x✝
[PROOFSTEP]
dsimp
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ 0 + descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rw [zero_add]
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add x✝ zero) = descFunLift F s x✝
[PROOFSTEP]

| add_zero => dsimp; rw [add_zero]
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add x✝ zero) = descFunLift F s x✝
[PROOFSTEP]
dsimp
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ + 0 = descFunLift F s x✝
[PROOFSTEP]
rw [add_zero]
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add (neg x✝) x✝) = descFunLift F s zero
[PROOFSTEP]

| add_left_neg => dsimp; rw [add_left_neg]
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add (neg x✝) x✝) = descFunLift F s zero
[PROOFSTEP]
dsimp
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ : Prequotient F
⊢ -descFunLift F s x✝ + descFunLift F s x✝ = 0
[PROOFSTEP]
rw [add_left_neg]
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s (add x✝ y✝) = descFunLift F s (add y✝ x✝)
[PROOFSTEP]

| add_comm => dsimp; rw [add_comm]
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s (add x✝ y✝) = descFunLift F s (add y✝ x✝)
[PROOFSTEP]
dsimp
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s x✝ + descFunLift F s y✝ = descFunLift F s y✝ + descFunLift F s x✝
[PROOFSTEP]
rw [add_comm]
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s (add (add x✝ y✝) z✝) = descFunLift F s (add x✝ (add y✝ z✝))
[PROOFSTEP]

| add_assoc => dsimp; rw [add_assoc]
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s (add (add x✝ y✝) z✝) = descFunLift F s (add x✝ (add y✝ z✝))
[PROOFSTEP]
dsimp
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s x✝ + descFunLift F s y✝ + descFunLift F s z✝ =
    descFunLift F s x✝ + (descFunLift F s y✝ + descFunLift F s z✝)
[PROOFSTEP]
rw [add_assoc]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : ↑(colimit F)
x✝¹ x✝ : Prequotient F
⊢ ZeroHom.toFun { toFun := descFun F s, map_zero' := (_ : descFun F s 0 = descFun F s 0) }
      (Quot.mk Setoid.r x✝¹ + Quot.mk Setoid.r x✝) =
    ZeroHom.toFun { toFun := descFun F s, map_zero' := (_ : descFun F s 0 = descFun F s 0) } (Quot.mk Setoid.r x✝¹) +
      ZeroHom.toFun { toFun := descFun F s, map_zero' := (_ : descFun F s 0 = descFun F s 0) } (Quot.mk Setoid.r x✝)
[PROOFSTEP]
dsimp [(· + ·)]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : ↑(colimit F)
x✝¹ x✝ : Prequotient F
⊢ descFun F s (Add.add (Quot.mk Setoid.r x✝¹) (Quot.mk Setoid.r x✝)) =
    Add.add (descFun F s (Quot.mk Setoid.r x✝¹)) (descFun F s (Quot.mk Setoid.r x✝))
[PROOFSTEP]
rw [← quot_add F]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
x y : ↑(colimit F)
x✝¹ x✝ : Prequotient F
⊢ descFun F s (Quot.mk Setoid.r (add x✝¹ x✝)) =
    Add.add (descFun F s (Quot.mk Setoid.r x✝¹)) (descFun F s (Quot.mk Setoid.r x✝))
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
[PROOFSTEP]
change (m : ColimitType F →+ s.pt) _ = (descMorphism F s : ColimitType F →+ s.pt) _
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction x using Prequotient.recOn with
| of j x => exact FunLike.congr_fun (w j) x
| zero =>
  dsimp only [quot_zero]
  rw [map_zero, map_zero]
| neg x ih =>
  dsimp only [quot_neg]
  rw [map_neg, map_neg, ih]
| add x y ihx ihy =>
  simp only [quot_add]
  erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction x using Prequotient.recOn with
| of j x => exact FunLike.congr_fun (w j) x
| zero =>
  dsimp only [quot_zero]
  rw [map_zero, map_zero]
| neg x ih =>
  dsimp only [quot_neg]
  rw [map_neg, map_neg, ih]
| add x y ihx ihy =>
  simp only [quot_add]
  erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
[GOAL]
case of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]

| of j x => exact FunLike.congr_fun (w j) x
[GOAL]
case of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]
exact FunLike.congr_fun (w j) x
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Quot Setoid.r
⊢ ↑m (Quot.mk Setoid.r zero) = ↑(descMorphism F s) (Quot.mk Setoid.r zero)
[PROOFSTEP]

| zero =>
  dsimp only [quot_zero]
  rw [map_zero, map_zero]
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Quot Setoid.r
⊢ ↑m (Quot.mk Setoid.r zero) = ↑(descMorphism F s) (Quot.mk Setoid.r zero)
[PROOFSTEP]
dsimp only [quot_zero]
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Quot Setoid.r
⊢ ↑m 0 = ↑(descMorphism F s) 0
[PROOFSTEP]
rw [map_zero, map_zero]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
⊢ ↑m (Quot.mk Setoid.r (neg x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (neg x))
[PROOFSTEP]

| neg x ih =>
  dsimp only [quot_neg]
  rw [map_neg, map_neg, ih]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
⊢ ↑m (Quot.mk Setoid.r (neg x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (neg x))
[PROOFSTEP]
dsimp only [quot_neg]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
⊢ ↑m (-Quot.mk Setoid.r x) = ↑(descMorphism F s) (-Quot.mk Setoid.r x)
[PROOFSTEP]
rw [map_neg, map_neg, ih]
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x y : Prequotient F
ihx : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
ihy : ↑m (Quot.mk Setoid.r y) = ↑(descMorphism F s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (add x y)) = ↑(descMorphism F s) (Quot.mk Setoid.r (add x y))
[PROOFSTEP]

| add x y ihx ihy =>
  simp only [quot_add]
  erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x y : Prequotient F
ihx : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
ihy : ↑m (Quot.mk Setoid.r y) = ↑(descMorphism F s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (add x y)) = ↑(descMorphism F s) (Quot.mk Setoid.r (add x y))
[PROOFSTEP]
simp only [quot_add]
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : Quot Setoid.r
x y : Prequotient F
ihx : ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
ihy : ↑m (Quot.mk Setoid.r y) = ↑(descMorphism F s) (Quot.mk Setoid.r y)
⊢ ↑m (Add.add (Quot.mk Setoid.r x) (Quot.mk Setoid.r y)) =
    ↑(descMorphism F s) (Add.add (Quot.mk Setoid.r x) (Quot.mk Setoid.r y))
[PROOFSTEP]
erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ f ≫ mk' (AddMonoidHom.range f) = 0
[PROOFSTEP]
ext x
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑(f ≫ mk' (AddMonoidHom.range f)) x = ↑0 x
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case w.a
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑f x ≈ 0
[PROOFSTEP]
apply leftRel_apply.mpr
[GOAL]
case w.a
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ -↑f x + 0 ∈ AddMonoidHom.range f
[PROOFSTEP]
fconstructor
[GOAL]
case w.a.w
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑G
case w.a.h G H : AddCommGroupCat f : G ⟶ H x : ↑G ⊢ ↑f ?w.a.w = -↑f x + 0
[PROOFSTEP]
exact -x
[GOAL]
case w.a.h
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑f (-x) = -↑f x + 0
[PROOFSTEP]
simp only [add_zero, AddMonoidHom.map_neg]
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
⊢ ↑(cokernel.π f) (↑f x) = 0
[PROOFSTEP]
exact cokernel.condition_apply f x
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ cokernel.desc f (mk' (AddMonoidHom.range f)) (_ : f ≫ mk' (AddMonoidHom.range f) = 0) ≫
      lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) =
    𝟙 (cokernel f)
[PROOFSTEP]
refine coequalizer.hom_ext ?_
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ coequalizer.π f 0 ≫
      cokernel.desc f (mk' (AddMonoidHom.range f)) (_ : f ≫ mk' (AddMonoidHom.range f) = 0) ≫
        lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) =
    coequalizer.π f 0 ≫ 𝟙 (cokernel f)
[PROOFSTEP]
simp only [coequalizer_as_cokernel, cokernel.π_desc_assoc, Category.comp_id]
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ mk' (AddMonoidHom.range f) ≫
      lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) =
    cokernel.π f
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) ≫
      cokernel.desc f (mk' (AddMonoidHom.range f)) (_ : f ≫ mk' (AddMonoidHom.range f) = 0) =
    𝟙 (of (↑H ⧸ AddMonoidHom.range f))
[PROOFSTEP]
ext x
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
x : ↑(of (↑H ⧸ AddMonoidHom.range f))
⊢ ↑(lift (AddMonoidHom.range f) (cokernel.π f) (_ : ∀ (x : ↑H), x ∈ AddMonoidHom.range f → ↑(cokernel.π f) x = 0) ≫
          cokernel.desc f (mk' (AddMonoidHom.range f)) (_ : f ≫ mk' (AddMonoidHom.range f) = 0))
      x =
    ↑(𝟙 (of (↑H ⧸ AddMonoidHom.range f))) x
[PROOFSTEP]
exact QuotientAddGroup.induction_on x <| cokernel.π_desc_apply f _ _


[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ∀ ⦃X Y : Discrete WalkingPair⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map f ≫
        (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N)) Y =
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N)) X ≫
        (pair M N).map f
[PROOFSTEP]
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟨⟩⟩⟩
[GOAL]
case mk.left.mk.left.up.up.refl
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map
        { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } } ≫
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N))
        { as := WalkingPair.left } =
    (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N))
        { as := WalkingPair.left } ≫
      (pair M N).map { down := { down := (_ : { as := WalkingPair.left }.as = { as := WalkingPair.left }.as) } }
[PROOFSTEP]
rfl
[GOAL]
case mk.right.mk.right.up.up.refl
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ((Functor.const (Discrete WalkingPair)).obj (of R (↑M × ↑N))).map
        { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } } ≫
      (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N))
        { as := WalkingPair.right } =
    (fun j => Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N))
        { as := WalkingPair.right } ≫
      (pair M N).map { down := { down := (_ : { as := WalkingPair.right }.as = { as := WalkingPair.right }.as) } }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
⊢ ∀ (s : Cone (pair M N)) (j : Discrete WalkingPair),
    (fun s =>
            LinearMap.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
          s ≫
        NatTrans.app
          { pt := of R (↑M × ↑N),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
          j =
      NatTrans.app s.π j
[PROOFSTEP]
rintro s (⟨⟩ | ⟨⟩)
[GOAL]
case mk.left
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ (fun s => LinearMap.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
        s ≫
      NatTrans.app
        { pt := of R (↑M × ↑N),
            π :=
              NatTrans.mk fun j =>
                Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
        { as := WalkingPair.left } =
    NatTrans.app s.π { as := WalkingPair.left }
[PROOFSTEP]
rfl
[GOAL]
case mk.right
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
⊢ (fun s => LinearMap.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
        s ≫
      NatTrans.app
        { pt := of R (↑M × ↑N),
            π :=
              NatTrans.mk fun j =>
                Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
        { as := WalkingPair.right } =
    NatTrans.app s.π { as := WalkingPair.right }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          NatTrans.mk fun j =>
            Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        NatTrans.app
          { pt := of R (↑M × ↑N),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
          j =
      NatTrans.app s.π j
⊢ m =
    (fun s =>
        LinearMap.prod (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right }))
      s
[PROOFSTEP]
simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          NatTrans.mk fun j =>
            Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        NatTrans.app
          { pt := of R (↑M × ↑N),
              π :=
                NatTrans.mk fun j =>
                  Discrete.casesOn j fun j => WalkingPair.casesOn j (LinearMap.fst R ↑M ↑N) (LinearMap.snd R ↑M ↑N) }.π
          j =
      NatTrans.app s.π j
⊢ m = LinearMap.prod (m ≫ LinearMap.fst R ↑M ↑N) (m ≫ LinearMap.snd R ↑M ↑N)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : ↑s.pt
⊢ (fun x j => ↑(NatTrans.app s.π { as := j }) x) (x + y) =
    (fun x j => ↑(NatTrans.app s.π { as := j }) x) x + (fun x j => ↑(NatTrans.app s.π { as := j }) x) y
[PROOFSTEP]
simp only [Functor.const_obj_obj, map_add]
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : ↑s.pt
⊢ (fun j => ↑(NatTrans.app s.π { as := j }) x + ↑(NatTrans.app s.π { as := j }) y) =
    (fun j => ↑(NatTrans.app s.π { as := j }) x) + fun j => ↑(NatTrans.app s.π { as := j }) y
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
r : R
x : ↑s.pt
⊢ AddHom.toFun
      { toFun := fun x j => ↑(NatTrans.app s.π { as := j }) x,
        map_add' :=
          (_ :
            ∀ (x y : ↑s.pt),
              (fun x j => ↑(NatTrans.app s.π { as := j }) x) (x + y) =
                (fun x j => ↑(NatTrans.app s.π { as := j }) x) x + (fun x j => ↑(NatTrans.app s.π { as := j }) x) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun x j => ↑(NatTrans.app s.π { as := j }) x,
          map_add' :=
            (_ :
              ∀ (x y : ↑s.pt),
                (fun x j => ↑(NatTrans.app s.π { as := j }) x) (x + y) =
                  (fun x j => ↑(NatTrans.app s.π { as := j }) x) x + (fun x j => ↑(NatTrans.app s.π { as := j }) x) y) }
        x
[PROOFSTEP]
simp only [Functor.const_obj_obj, map_smul]
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
r : R
x : ↑s.pt
⊢ (fun j => r • ↑(NatTrans.app s.π { as := j }) x) = ↑(RingHom.id R) r • fun j => ↑(NatTrans.app s.π { as := j }) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫ NatTrans.app { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.π j =
      NatTrans.app s.π j
⊢ m = lift f s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫ NatTrans.app { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.π j =
      NatTrans.app s.π j
x : ↑s.pt
⊢ ↑m x = ↑(lift f s) x
[PROOFSTEP]
funext j
[GOAL]
case h.h
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.pt
w :
  ∀ (j : Discrete J),
    m ≫ NatTrans.app { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.π j =
      NatTrans.app s.π j
x : ↑s.pt
j : J
⊢ ↑m x j = ↑(lift f s) x j
[PROOFSTEP]
exact congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩)