[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
⊢ Inhabited (ColimitType F)
[PROOFSTEP]
dsimp [ColimitType]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
⊢ Inhabited (Quotient (colimitSetoid F))
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
⊢ Monoid (ColimitType F)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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 ⥤ MonCat
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 ⥤ MonCat
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 ⥤ MonCat
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 ⥤ MonCat
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 ⥤ MonCat
s : Cocone F
⊢ ColimitType F → ↑s.pt
[PROOFSTEP]
fapply Quot.lift
[GOAL]
case f
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
⊢ Prequotient F → ↑s.pt
[PROOFSTEP]
exact descFunLift F s
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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 ⥤ MonCat
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 _ _ _ _ _ h₁ h₂ _ _ f x _ _ _ _ _ _ _ _ h _ _ _ _ h
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
h : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
h : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
h₁ : descFunLift F s x✝² = descFunLift F s y✝
h₂ : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
h₁ : descFunLift F s x✝² = descFunLift F s y✝
h₂ : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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]
try
  simp
    -- symm
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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]
simp
  -- symm
[GOAL]
case a.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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]
try
  simp
    -- symm
[GOAL]
case a.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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
  -- symm
[GOAL]
case a.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
j✝ : J
⊢ descFunLift F s (Prequotient.of j✝ 1) = descFunLift F s one
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
j✝ : J
⊢ descFunLift F s (Prequotient.of j✝ 1) = descFunLift F s one
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
h : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (mul x✝¹ y✝) = descFunLift F s (mul x'✝ y✝)
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
h : descFunLift F s x✝¹ = descFunLift F s x'✝
⊢ descFunLift F s (mul x✝¹ y✝) = descFunLift F s (mul x'✝ y✝)
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
h : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s (mul x✝¹ y✝) = descFunLift F s (mul x✝¹ y'✝)
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
h : descFunLift F s y✝ = descFunLift F s y'✝
⊢ descFunLift F s (mul x✝¹ y✝) = descFunLift F s (mul x✝¹ y'✝)
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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]
try
  simp
    -- symm
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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]
simp
  -- symm
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (mul one x✝) = descFunLift F s x✝
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (mul one x✝) = descFunLift F s x✝
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (mul x✝ one) = descFunLift F s x✝
[PROOFSTEP]
try
  simp
    -- symm
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (mul x✝ one) = descFunLift F s x✝
[PROOFSTEP]
simp
  -- symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ : Prequotient F
x✝ : Relation F x✝¹ y✝
h : descFunLift F s x✝¹ = descFunLift F s y✝
⊢ descFunLift F s y✝ = descFunLift F s x✝¹
[PROOFSTEP]
exact h.symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝² y✝ z✝ : Prequotient F
x✝¹ : Relation F x✝² y✝
x✝ : Relation F y✝ z✝
h₁ : descFunLift F s x✝² = descFunLift F s y✝
h₂ : descFunLift F s y✝ = descFunLift F s z✝
⊢ descFunLift F s x✝² = descFunLift F s z✝
[PROOFSTEP]
exact h₁.trans h₂
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x✝ y : Prequotient F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : ↑(F.obj j✝)
⊢ ↑(NatTrans.app s.ι j'✝) (↑(F.map f) x) = ↑(NatTrans.app s.ι j✝) x
[PROOFSTEP]
exact s.w_apply f x
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ x'✝ y✝ : Prequotient F
x✝ : Relation F x✝¹ x'✝
h : 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 [h]
  -- mul_2
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
x y x✝¹ y✝ y'✝ : Prequotient F
x✝ : Relation F y✝ y'✝
h : 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 [h]
  -- mul_assoc
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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]
induction x using Quot.inductionOn
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
y : ↑(colimit F)
a✝ : Prequotient F
⊢ OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (Quot.mk Setoid.r a✝ * y) =
    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (Quot.mk Setoid.r a✝) *
      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y
[PROOFSTEP]
induction y using Quot.inductionOn
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
a✝¹ a✝ : Prequotient F
⊢ OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) }
      (Quot.mk Setoid.r a✝¹ * Quot.mk Setoid.r a✝) =
    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (Quot.mk Setoid.r a✝¹) *
      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (Quot.mk Setoid.r a✝)
[PROOFSTEP]
dsimp [descFun]
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
a✝¹ a✝ : 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 a✝¹ * Quot.mk Setoid.r a✝) =
    descFunLift F s a✝¹ * descFunLift F s a✝
[PROOFSTEP]
rw [← quot_mul]
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
a✝¹ a✝ : 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 (mul a✝¹ a✝)) =
    descFunLift F s a✝¹ * descFunLift F s a✝
[PROOFSTEP]
simp only [descFunLift]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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 w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
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]
induction' x using Quot.inductionOn with x
[GOAL]
case w.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
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 j x x y hx hy
[GOAL]
case w.h.of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
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]
change _ = s.ι.app j _
[GOAL]
case w.h.of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
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)) = ↑(NatTrans.app s.ι j) x
[PROOFSTEP]
rw [← w j]
[GOAL]
case w.h.of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
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)) = ↑(NatTrans.app (colimitCocone F).ι j ≫ m) x
[PROOFSTEP]
rfl
[GOAL]
case w.h.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
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]
rw [quot_one, map_one]
[GOAL]
case w.h.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ 1 = ↑((fun s => descMorphism F s) s) 1
[PROOFSTEP]
rfl
[GOAL]
case w.h.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
hx : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
hy : ↑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]
rw [quot_mul, map_mul, hx, hy]
[GOAL]
case w.h.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
hx : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
hy : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x) * ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y) =
    ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x * Quot.mk Setoid.r y)
[PROOFSTEP]
dsimp [descMorphism, FunLike.coe, descFun]
[GOAL]
case w.h.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
hx : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
hy : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ descFunLift F s x * descFunLift F s y =
    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 x * Quot.mk Setoid.r y)
[PROOFSTEP]
simp only [← quot_mul, descFunLift]
