[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
⊢ ∀ (x y : ↑(F.obj j)), coconeFun F j (x + y) = coconeFun F j x + coconeFun F j y
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
x✝ y✝ : ↑(F.obj j)
⊢ coconeFun F j (x✝ + y✝) = coconeFun F j x✝ + coconeFun F j y✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
⊢ ∀ (r : R) (x : ↑(F.obj j)),
    AddHom.toFun
        { toFun := coconeFun F j,
          map_add' :=
            (_ :
              ∀ (x y : ↑(F.obj j)),
                Quot.mk Setoid.r (Prequotient.of j (x + y)) =
                  Quot.mk Setoid.r (add (Prequotient.of j x) (Prequotient.of j y))) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := coconeFun F j,
            map_add' :=
              (_ :
                ∀ (x y : ↑(F.obj j)),
                  Quot.mk Setoid.r (Prequotient.of j (x + y)) =
                    Quot.mk Setoid.r (add (Prequotient.of j x) (Prequotient.of j y))) }
          x
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
r✝ : R
x✝ : ↑(F.obj j)
⊢ AddHom.toFun
      { toFun := coconeFun F j,
        map_add' :=
          (_ :
            ∀ (x y : ↑(F.obj j)),
              Quot.mk Setoid.r (Prequotient.of j (x + y)) =
                Quot.mk Setoid.r (add (Prequotient.of j x) (Prequotient.of j y))) }
      (r✝ • x✝) =
    ↑(RingHom.id R) r✝ •
      AddHom.toFun
        { toFun := coconeFun F j,
          map_add' :=
            (_ :
              ∀ (x y : ↑(F.obj j)),
                Quot.mk Setoid.r (Prequotient.of j (x + y)) =
                  Quot.mk Setoid.r (add (Prequotient.of j x) (Prequotient.of j y))) }
        x✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
r✝ : R
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j (r✝ • x✝)) (smul (↑(RingHom.id R) r✝) (Prequotient.of j x✝))
[PROOFSTEP]
apply Relation.smul
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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 h.a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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 ModuleCat.Colimits.Relation.map
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
⊢ ColimitType F → ↑s.pt
[PROOFSTEP]
fapply Quot.lift
[GOAL]
case f
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
⊢ Prequotient F → ↑s.pt
[PROOFSTEP]
exact descFunLift F s
[GOAL]
case a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction' r with h₁ r_x r_y r_h r_ih r_x r_y r_z r_h r_k r_ih_h r_ih_k r_j r_j' r_f r_x j j x j x y j s x u v r r_ih u
  v w r r_ih u v w r r_ih s u v r r_ih
[GOAL]
case a.refl
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y h₁ : Prequotient F
⊢ descFunLift F s h₁ = descFunLift F s h₁
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.refl
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y h₁ : Prequotient F
⊢ descFunLift F s h₁ = descFunLift F s h₁
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.symm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y : Prequotient F
r_h : Relation F r_x r_y
r_ih : descFunLift F s r_x = descFunLift F s r_y
⊢ descFunLift F s r_y = descFunLift F s r_x
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.symm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y : Prequotient F
r_h : Relation F r_x r_y
r_ih : descFunLift F s r_x = descFunLift F s r_y
⊢ descFunLift F s r_y = descFunLift F s r_x
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.trans
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y r_z : Prequotient F
r_h : Relation F r_x r_y
r_k : Relation F r_y r_z
r_ih_h : descFunLift F s r_x = descFunLift F s r_y
r_ih_k : descFunLift F s r_y = descFunLift F s r_z
⊢ descFunLift F s r_x = descFunLift F s r_z
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.trans
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y r_z : Prequotient F
r_h : Relation F r_x r_y
r_k : Relation F r_y r_z
r_ih_h : descFunLift F s r_x = descFunLift F s r_y
r_ih_k : descFunLift F s r_y = descFunLift F s r_z
⊢ descFunLift F s r_x = descFunLift F s r_z
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.map
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
r_j r_j' : J
r_f : r_j ⟶ r_j'
r_x : ↑(F.obj r_j)
⊢ descFunLift F s (Prequotient.of r_j' (↑(F.map r_f) r_x)) = descFunLift F s (Prequotient.of r_j r_x)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.map
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
r_j r_j' : J
r_f : r_j ⟶ r_j'
r_x : ↑(F.obj r_j)
⊢ descFunLift F s (Prequotient.of r_j' (↑(F.map r_f) r_x)) = descFunLift F s (Prequotient.of r_j r_x)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x✝ y : Prequotient F
j : J
s : R
x : ↑(F.obj j)
⊢ descFunLift F s✝ (Prequotient.of j (s • x)) = descFunLift F s✝ (smul s (Prequotient.of j x))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x✝ y : Prequotient F
j : J
s : R
x : ↑(F.obj j)
⊢ descFunLift F s✝ (Prequotient.of j (s • x)) = descFunLift F s✝ (smul s (Prequotient.of j x))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.neg_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s (neg u) = descFunLift F s (neg v)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.neg_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s (neg u) = descFunLift F s (neg v)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s (add u w) = descFunLift F s (add v w)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s (add u w) = descFunLift F s (add v w)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F v w
r_ih : descFunLift F s v = descFunLift F s w
⊢ descFunLift F s (add u v) = descFunLift F s (add u w)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F v w
r_ih : descFunLift F s v = descFunLift F s w
⊢ descFunLift F s (add u v) = descFunLift F s (add u w)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.smul_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x y : Prequotient F
s : R
u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s✝ u = descFunLift F s✝ v
⊢ descFunLift F s✝ (smul s u) = descFunLift F s✝ (smul s v)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.smul_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x y : Prequotient F
s : R
u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s✝ u = descFunLift F s✝ v
⊢ descFunLift F s✝ (smul s u) = descFunLift F s✝ (smul s v)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.zero_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add zero x✝) = descFunLift F s x✝
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.zero_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add zero x✝) = descFunLift F s x✝
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add x✝ zero) = descFunLift F s x✝
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add x✝ zero) = descFunLift F s x✝
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_left_neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add (neg x✝) x✝) = descFunLift F s zero
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_left_neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add (neg x✝) x✝) = descFunLift F s zero
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_comm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s (add x✝ y✝) = descFunLift F s (add y✝ x✝)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_comm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s (add x✝ y✝) = descFunLift F s (add y✝ x✝)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_assoc
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_assoc
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.one_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (smul 1 x✝) = descFunLift F s x✝
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.one_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (smul 1 x✝) = descFunLift F s x✝
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.mul_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ descFunLift F s (smul (s✝ * t✝) x✝) = descFunLift F s (smul s✝ (smul t✝ x✝))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.mul_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ descFunLift F s (smul (s✝ * t✝) x✝) = descFunLift F s (smul s✝ (smul t✝ x✝))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.smul_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
x✝ y✝ : Prequotient F
⊢ descFunLift F s (smul s✝ (add x✝ y✝)) = descFunLift F s (add (smul s✝ x✝) (smul s✝ y✝))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.smul_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
x✝ y✝ : Prequotient F
⊢ descFunLift F s (smul s✝ (add x✝ y✝)) = descFunLift F s (add (smul s✝ x✝) (smul s✝ y✝))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.smul_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
⊢ descFunLift F s (smul s✝ zero) = descFunLift F s zero
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.smul_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
⊢ descFunLift F s (smul s✝ zero) = descFunLift F s zero
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ descFunLift F s (smul (s✝ + t✝) x✝) = descFunLift F s (add (smul s✝ x✝) (smul t✝ x✝))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ descFunLift F s (smul (s✝ + t✝) x✝) = descFunLift F s (add (smul s✝ x✝) (smul t✝ x✝))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.zero_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (smul 0 x✝) = descFunLift F s zero
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.zero_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (smul 0 x✝) = descFunLift F s zero
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.symm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y : Prequotient F
r_h : Relation F r_x r_y
r_ih : descFunLift F s r_x = descFunLift F s r_y
⊢ descFunLift F s r_y = descFunLift F s r_x
[PROOFSTEP]
exact r_ih.symm
[GOAL]
case a.trans
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y r_z : Prequotient F
r_h : Relation F r_x r_y
r_k : Relation F r_y r_z
r_ih_h : descFunLift F s r_x = descFunLift F s r_y
r_ih_k : descFunLift F s r_y = descFunLift F s r_z
⊢ descFunLift F s r_x = descFunLift F s r_z
[PROOFSTEP]
exact Eq.trans r_ih_h r_ih_k
[GOAL]
case a.map
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
r_j r_j' : J
r_f : r_j ⟶ r_j'
r_x : ↑(F.obj r_j)
⊢ ↑(NatTrans.app s.ι r_j') (↑(F.map r_f) r_x) = ↑(NatTrans.app s.ι r_j) r_x
[PROOFSTEP]
exact s.w_apply r_f r_x
[GOAL]
case a.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
j : J
⊢ ↑(NatTrans.app s.ι j) 0 = 0
[PROOFSTEP]
simp
  -- neg
[GOAL]
case a.neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x✝ y : Prequotient F
j : J
x : ↑(F.obj j)
⊢ ↑(NatTrans.app s.ι j) (-x) = -↑(NatTrans.app s.ι j) x
[PROOFSTEP]
simp
  -- add
[GOAL]
case a.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ ↑(NatTrans.app s.ι j) (x + y) = ↑(NatTrans.app s.ι j) x + ↑(NatTrans.app s.ι j) y
[PROOFSTEP]
simp
  -- smul,
[GOAL]
case a.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x✝ y : Prequotient F
j : J
s : R
x : ↑(F.obj j)
⊢ ↑(NatTrans.app s✝.ι j) (s • x) = s • ↑(NatTrans.app s✝.ι j) x
[PROOFSTEP]
simp
  -- neg_1
[GOAL]
case a.neg_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ -descFunLift F s u = -descFunLift F s v
[PROOFSTEP]
rw [r_ih]
  -- add_1
[GOAL]
case a.add_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s u + descFunLift F s w = descFunLift F s v + descFunLift F s w
[PROOFSTEP]
rw [r_ih]
  -- add_2
[GOAL]
case a.add_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F v w
r_ih : descFunLift F s v = descFunLift F s w
⊢ descFunLift F s u + descFunLift F s v = descFunLift F s u + descFunLift F s w
[PROOFSTEP]
rw [r_ih]
  -- smul_1
[GOAL]
case a.smul_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x y : Prequotient F
s : R
u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s✝ u = descFunLift F s✝ v
⊢ s • descFunLift F s✝ u = s • descFunLift F s✝ v
[PROOFSTEP]
rw [r_ih]
  -- zero_add
[GOAL]
case a.zero_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ 0 + descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rw [zero_add]
  -- add_zero
[GOAL]
case a.add_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ + 0 = descFunLift F s x✝
[PROOFSTEP]
rw [add_zero]
  -- add_left_neg
[GOAL]
case a.add_left_neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ -descFunLift F s x✝ + descFunLift F s x✝ = 0
[PROOFSTEP]
rw [add_left_neg]
  -- add_comm
[GOAL]
case a.add_comm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
  -- add_assoc
[GOAL]
case a.add_assoc
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
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]
  -- one_smul
[GOAL]
case a.one_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ 1 • descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rw [one_smul]
  -- mul_smul
[GOAL]
case a.mul_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ (s✝ * t✝) • descFunLift F s x✝ = s✝ • t✝ • descFunLift F s x✝
[PROOFSTEP]
rw [mul_smul]
  -- smul_add
[GOAL]
case a.smul_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
x✝ y✝ : Prequotient F
⊢ s✝ • (descFunLift F s x✝ + descFunLift F s y✝) = s✝ • descFunLift F s x✝ + s✝ • descFunLift F s y✝
[PROOFSTEP]
rw [smul_add]
  -- smul_zero
[GOAL]
case a.smul_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
⊢ s✝ • 0 = 0
[PROOFSTEP]
rw [smul_zero]
  -- add_smul
[GOAL]
case a.add_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ (s✝ + t✝) • descFunLift F s x✝ = s✝ • descFunLift F s x✝ + t✝ • descFunLift F s x✝
[PROOFSTEP]
rw [add_smul]
  -- zero_smul
[GOAL]
case a.zero_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ 0 • descFunLift F s x✝ = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : ↑(colimit F)
⊢ descFun F s (x + y) = descFun F s x + descFun F s y
[PROOFSTEP]
rcases x
[GOAL]
case mk
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : ↑(colimit F)
a✝ : Prequotient F
⊢ descFun F s (Quot.mk Setoid.r a✝ + y) = descFun F s (Quot.mk Setoid.r a✝) + descFun F s y
[PROOFSTEP]
rcases y
[GOAL]
case mk.mk
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : ↑(colimit F)
a✝¹ a✝ : Prequotient F
⊢ descFun F s (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝) =
    descFun F s (Quot.mk Setoid.r a✝¹) + descFun F s (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
s : R
x : ↑(colimit F)
⊢ AddHom.toFun
      { toFun := descFun F s✝,
        map_add' := (_ : ∀ (x y : ↑(colimit F)), descFun F s✝ (x + y) = descFun F s✝ x + descFun F s✝ y) }
      (s • x) =
    ↑(RingHom.id R) s •
      AddHom.toFun
        { toFun := descFun F s✝,
          map_add' := (_ : ∀ (x y : ↑(colimit F)), descFun F s✝ (x + y) = descFun F s✝ x + descFun F s✝ y) }
        x
[PROOFSTEP]
rcases x
[GOAL]
case mk
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
s : R
x : ↑(colimit F)
a✝ : Prequotient F
⊢ AddHom.toFun
      { toFun := descFun F s✝,
        map_add' := (_ : ∀ (x y : ↑(colimit F)), descFun F s✝ (x + y) = descFun F s✝ x + descFun F s✝ y) }
      (s • Quot.mk Setoid.r a✝) =
    ↑(RingHom.id R) s •
      AddHom.toFun
        { toFun := descFun F s✝,
          map_add' := (_ : ∀ (x y : ↑(colimit F)), descFun F s✝ (x + y) = descFun F s✝ x + descFun F s✝ y) }
        (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => descMorphism F s) s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
⊢ ↑m x = ↑((fun s => descMorphism F s) s) x
[PROOFSTEP]
refine Quot.rec (motive := fun x ↦ m x = _) (fun x ↦ ?_) (fun x_a x_b x_p ↦ ?_) x
[GOAL]
case h.refine_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : ↑(colimitCocone F).pt
x : Prequotient F
⊢ (fun x => ↑m x = ↑((fun s => descMorphism F s) s) x) (Quot.mk Setoid.r x)
case h.refine_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_a x_b : Prequotient F
x_p : Setoid.r x_a x_b
⊢ (_ : ↑m (Quot.mk Setoid.r x_b) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x_b)) =
    (_ : (fun x => ↑m x = ↑((fun s => descMorphism F s) s) x) (Quot.mk Setoid.r x_b))
[PROOFSTEP]
dsimp
[GOAL]
case h.refine_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : ↑(colimitCocone F).pt
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
case h.refine_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_a x_b : Prequotient F
x_p : Setoid.r x_a x_b
⊢ (_ : ↑m (Quot.mk Setoid.r x_b) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x_b)) =
    (_ : (fun x => ↑m x = ↑((fun s => descMorphism F s) s) x) (Quot.mk Setoid.r x_b))
[PROOFSTEP]
induction' x with x_j x_x
[GOAL]
case h.refine_1.of
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_j : J
x_x : ↑(F.obj x_j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of x_j x_x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of x_j x_x))
[PROOFSTEP]
have w' := congr_fun (congr_arg (fun f : F.obj x_j ⟶ s.pt => (f : F.obj x_j → s.pt)) (w x_j)) x_x
[GOAL]
case h.refine_1.of
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_j : J
x_x : ↑(F.obj x_j)
w' : (fun f => ↑f) (NatTrans.app (colimitCocone F).ι x_j ≫ m) x_x = (fun f => ↑f) (NatTrans.app s.ι x_j) x_x
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of x_j x_x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of x_j x_x))
[PROOFSTEP]
simp only at w' 
[GOAL]
case h.refine_1.of
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_j : J
x_x : ↑(F.obj x_j)
w' : ↑(NatTrans.app (colimitCocone F).ι x_j ≫ m) x_x = ↑(NatTrans.app s.ι x_j) x_x
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of x_j x_x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of x_j x_x))
[PROOFSTEP]
erw [w']
[GOAL]
case h.refine_1.of
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_j : J
x_x : ↑(F.obj x_j)
w' : ↑(NatTrans.app (colimitCocone F).ι x_j ≫ m) x_x = ↑(NatTrans.app s.ι x_j) x_x
⊢ ↑(NatTrans.app s.ι x_j) x_x = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of x_j x_x))
[PROOFSTEP]
rfl
[GOAL]
case h.refine_1.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
⊢ ↑m (Quot.mk Setoid.r zero) = ↑(descMorphism F s) (Quot.mk Setoid.r zero)
[PROOFSTEP]
rw [quot_zero, map_zero]
  -- porting note: was `simp` but `map_zero` won't fire
[GOAL]
case h.refine_1.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
⊢ 0 = ↑(descMorphism F s) 0
[PROOFSTEP]
rfl
[GOAL]
case h.refine_1.neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝ : Prequotient F
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ ↑m (Quot.mk Setoid.r (neg a✝)) = ↑(descMorphism F s) (Quot.mk Setoid.r (neg a✝))
[PROOFSTEP]
simpa
[GOAL]
case h.refine_1.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝¹ a✝ : Prequotient F
a_ih✝¹ : ↑m (Quot.mk Setoid.r a✝¹) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝¹)
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ ↑m (Quot.mk Setoid.r (add a✝¹ a✝)) = ↑(descMorphism F s) (Quot.mk Setoid.r (add a✝¹ a✝))
[PROOFSTEP]
rw [quot_add, map_add, map_add]
  -- porting note: this was closed by `simp [*]`
[GOAL]
case h.refine_1.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝¹ a✝ : Prequotient F
a_ih✝¹ : ↑m (Quot.mk Setoid.r a✝¹) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝¹)
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ ↑m (ColimitType.mk a✝¹) + ↑m (ColimitType.mk a✝) =
    ↑(descMorphism F s) (ColimitType.mk a✝¹) + ↑(descMorphism F s) (ColimitType.mk a✝)
[PROOFSTEP]
congr 1
[GOAL]
case h.refine_1.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝¹ : R
a✝ : Prequotient F
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ ↑m (Quot.mk Setoid.r (smul a✝¹ a✝)) = ↑(descMorphism F s) (Quot.mk Setoid.r (smul a✝¹ a✝))
[PROOFSTEP]
rw [quot_smul, map_smul, map_smul]
  -- porting note: this was closed by `simp [*]`
[GOAL]
case h.refine_1.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝¹ : R
a✝ : Prequotient F
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ a✝¹ • ↑m (ColimitType.mk a✝) = a✝¹ • ↑(descMorphism F s) (ColimitType.mk a✝)
[PROOFSTEP]
congr 1
[GOAL]
case h.refine_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_a x_b : Prequotient F
x_p : Setoid.r x_a x_b
⊢ (_ : ↑m (Quot.mk Setoid.r x_b) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x_b)) =
    (_ : (fun x => ↑m x = ↑((fun s => descMorphism F s) s) x) (Quot.mk Setoid.r x_b))
[PROOFSTEP]
rfl
  -- porting note: this wasn't here
