case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ∃ k f g, ↑(F.map f) { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.snd = ↑(F.map g) { fst := j, snd := 1 }.snd
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ 1 = M.mk F { fst := j, snd := 1 }
apply M.mk_eq
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ↑(F.map (IsFiltered.leftToMax { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.fst j))
      { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.snd =
    ↑(F.map (IsFiltered.rightToMax { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.fst j))
      { fst := j, snd := 1 }.snd
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ∃ k f g, ↑(F.map f) { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.snd = ↑(F.map g) { fst := j, snd := 1 }.snd
refine' ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, _⟩
no goals
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ↑(F.map (IsFiltered.leftToMax { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.fst j))
      { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.snd =
    ↑(F.map (IsFiltered.rightToMax { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.fst j))
      { fst := j, snd := 1 }.snd
simp