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
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
apply G.mk_eq
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
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
obtain ⟨k, f, g, hfg⟩ := h
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
⊢ ↑(F.map f) { fst := x.fst, snd := x.snd⁻¹ }.snd = ↑(F.map g) { fst := y.fst, snd := y.snd⁻¹ }.snd
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
use k, f, g
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
⊢ ↑(F.map f) x.snd = ↑(F.map g) y.snd
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
⊢ ↑(F.map f) { fst := x.fst, snd := x.snd⁻¹ }.snd = ↑(F.map g) { fst := y.fst, snd := y.snd⁻¹ }.snd
rw [MonoidHom.map_inv, MonoidHom.map_inv, inv_inj]
no goals
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
⊢ ↑(F.map f) x.snd = ↑(F.map g) y.snd
exact hfg