case h.mk.h.mk.a
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y } ↔
    EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y }
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
⊢ FilteredColimit.Rel F = EqvGen (Quot.Rel F)
ext ⟨j, x⟩ ⟨j', y⟩
case h.mk.h.mk.a.mp
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y } →
    EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y }

case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y } →
    FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y }
case h.mk.h.mk.a
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y } ↔
    EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y }
constructor
no goals
case h.mk.h.mk.a.mp
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y } →
    EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y }
apply eqvGen_quot_rel_of_rel
case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y } →
    EqvGen (FilteredColimit.Rel F) { fst := j, snd := x } { fst := j', snd := y }
case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y } →
    FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y }
rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
no goals
case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y } →
    EqvGen (FilteredColimit.Rel F) { fst := j, snd := x } { fst := j', snd := y }
exact EqvGen.mono (rel_of_quot_rel F)