[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk Setoid.r x * (Quot.mk Setoid.r y + Quot.mk Setoid.r z) =
    Quot.mk Setoid.r x * Quot.mk Setoid.r y + Quot.mk Setoid.r x * Quot.mk Setoid.r z
[PROOFSTEP]
simp only [(· + ·), (· * ·), Add.add]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
      (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
      (Quotient.map₂ add (_ : ∀ (x x' : Prequotient F), x ≈ x' → ∀ (y y' : Prequotient F), y ≈ y' → add x y ≈ add x' y')
        (Quot.mk Setoid.r y) (Quot.mk Setoid.r z)) =
    Quotient.map₂ add (_ : ∀ (x x' : Prequotient F), x ≈ x' → ∀ (y y' : Prequotient F), y ≈ y' → add x y ≈ add x' y')
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
        (Quot.mk Setoid.r y))
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
        (Quot.mk Setoid.r z))
[PROOFSTEP]
exact Quot.sound (Relation.left_distrib _ _ _)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ (Quot.mk Setoid.r x + Quot.mk Setoid.r y) * Quot.mk Setoid.r z =
    Quot.mk Setoid.r x * Quot.mk Setoid.r z + Quot.mk Setoid.r y * Quot.mk Setoid.r z
[PROOFSTEP]
simp only [(· + ·), (· * ·), Add.add]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
      (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y))
      (Quotient.map₂ add (_ : ∀ (x x' : Prequotient F), x ≈ x' → ∀ (y y' : Prequotient F), y ≈ y' → add x y ≈ add x' y')
        (Quot.mk Setoid.r x) (Quot.mk Setoid.r y))
      (Quot.mk Setoid.r z) =
    Quotient.map₂ add (_ : ∀ (x x' : Prequotient F), x ≈ x' → ∀ (y y' : Prequotient F), y ≈ y' → add x y ≈ add x' y')
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
        (Quot.mk Setoid.r z))
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r y)
        (Quot.mk Setoid.r z))
[PROOFSTEP]
exact Quot.sound (Relation.right_distrib _ _ _)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk Setoid.r x * Quot.mk Setoid.r y * Quot.mk Setoid.r z =
    Quot.mk Setoid.r x * (Quot.mk Setoid.r y * Quot.mk Setoid.r z)
[PROOFSTEP]
simp only [(· * ·)]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
      (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y))
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
        (Quot.mk Setoid.r y))
      (Quot.mk Setoid.r z) =
    Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
      (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r y)
        (Quot.mk Setoid.r z))
[PROOFSTEP]
exact Quot.sound (Relation.mul_assoc _ _ _)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ coconeFun F j 1 = 1
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ Setoid.r (Prequotient.of j 1) one
[PROOFSTEP]
apply Relation.one
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ ∀ (x y : ↑(F.obj j)),
    OneHom.toFun
        { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) }
        (x * y) =
      OneHom.toFun
          { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) } x *
        OneHom.toFun
          { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) } y
[PROOFSTEP]
intros
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ OneHom.toFun
      { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) } x✝ *
      OneHom.toFun
        { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) } y✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j (x✝ * y✝)) (mul (Prequotient.of j x✝) (Prequotient.of j y✝))
[PROOFSTEP]
apply Relation.mul
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑(F.obj j)),
                Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                  Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
      0 =
    0
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ Setoid.r (Prequotient.of j 0) zero
[PROOFSTEP]
apply Relation.zero
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ ∀ (x y : ↑(F.obj j)),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := coconeFun F j,
                map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(F.obj j)),
                  Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                    Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := coconeFun F j,
                  map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑(F.obj j)),
                    Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                      Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := coconeFun F j,
                  map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑(F.obj j)),
                    Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                      Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
          y
[PROOFSTEP]
intros
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑(F.obj j)),
                Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                  Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
      (x✝ + y✝) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := coconeFun F j,
                map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(F.obj j)),
                  Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                    Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
        x✝ +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := coconeFun F j,
                map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(F.obj j)),
                  Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                    Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
        y✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : (forget CommRingCat).obj (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 ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : (forget CommRingCat).obj (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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
s : Cocone F
⊢ ColimitType F → ↑s.pt
[PROOFSTEP]
fapply Quot.lift
[GOAL]
case f
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ Prequotient F → ↑s.pt
[PROOFSTEP]
exact descFunLift F s
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
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 x y _ ih => exact ih.symm
| trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
| map j j' f x => exact RingHom.congr_fun (s.ι.naturality f) x
| zero j => simp
| one j => simp
| neg j x => simp
| add j x y => simp
| mul j x y => simp
| neg_1 x x' r ih => dsimp; rw [ih]
| add_1 x x' y r ih => dsimp; rw [ih]
| add_2 x y y' r ih => dsimp; rw [ih]
| mul_1 x x' y r ih => dsimp; rw [ih]
| mul_2 x y y' r ih => dsimp; rw [ih]
| zero_add x => dsimp; rw [zero_add]
| add_zero x => dsimp; rw [add_zero]
| one_mul x => dsimp; rw [one_mul]
| mul_one x => dsimp; rw [mul_one]
| add_left_neg x => dsimp; rw [add_left_neg]
| add_comm x y => dsimp; rw [add_comm]
| mul_comm x y => dsimp; rw [mul_comm]
| add_assoc x y z => dsimp; rw [add_assoc]
| mul_assoc x y z => dsimp; rw [mul_assoc]
| left_distrib x y z => dsimp; rw [mul_add]
| right_distrib x y z => dsimp; rw [add_mul]
| zero_mul x => dsimp; rw [zero_mul]
| mul_zero x => dsimp; rw [mul_zero]
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 x y _ ih => exact ih.symm
| trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
| map j j' f x => exact RingHom.congr_fun (s.ι.naturality f) x
| zero j => simp
| one j => simp
| neg j x => simp
| add j x y => simp
| mul j x y => simp
| neg_1 x x' r ih => dsimp; rw [ih]
| add_1 x x' y r ih => dsimp; rw [ih]
| add_2 x y y' r ih => dsimp; rw [ih]
| mul_1 x x' y r ih => dsimp; rw [ih]
| mul_2 x y y' r ih => dsimp; rw [ih]
| zero_add x => dsimp; rw [zero_add]
| add_zero x => dsimp; rw [add_zero]
| one_mul x => dsimp; rw [one_mul]
| mul_one x => dsimp; rw [mul_one]
| add_left_neg x => dsimp; rw [add_left_neg]
| add_comm x y => dsimp; rw [add_comm]
| mul_comm x y => dsimp; rw [mul_comm]
| add_assoc x y z => dsimp; rw [add_assoc]
| mul_assoc x y z => dsimp; rw [mul_assoc]
| left_distrib x y z => dsimp; rw [mul_add]
| right_distrib x y z => dsimp; rw [add_mul]
| zero_mul x => dsimp; rw [zero_mul]
| mul_zero x => dsimp; rw [mul_zero]
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
s : Cocone F
x✝¹ y✝ x y : Prequotient F
x✝ : Relation F x y
ih : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x
[PROOFSTEP]

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

| trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝² y✝ x y z : Prequotient F
x✝¹ : Relation F x y
x✝ : Relation F y z
ih1 : descFunLift F s x = descFunLift F s y
ih2 : descFunLift F s y = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s z
[PROOFSTEP]
exact ih1.trans ih2
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 => exact RingHom.congr_fun (s.ι.naturality f) x
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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]
exact RingHom.congr_fun (s.ι.naturality f) x
[GOAL]
case a.zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
[PROOFSTEP]

| zero j => simp
[GOAL]
case a.zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 1) = descFunLift F s one
[PROOFSTEP]

| one j => simp
[GOAL]
case a.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 1) = descFunLift F s one
[PROOFSTEP]
simp
[GOAL]
case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 j x => simp
[GOAL]
case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
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 j x y => simp
[GOAL]
case a.add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 (mul (Prequotient.of j x) (Prequotient.of j y))
[PROOFSTEP]

| mul j x y => simp
[GOAL]
case a.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 (mul (Prequotient.of j x) (Prequotient.of j y))
[PROOFSTEP]
simp
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (neg x) = descFunLift F s (neg x')
[PROOFSTEP]

| neg_1 x x' r ih => dsimp; rw [ih]
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
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 ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ -descFunLift F s x = -descFunLift F s x'
[PROOFSTEP]
rw [ih]
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (add x y) = descFunLift F s (add x' y)
[PROOFSTEP]

| add_1 x x' y r ih => dsimp; rw [ih]
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
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 ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
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 [ih]
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (add x y) = descFunLift F s (add x y')
[PROOFSTEP]

| add_2 x y y' r ih => dsimp; rw [ih]
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
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 ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
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 [ih]
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (mul x y) = descFunLift F s (mul x' y)
[PROOFSTEP]

| mul_1 x x' y r ih => dsimp; rw [ih]
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (mul x y) = descFunLift F s (mul x' y)
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
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 [ih]
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (mul x y) = descFunLift F s (mul x y')
[PROOFSTEP]

| mul_2 x y y' r ih => dsimp; rw [ih]
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (mul x y) = descFunLift F s (mul x y')
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
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 [ih]
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add zero x) = descFunLift F s x
[PROOFSTEP]

| zero_add x => dsimp; rw [zero_add]
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add x zero) = descFunLift F s x
[PROOFSTEP]

| add_zero x => dsimp; rw [add_zero]
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x + 0 = descFunLift F s x
[PROOFSTEP]
rw [add_zero]
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul one x) = descFunLift F s x
[PROOFSTEP]

| one_mul x => dsimp; rw [one_mul]
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul one x) = descFunLift F s x
[PROOFSTEP]
dsimp
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 1 * descFunLift F s x = descFunLift F s x
[PROOFSTEP]
rw [one_mul]
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul x one) = descFunLift F s x
[PROOFSTEP]

| mul_one x => dsimp; rw [mul_one]
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul x one) = descFunLift F s x
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x * 1 = descFunLift F s x
[PROOFSTEP]
rw [mul_one]
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add (neg x) x) = descFunLift F s zero
[PROOFSTEP]

| add_left_neg x => dsimp; rw [add_left_neg]
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s (add x y) = descFunLift F s (add y x)
[PROOFSTEP]

| add_comm x y => dsimp; rw [add_comm]
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
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.mul_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s (mul x y) = descFunLift F s (mul y x)
[PROOFSTEP]

| mul_comm x y => dsimp; rw [mul_comm]
[GOAL]
case a.mul_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s (mul x y) = descFunLift F s (mul y x)
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 [mul_comm]
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 x y z => dsimp; rw [add_assoc]
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 ⥤ CommRingCat
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]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul (mul x y) z) = descFunLift F s (mul x (mul y z))
[PROOFSTEP]

| mul_assoc x y z => dsimp; rw [mul_assoc]
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul (mul x y) z) = descFunLift F s (mul x (mul y z))
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 [mul_assoc]
[GOAL]
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul x (add y z)) = descFunLift F s (add (mul x y) (mul x z))
[PROOFSTEP]

| left_distrib x y z => dsimp; rw [mul_add]
[GOAL]
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul x (add y z)) = descFunLift F s (add (mul x y) (mul x z))
[PROOFSTEP]
dsimp
[GOAL]
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 x * descFunLift F s z
[PROOFSTEP]
rw [mul_add]
[GOAL]
case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul (add x y) z) = descFunLift F s (add (mul x z) (mul y z))
[PROOFSTEP]

| right_distrib x y z => dsimp; rw [add_mul]
[GOAL]
case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul (add x y) z) = descFunLift F s (add (mul x z) (mul y z))
[PROOFSTEP]
dsimp
[GOAL]
case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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 z + descFunLift F s y * descFunLift F s z
[PROOFSTEP]
rw [add_mul]
[GOAL]
case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul zero x) = descFunLift F s zero
[PROOFSTEP]

| zero_mul x => dsimp; rw [zero_mul]
[GOAL]
case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul zero x) = descFunLift F s zero
[PROOFSTEP]
dsimp
[GOAL]
case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 * descFunLift F s x = 0
[PROOFSTEP]
rw [zero_mul]
[GOAL]
case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul x zero) = descFunLift F s zero
[PROOFSTEP]

| mul_zero x => dsimp; rw [mul_zero]
[GOAL]
case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul x zero) = descFunLift F s zero
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x * 0 = 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
⊢ OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y
[PROOFSTEP]
exact Quot.induction_on₂ x y fun a b => rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑(colimit F)),
                OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
      (x + y) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(colimit F)),
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
        x +
      OneHom.toFun
        (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(colimit F)),
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
        y
[PROOFSTEP]
refine Quot.induction_on₂ x y fun a b => ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
a b : Prequotient F
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑(colimit F)),
                OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
      (Quot.mk Setoid.r a + Quot.mk Setoid.r b) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(colimit F)),
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
        (Quot.mk Setoid.r a) +
      OneHom.toFun
        (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(colimit F)),
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
        (Quot.mk Setoid.r b)
[PROOFSTEP]
dsimp [descFun, (· + ·)]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
a b : Prequotient F
⊢ Quot.lift (descFunLift F s) (_ : ∀ (x y : Prequotient F), Setoid.r x y → descFunLift F s x = descFunLift F s y)
      (Add.add (Quot.mk Setoid.r a) (Quot.mk Setoid.r b)) =
    Add.add (descFunLift F s a) (descFunLift F s b)
[PROOFSTEP]
rw [← quot_add]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
a b : Prequotient F
⊢ Quot.lift (descFunLift F s) (_ : ∀ (x y : Prequotient F), Setoid.r x y → descFunLift F s x = descFunLift F s y)
      (Quot.mk Setoid.r (add a b)) =
    Add.add (descFunLift F s a) (descFunLift F s b)
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
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]
change (colimitCocone F).pt →+* s.pt at m 
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m x = ↑((fun s => descMorphism F s) s) x
[PROOFSTEP]
refine Quot.inductionOn x ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (a : Prequotient F), ↑m (Quot.mk Setoid.r a) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r a)
[PROOFSTEP]
intro x
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction x with
| zero => erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero]
| one => erw [quot_one, map_one (f := m), (descMorphism F s).map_one]
| neg x ih => erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]
| of j x => exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
| add x y ih_x ih_y => erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]
| mul x y ih_x ih_y => erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction x with
| zero => erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero]
| one => erw [quot_one, map_one (f := m), (descMorphism F s).map_one]
| neg x ih => erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]
| of j x => exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
| add x y ih_x ih_y => erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]
| mul x y ih_x ih_y => erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r zero) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r zero)
[PROOFSTEP]

| zero => erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero]
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r zero) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r zero)
[PROOFSTEP]
erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero]
[GOAL]
case one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r one) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r one)
[PROOFSTEP]

| one => erw [quot_one, map_one (f := m), (descMorphism F s).map_one]
[GOAL]
case one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r one) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r one)
[PROOFSTEP]
erw [quot_one, map_one (f := m), (descMorphism F s).map_one]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
⊢ ↑m (Quot.mk Setoid.r (neg x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (neg x))
[PROOFSTEP]

| neg x ih => erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
⊢ ↑m (Quot.mk Setoid.r (neg x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (neg x))
[PROOFSTEP]
erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]
[GOAL]
case of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]

| of j x => exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
[GOAL]
case of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]
exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
ih_x : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
ih_y : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (add x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (add x y))
[PROOFSTEP]

| add x y ih_x ih_y => erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
ih_x : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
ih_y : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (add x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (add x y))
[PROOFSTEP]
erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]
[GOAL]
case mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
ih_x : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
ih_y : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (mul x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (mul x y))
[PROOFSTEP]

| mul x y ih_x ih_y => erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]
[GOAL]
case mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
ih_x : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
ih_y : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (mul x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (mul x y))
[PROOFSTEP]
erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]
