[GOAL]
X Y : FinBoolAlgCat
f g : X ⟶ Y
h : (forget₂ FinBoolAlgCat FinPartOrd).map f = (forget₂ FinBoolAlgCat FinPartOrd).map g
⊢ f = g
[PROOFSTEP]
dsimp at *
[GOAL]
X Y : FinBoolAlgCat
f g : X ⟶ Y
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
apply FunLike.coe_injective
[GOAL]
case a
X Y : FinBoolAlgCat
f g : X ⟶ Y
h : ↑f = ↑g
⊢ (fun f => ↑f) f = (fun f => ↑f) g
[PROOFSTEP]
dsimp
[GOAL]
case a
X Y : FinBoolAlgCat
f g : X ⟶ Y
h : ↑f = ↑g
⊢ ↑f = ↑g
[PROOFSTEP]
ext x
[GOAL]
case a.h
X Y : FinBoolAlgCat
f g : X ⟶ Y
h : ↑f = ↑g
x : ↑X.toBoolAlgCat
⊢ ↑f x = ↑g x
[PROOFSTEP]
apply_fun (fun f => f x) at h
[GOAL]
case a.h
X Y : FinBoolAlgCat
f g : X ⟶ Y
x : ↑X.toBoolAlgCat
h : ↑↑f x = ↑↑g x
⊢ ↑f x = ↑g x
[PROOFSTEP]
exact h
[GOAL]
α β : FinBoolAlgCat
e : ↑α.toBoolAlgCat ≃o ↑β.toBoolAlgCat
⊢ ((let src :=
        { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α.toBoolAlgCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α.toBoolAlgCat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) ≫
      let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ :
                  ∀ (a b : ↑β.toBoolAlgCat),
                    ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' :=
            (_ : ∀ (a b : ↑β.toBoolAlgCat), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β.toBoolAlgCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β.toBoolAlgCat),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β.toBoolAlgCat),
                                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBoolAlgCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toBoolAlgCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBoolAlgCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toBoolAlgCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β.toBoolAlgCat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : FinBoolAlgCat
e : ↑α.toBoolAlgCat ≃o ↑β.toBoolAlgCat
x✝ : (forget FinBoolAlgCat).obj α
⊢ ↑((let src :=
            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α.toBoolAlgCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑e,
                                      map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α.toBoolAlgCat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) ≫
          let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ :
                      ∀ (a b : ↑β.toBoolAlgCat),
                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ :
                  ∀ (a b : ↑β.toBoolAlgCat),
                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β.toBoolAlgCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β.toBoolAlgCat),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β.toBoolAlgCat),
                                        ↑(OrderIso.symm e) (a ⊓ b) =
                                          ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toBoolAlgCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBoolAlgCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toBoolAlgCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBoolAlgCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β.toBoolAlgCat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : FinBoolAlgCat
e : ↑α.toBoolAlgCat ≃o ↑β.toBoolAlgCat
⊢ ((let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ :
                  ∀ (a b : ↑β.toBoolAlgCat),
                    ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' :=
            (_ : ∀ (a b : ↑β.toBoolAlgCat), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β.toBoolAlgCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β.toBoolAlgCat),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β.toBoolAlgCat),
                                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBoolAlgCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toBoolAlgCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBoolAlgCat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toBoolAlgCat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β.toBoolAlgCat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) ≫
      let src :=
        { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α.toBoolAlgCat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e,
                                    map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α.toBoolAlgCat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : FinBoolAlgCat
e : ↑α.toBoolAlgCat ≃o ↑β.toBoolAlgCat
x✝ : (forget FinBoolAlgCat).obj β
⊢ ↑((let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ :
                      ∀ (a b : ↑β.toBoolAlgCat),
                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ :
                  ∀ (a b : ↑β.toBoolAlgCat),
                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β.toBoolAlgCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β.toBoolAlgCat),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β.toBoolAlgCat),
                                        ↑(OrderIso.symm e) (a ⊓ b) =
                                          ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toBoolAlgCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBoolAlgCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toBoolAlgCat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toBoolAlgCat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β.toBoolAlgCat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) ≫
          let src :=
            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α.toBoolAlgCat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑e,
                                      map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e,
                                        map_sup' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toBoolAlgCat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α.toBoolAlgCat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
⊢ ConcreteCategory CompleteLatCat
[PROOFSTEP]
dsimp [CompleteLatCat]
[GOAL]
⊢ ConcreteCategory (Bundled CompleteLattice)
[PROOFSTEP]
infer_instance
[GOAL]
α β : CompleteLatCat
e : ↑α ≃o ↑β
⊢ { tosInfHom := { toFun := ↑e, map_sInf' := (_ : ∀ (s : Set ↑α), ↑e (sInf s) = sInf (↑e '' s)) },
        map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } ≫
      {
        tosInfHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sInf' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sInf s) = sInf (↑(OrderIso.symm e) '' s)) },
        map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : CompleteLatCat
e : ↑α ≃o ↑β
x✝ : (forget CompleteLatCat).obj α
⊢ ↑({ tosInfHom := { toFun := ↑e, map_sInf' := (_ : ∀ (s : Set ↑α), ↑e (sInf s) = sInf (↑e '' s)) },
            map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } ≫
          {
            tosInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sInf' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sInf s) = sInf (↑(OrderIso.symm e) '' s)) },
            map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : CompleteLatCat
e : ↑α ≃o ↑β
⊢ {
        tosInfHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sInf' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sInf s) = sInf (↑(OrderIso.symm e) '' s)) },
        map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } ≫
      { tosInfHom := { toFun := ↑e, map_sInf' := (_ : ∀ (s : Set ↑α), ↑e (sInf s) = sInf (↑e '' s)) },
        map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : CompleteLatCat
e : ↑α ≃o ↑β
x✝ : (forget CompleteLatCat).obj β
⊢ ↑({
            tosInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sInf' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sInf s) = sInf (↑(OrderIso.symm e) '' s)) },
            map_sSup' := (_ : ∀ (s : Set ↑β), ↑(OrderIso.symm e) (sSup s) = sSup (↑(OrderIso.symm e) '' s)) } ≫
          { tosInfHom := { toFun := ↑e, map_sInf' := (_ : ∀ (s : Set ↑α), ↑e (sInf s) = sInf (↑e '' s)) },
            map_sSup' := (_ : ∀ (s : Set ↑α), ↑e (sSup s) = sSup (↑e '' s)) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
α β : BddLatCat
e : ↑α.toLat ≃o ↑β.toLat
⊢ ((let src :=
        { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α.toLat),
                      SupHom.toFun
                          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α.toLat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) ≫
      let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ : ∀ (a b : ↑β.toLat), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' :=
            (_ : ∀ (a b : ↑β.toLat), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β.toLat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β.toLat),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β.toLat),
                                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toLat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toLat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toLat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toLat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β.toLat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : BddLatCat
e : ↑α.toLat ≃o ↑β.toLat
x✝ : (forget BddLatCat).obj α
⊢ ↑((let src :=
            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α.toLat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α.toLat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) ≫
          let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ :
                      ∀ (a b : ↑β.toLat), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ : ∀ (a b : ↑β.toLat), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β.toLat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β.toLat),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β.toLat),
                                        ↑(OrderIso.symm e) (a ⊓ b) =
                                          ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toLat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toLat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toLat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toLat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β.toLat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : BddLatCat
e : ↑α.toLat ≃o ↑β.toLat
⊢ ((let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ : ∀ (a b : ↑β.toLat), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' :=
            (_ : ∀ (a b : ↑β.toLat), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β.toLat),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β.toLat),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β.toLat),
                                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toLat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toLat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β.toLat),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β.toLat),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β.toLat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) ≫
      let src :=
        { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α.toLat),
                      SupHom.toFun
                          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α.toLat),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : BddLatCat
e : ↑α.toLat ≃o ↑β.toLat
x✝ : (forget BddLatCat).obj β
⊢ ↑((let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ :
                      ∀ (a b : ↑β.toLat), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ : ∀ (a b : ↑β.toLat), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β.toLat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β.toLat),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β.toLat),
                                        ↑(OrderIso.symm e) (a ⊓ b) =
                                          ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toLat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toLat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β.toLat),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β.toLat),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β.toLat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) ≫
          let src :=
            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α.toLat),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α.toLat), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α.toLat),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
[GOAL]
X : LatCat
Y : BddLatCat
f : latToBddLatCat.obj X ⟶ Y
a b : ↑X
⊢ (some ∘ some) (a ⊔ b) = (some ∘ some) a ⊔ (some ∘ some) b
[PROOFSTEP]
rfl
[GOAL]
X : LatCat
Y : BddLatCat
f : latToBddLatCat.obj X ⟶ Y
a b : ↑X
⊢ (some ∘ some) (a ⊓ b) = (some ∘ some) a ⊓ (some ∘ some) b
[PROOFSTEP]
rfl


[GOAL]
α β : SemilatSupCat
e : α.X ≃o β.X
⊢ { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : α.X), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
        map_bot' := (_ : ↑e ⊥ = ⊥) } ≫
      {
        toSupHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sup' := (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
        map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : SemilatSupCat
e : α.X ≃o β.X
x✝ : (forget SemilatSupCat).obj α
⊢ ↑({ toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : α.X), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_bot' := (_ : ↑e ⊥ = ⊥) } ≫
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : SemilatSupCat
e : α.X ≃o β.X
⊢ {
        toSupHom :=
          { toFun := ↑(OrderIso.symm e),
            map_sup' := (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
        map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) } ≫
      { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : α.X), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
        map_bot' := (_ : ↑e ⊥ = ⊥) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : SemilatSupCat
e : α.X ≃o β.X
x✝ : (forget SemilatSupCat).obj β
⊢ ↑({
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
            map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) } ≫
          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : α.X), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
            map_bot' := (_ : ↑e ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
[GOAL]
α β : SemilatInfCat
e : α.X ≃o β.X
⊢ { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : α.X), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
        map_top' := (_ : ↑e ⊤ = ⊤) } ≫
      {
        toInfHom :=
          { toFun := ↑(OrderIso.symm e),
            map_inf' := (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : SemilatInfCat
e : α.X ≃o β.X
x✝ : (forget SemilatInfCat).obj α
⊢ ↑({ toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : α.X), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_top' := (_ : ↑e ⊤ = ⊤) } ≫
          {
            toInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_inf' :=
                  (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : SemilatInfCat
e : α.X ≃o β.X
⊢ {
        toInfHom :=
          { toFun := ↑(OrderIso.symm e),
            map_inf' := (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) } ≫
      { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : α.X), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
        map_top' := (_ : ↑e ⊤ = ⊤) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : SemilatInfCat
e : α.X ≃o β.X
x✝ : (forget SemilatInfCat).obj β
⊢ ↑({
            toInfHom :=
              { toFun := ↑(OrderIso.symm e),
                map_inf' :=
                  (_ : ∀ (a b : β.X), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤) } ≫
          { toInfHom := { toFun := ↑e, map_inf' := (_ : ∀ (a b : α.X), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) },
            map_top' := (_ : ↑e ⊤ = ⊤) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
α β : LinOrdCat
e : ↑α ≃o ↑β
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext x
[GOAL]
case w
α β : LinOrdCat
e : ↑α ≃o ↑β
x : (forget LinOrdCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x = ↑(𝟙 α) x
[PROOFSTEP]
exact e.symm_apply_apply x
[GOAL]
α β : LinOrdCat
e : ↑α ≃o ↑β
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext x
[GOAL]
case w
α β : LinOrdCat
e : ↑α ≃o ↑β
x : (forget LinOrdCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x = ↑(𝟙 β) x
[PROOFSTEP]
exact e.apply_symm_apply x


[GOAL]
α β : PartOrdCat
e : ↑α ≃o ↑β
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext x
[GOAL]
case w
α β : PartOrdCat
e : ↑α ≃o ↑β
x : (forget PartOrdCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x = ↑(𝟙 α) x
[PROOFSTEP]
exact e.symm_apply_apply x
[GOAL]
α β : PartOrdCat
e : ↑α ≃o ↑β
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext x
[GOAL]
case w
α β : PartOrdCat
e : ↑α ≃o ↑β
x : (forget PartOrdCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x = ↑(𝟙 β) x
[PROOFSTEP]
exact e.apply_symm_apply x
[GOAL]
X : PreordCat
⊢ { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
          map := fun {X Y} f => OrderHom.antisymmetrization f }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
            map := fun {X Y} f => OrderHom.antisymmetrization f }.obj
        X)
[PROOFSTEP]
ext x
[GOAL]
case w
X : PreordCat
x :
  (forget PartOrdCat).obj
    ({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
          map := fun {X Y} f => OrderHom.antisymmetrization f }.obj
      X)
⊢ ↑({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
              map := fun {X Y} f => OrderHom.antisymmetrization f }.map
          (𝟙 X))
      x =
    ↑(𝟙
          ({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
                map := fun {X Y} f => OrderHom.antisymmetrization f }.obj
            X))
      x
[PROOFSTEP]
exact Quotient.inductionOn' x fun x => Quotient.map'_mk'' _ (fun a b => id) _
[GOAL]
X✝ Y✝ Z✝ : PreordCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
          map := fun {X Y} f => OrderHom.antisymmetrization f }.map
      (f ≫ g) =
    { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
            map := fun {X Y} f => OrderHom.antisymmetrization f }.map
        f ≫
      { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
            map := fun {X Y} f => OrderHom.antisymmetrization f }.map
        g
[PROOFSTEP]
ext x
[GOAL]
case w
X✝ Y✝ Z✝ : PreordCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x :
  (forget PartOrdCat).obj
    ({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
          map := fun {X Y} f => OrderHom.antisymmetrization f }.obj
      X✝)
⊢ ↑({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
              map := fun {X Y} f => OrderHom.antisymmetrization f }.map
          (f ≫ g))
      x =
    ↑({ obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
                map := fun {X Y} f => OrderHom.antisymmetrization f }.map
            f ≫
          { obj := fun X => PartOrdCat.of (Antisymmetrization ↑X fun x x_1 => x ≤ x_1),
                map := fun {X Y} f => OrderHom.antisymmetrization f }.map
            g)
      x
[PROOFSTEP]
exact Quotient.inductionOn' x fun x => OrderHom.antisymmetrization_apply_mk _ _


[GOAL]
α β : BoolAlgCat
e : ↑α ≃o ↑β
⊢ ((let src :=
        { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α),
                      SupHom.toFun
                          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) ≫
      let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β),
                                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : BoolAlgCat
e : ↑α ≃o ↑β
x✝ : (forget BoolAlgCat).obj α
⊢ ↑((let src :=
            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α),
                          SupHom.toFun
                              { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) ≫
          let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β),
                                        ↑(OrderIso.symm e) (a ⊓ b) =
                                          ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : BoolAlgCat
e : ↑α ≃o ↑β
⊢ ((let src :=
        {
          toSupHom :=
            { toFun := ↑(OrderIso.symm e),
              map_sup' :=
                (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
          map_inf' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑(OrderIso.symm e),
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑β),
                      SupHom.toFun
                          {
                              toSupHom :=
                                { toFun := ↑(OrderIso.symm e),
                                  map_sup' :=
                                    (_ :
                                      ∀ (a b : ↑β),
                                        ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                              map_inf' :=
                                (_ :
                                  ∀ (a b : ↑β),
                                    ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            {
                                toSupHom :=
                                  { toFun := ↑(OrderIso.symm e),
                                    map_sup' :=
                                      (_ :
                                        ∀ (a b : ↑β),
                                          ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                map_inf' :=
                                  (_ :
                                    ∀ (a b : ↑β),
                                      ↑(OrderIso.symm e) (a ⊓ b) =
                                        ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑β),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) ≫
      let src :=
        { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
          map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
      {
        toLatticeHom :=
          {
            toSupHom :=
              { toFun := ↑e,
                map_sup' :=
                  (_ :
                    ∀ (a b : ↑α),
                      SupHom.toFun
                          { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                              map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                          (a ⊔ b) =
                        SupHom.toFun
                            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            a ⊔
                          SupHom.toFun
                            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                            b) },
            map_inf' :=
              (_ :
                ∀ (a b : ↑α),
                  SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
        map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) }) =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : BoolAlgCat
e : ↑α ≃o ↑β
x✝ : (forget BoolAlgCat).obj β
⊢ ↑((let src :=
            {
              toSupHom :=
                { toFun := ↑(OrderIso.symm e),
                  map_sup' :=
                    (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
              map_inf' :=
                (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⊓ b) = ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑(OrderIso.symm e),
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑β),
                          SupHom.toFun
                              {
                                  toSupHom :=
                                    { toFun := ↑(OrderIso.symm e),
                                      map_sup' :=
                                        (_ :
                                          ∀ (a b : ↑β),
                                            ↑(OrderIso.symm e) (a ⊔ b) = ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                  map_inf' :=
                                    (_ :
                                      ∀ (a b : ↑β),
                                        ↑(OrderIso.symm e) (a ⊓ b) =
                                          ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                {
                                    toSupHom :=
                                      { toFun := ↑(OrderIso.symm e),
                                        map_sup' :=
                                          (_ :
                                            ∀ (a b : ↑β),
                                              ↑(OrderIso.symm e) (a ⊔ b) =
                                                ↑(OrderIso.symm e) a ⊔ ↑(OrderIso.symm e) b) },
                                    map_inf' :=
                                      (_ :
                                        ∀ (a b : ↑β),
                                          ↑(OrderIso.symm e) (a ⊓ b) =
                                            ↑(OrderIso.symm e) a ⊓ ↑(OrderIso.symm e) b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑β),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑(OrderIso.symm e) ⊤ = ⊤), map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥) }) ≫
          let src :=
            { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
              map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) };
          {
            toLatticeHom :=
              {
                toSupHom :=
                  { toFun := ↑e,
                    map_sup' :=
                      (_ :
                        ∀ (a b : ↑α),
                          SupHom.toFun
                              { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                  map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                              (a ⊔ b) =
                            SupHom.toFun
                                { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                a ⊔
                              SupHom.toFun
                                { toSupHom := { toFun := ↑e, map_sup' := (_ : ∀ (a b : ↑α), ↑e (a ⊔ b) = ↑e a ⊔ ↑e b) },
                                    map_inf' := (_ : ∀ (a b : ↑α), ↑e (a ⊓ b) = ↑e a ⊓ ↑e b) }.toSupHom
                                b) },
                map_inf' :=
                  (_ :
                    ∀ (a b : ↑α),
                      SupHom.toFun src.toSupHom (a ⊓ b) = SupHom.toFun src.toSupHom a ⊓ SupHom.toFun src.toSupHom b) },
            map_top' := (_ : ↑e ⊤ = ⊤), map_bot' := (_ : ↑e ⊥ = ⊥) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
α β : BddOrdCat
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : BddOrdCat
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
x✝ : (forget BddOrdCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x✝ = ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : BddOrdCat
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : BddOrdCat
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
x✝ : (forget BddOrdCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x✝ = ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _


[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
⊢ ∃ s x, r ≤ s
[PROOFSTEP]
let S := {s | IsPartialOrder α s}
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
⊢ ∃ s x, r ≤ s
[PROOFSTEP]
have hS : ∀ c, c ⊆ S → IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub :=
  by
  rintro c hc₁ hc₂ s hs
  haveI := (hc₁ hs).1
  refine' ⟨sSup c, _, fun z hz => le_sSup hz⟩
  refine'
      { refl := _
        trans := _
        antisymm := _ } <;>
    simp_rw [binary_relation_sSup_iff]
  · intro x
    exact ⟨s, hs, refl x⟩
  · rintro x y z ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
    haveI : IsPartialOrder _ _ := hc₁ h₁s₁
    haveI : IsPartialOrder _ _ := hc₁ h₁s₂
    cases' hc₂.total h₁s₁ h₁s₂ with h h
    · exact ⟨s₂, h₁s₂, _root_.trans (h _ _ h₂s₁) h₂s₂⟩
    · exact ⟨s₁, h₁s₁, _root_.trans h₂s₁ (h _ _ h₂s₂)⟩
  · rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
    haveI : IsPartialOrder _ _ := hc₁ h₁s₁
    haveI : IsPartialOrder _ _ := hc₁ h₁s₂
    cases' hc₂.total h₁s₁ h₁s₂ with h h
    · exact antisymm (h _ _ h₂s₁) h₂s₂
    · apply antisymm h₂s₁ (h _ _ h₂s₂)
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
⊢ ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
[PROOFSTEP]
rintro c hc₁ hc₂ s hs
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
[PROOFSTEP]
haveI := (hc₁ hs).1
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
[PROOFSTEP]
refine' ⟨sSup c, _, fun z hz => le_sSup hz⟩
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ sSup c ∈ S
[PROOFSTEP]
refine'
  { refl := _
    trans := _
    antisymm := _ }
[GOAL]
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a : α), sSup c a a
[PROOFSTEP]
simp_rw [binary_relation_sSup_iff]
[GOAL]
case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b c_1 : α), sSup c a b → sSup c b c_1 → sSup c a c_1
[PROOFSTEP]
simp_rw [binary_relation_sSup_iff]
[GOAL]
case refine'_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), sSup c a b → sSup c b a → a = b
[PROOFSTEP]
simp_rw [binary_relation_sSup_iff]
[GOAL]
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a : α), ∃ r, r ∈ c ∧ r a a
[PROOFSTEP]
intro x
[GOAL]
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x : α
⊢ ∃ r, r ∈ c ∧ r x x
[PROOFSTEP]
exact ⟨s, hs, refl x⟩
[GOAL]
case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b c_1 : α), (∃ r, r ∈ c ∧ r a b) → (∃ r, r ∈ c ∧ r b c_1) → ∃ r, r ∈ c ∧ r a c_1
[PROOFSTEP]
rintro x y z ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
⊢ ∃ r, r ∈ c ∧ r x z
[PROOFSTEP]
haveI : IsPartialOrder _ _ := hc₁ h₁s₁
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this : IsPartialOrder α s₁
⊢ ∃ r, r ∈ c ∧ r x z
[PROOFSTEP]
haveI : IsPartialOrder _ _ := hc₁ h₁s₂
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ ∃ r, r ∈ c ∧ r x z
[PROOFSTEP]
cases' hc₂.total h₁s₁ h₁s₂ with h h
[GOAL]
case refine'_2.intro.intro.intro.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₁ ≤ s₂
⊢ ∃ r, r ∈ c ∧ r x z
[PROOFSTEP]
exact ⟨s₂, h₁s₂, _root_.trans (h _ _ h₂s₁) h₂s₂⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₂ ≤ s₁
⊢ ∃ r, r ∈ c ∧ r x z
[PROOFSTEP]
exact ⟨s₁, h₁s₁, _root_.trans h₂s₁ (h _ _ h₂s₂)⟩
[GOAL]
case refine'_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), (∃ r, r ∈ c ∧ r a b) → (∃ r, r ∈ c ∧ r b a) → a = b
[PROOFSTEP]
rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
[GOAL]
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
⊢ x = y
[PROOFSTEP]
haveI : IsPartialOrder _ _ := hc₁ h₁s₁
[GOAL]
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this : IsPartialOrder α s₁
⊢ x = y
[PROOFSTEP]
haveI : IsPartialOrder _ _ := hc₁ h₁s₂
[GOAL]
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ x = y
[PROOFSTEP]
cases' hc₂.total h₁s₁ h₁s₂ with h h
[GOAL]
case refine'_3.intro.intro.intro.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₁ ≤ s₂
⊢ x = y
[PROOFSTEP]
exact antisymm (h _ _ h₂s₁) h₂s₂
[GOAL]
case refine'_3.intro.intro.intro.intro.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₂ ≤ s₁
⊢ x = y
[PROOFSTEP]
apply antisymm h₂s₁ (h _ _ h₂s₂)
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
⊢ ∃ s x, r ≤ s
[PROOFSTEP]
obtain ⟨s, hs₁ : IsPartialOrder _ _, rs, hs₂⟩ := zorn_nonempty_partialOrder₀ S hS r ‹_›
[GOAL]
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
⊢ ∃ s x, r ≤ s
[PROOFSTEP]
haveI : IsPartialOrder α s := hs₁
[GOAL]
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
⊢ ∃ s x, r ≤ s
[PROOFSTEP]
refine ⟨s, { total := ?_, refl := hs₁.refl, trans := hs₁.trans, antisymm := hs₁.antisymm }, rs⟩
[GOAL]
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
⊢ ∀ (a b : α), s a b ∨ s b a
[PROOFSTEP]
intro x y
[GOAL]
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
⊢ s x y ∨ s y x
[PROOFSTEP]
by_contra' h
[GOAL]
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
⊢ False
[PROOFSTEP]
let s' x' y' := s x' y' ∨ s x' x ∧ s y y'
[GOAL]
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ False
[PROOFSTEP]
rw [← hs₂ s' _ fun _ _ ↦ Or.inl] at h
[GOAL]
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False
[PROOFSTEP]
apply h.1 (Or.inr ⟨refl _, refl _⟩)
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S
[PROOFSTEP]
refine'
  { refl := fun x ↦ Or.inl (refl _)
    trans := _
    antisymm := _ }
[GOAL]
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b c : α), s' a b → s' b c → s' a c
case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b : α), s' a b → s' b a → a = b
[PROOFSTEP]
rintro a b c (ab | ⟨ax : s a x, yb : s y b⟩) (bc | ⟨bx : s b x, yc : s y c⟩)
[GOAL]
case refine'_1.inl.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bc : s b c
⊢ s' a c
[PROOFSTEP]
exact Or.inl (_root_.trans ab bc)
[GOAL]
case refine'_1.inl.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bx : s b x
yc : s y c
⊢ s' a c
[PROOFSTEP]
exact Or.inr ⟨_root_.trans ab bx, yc⟩
[GOAL]
case refine'_1.inr.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bc : s b c
⊢ s' a c
[PROOFSTEP]
exact Or.inr ⟨ax, _root_.trans yb bc⟩
[GOAL]
case refine'_1.inr.intro.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c
[PROOFSTEP]
exact Or.inr ⟨ax, yc⟩
[GOAL]
case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b : α), s' a b → s' b a → a = b
[PROOFSTEP]
rintro a b (ab | ⟨ax : s a x, yb : s y b⟩) (ba | ⟨bx : s b x, ya : s y a⟩)
[GOAL]
case refine'_2.inl.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
ba : s b a
⊢ a = b
[PROOFSTEP]
exact antisymm ab ba
[GOAL]
case refine'_2.inl.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
bx : s b x
ya : s y a
⊢ a = b
[PROOFSTEP]
exact (h.2 (_root_.trans ya (_root_.trans ab bx))).elim
[GOAL]
case refine'_2.inr.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b
[PROOFSTEP]
exact (h.2 (_root_.trans yb (_root_.trans ba ax))).elim
[GOAL]
case refine'_2.inr.intro.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b
[PROOFSTEP]
exact (h.2 (_root_.trans yb bx)).elim