[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget GroupCat) x y
⊢ colimitInvAux F x = colimitInvAux F y
[PROOFSTEP]
apply G.mk_eq
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget GroupCat) x y
⊢ ∃ k f g, ↑(F.map f) { fst := x.fst, snd := x.snd⁻¹ }.snd = ↑(F.map g) { fst := y.fst, snd := y.snd⁻¹ }.snd
[PROOFSTEP]
obtain ⟨k, f, g, hfg⟩ := h
[GOAL]
case h.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget GroupCat).map f x.snd = (F ⋙ forget GroupCat).map g y.snd
⊢ ∃ k f g, ↑(F.map f) { fst := x.fst, snd := x.snd⁻¹ }.snd = ↑(F.map g) { fst := y.fst, snd := y.snd⁻¹ }.snd
[PROOFSTEP]
use k, f, g
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget GroupCat).map f x.snd = (F ⋙ forget GroupCat).map g y.snd
⊢ ↑(F.map f) { fst := x.fst, snd := x.snd⁻¹ }.snd = ↑(F.map g) { fst := y.fst, snd := y.snd⁻¹ }.snd
[PROOFSTEP]
rw [MonoidHom.map_inv, MonoidHom.map_inv, inv_inj]
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget GroupCat).map f x.snd = (F ⋙ forget GroupCat).map g y.snd
⊢ ↑(F.map f) x.snd = ↑(F.map g) y.snd
[PROOFSTEP]
exact hfg
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x : ↑(G F)
⊢ ↑(G F)
[PROOFSTEP]
refine' Quot.lift (colimitInvAux.{v, u} F) _ x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x : ↑(G F)
⊢ ∀ (a b : (j : J) × ↑(F.obj j)),
    Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat) a b → colimitInvAux F a = colimitInvAux F b
[PROOFSTEP]
intro x y h
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat) x y
⊢ colimitInvAux F x = colimitInvAux F y
[PROOFSTEP]
apply colimitInvAux_eq_of_rel
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat) x y
⊢ Types.FilteredColimit.Rel (F ⋙ forget GroupCat) x y
[PROOFSTEP]
apply Types.FilteredColimit.rel_of_quot_rel
[GOAL]
case h.a
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat) x y
⊢ Types.Quot.Rel (F ⋙ forget GroupCat) x y
[PROOFSTEP]
exact h
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
x : ↑(G F)
⊢ x⁻¹ * x = 1
[PROOFSTEP]
refine Quot.inductionOn x ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
x : ↑(G F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) a)⁻¹ *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) a =
      1
[PROOFSTEP]
clear x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) a)⁻¹ *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) a =
      1
[PROOFSTEP]
intro x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
x : (j : J) × ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) x)⁻¹ *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) x =
    1
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
j : J
x : ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) { fst := j, snd := x })⁻¹ *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat)) { fst := j, snd := x } =
    1
[PROOFSTEP]
erw [colimit_inv_mk_eq, colimit_mul_mk_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j),
  colimit_one_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) j]
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
j : J
x : ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ GroupCat MonCat)
      { fst := j,
        snd :=
          ↑((F ⋙ forget₂ GroupCat MonCat).map (𝟙 j)) { fst := j, snd := { fst := j, snd := x }.snd⁻¹ }.snd *
            ↑((F ⋙ forget₂ GroupCat MonCat).map (𝟙 j)) { fst := j, snd := x }.snd } =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ GroupCat MonCat) { fst := j, snd := 1 }
[PROOFSTEP]
dsimp
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GroupCat
src✝¹ : Inv ↑(G F) := colimitInv F
src✝ : Monoid ↑(G F) := (G F).str
j : J
x : ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ GroupCat MonCat)
      { fst := j,
        snd := ↑((forget₂ GroupCat MonCat).map (F.map (𝟙 j))) x⁻¹ * ↑((forget₂ GroupCat MonCat).map (F.map (𝟙 j))) x } =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ GroupCat MonCat) { fst := j, snd := 1 }
[PROOFSTEP]
erw [CategoryTheory.Functor.map_id, mul_left_inv]
