case refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) x { fst := k, snd := F.map f x.snd }

case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) { fst := k, snd := F.map f x.snd } y
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) x y
refine' EqvGen.trans _ ⟨k, F.map f x.2⟩ _ _ _
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) { fst := k, snd := F.map f x.snd } y
case refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) x { fst := k, snd := F.map f x.snd }

case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) { fst := k, snd := F.map f x.snd } y
. exact (EqvGen.rel _ _ ⟨f, rfl⟩)
no goals
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) { fst := k, snd := F.map f x.snd } y
. exact (EqvGen.symm _ _ (EqvGen.rel _ _ ⟨g, h⟩))
no goals
case refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) x { fst := k, snd := F.map f x.snd }
exact (EqvGen.rel _ _ ⟨f, rfl⟩)
no goals
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) { fst := k, snd := F.map f x.snd } y
exact (EqvGen.symm _ _ (EqvGen.rel _ _ ⟨g, h⟩))