∀ {X Y : FintypeCat} (f : X ⟶ Y),
  fintypeToFinBoolAlgOp.map f =
    (CategoryTheory.InducedCategory.homMk
        (BoolAlg.ofHom
          (have __src :=
            { toFun := ⇑(CompleteLatticeHom.setPreimage ⇑(CategoryTheory.ConcreteCategory.hom f)), map_sup' := ⋯,
              map_inf' := ⋯ };
          { toFun := ⇑(CompleteLatticeHom.setPreimage ⇑(CategoryTheory.ConcreteCategory.hom f)), map_sup' := ⋯,
            map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))).op