[GOAL]
⊢ ConcreteCategory HeytAlgCat
[PROOFSTEP]
dsimp [HeytAlgCat]
[GOAL]
⊢ ConcreteCategory (Bundled HeytingAlgebra)
[PROOFSTEP]
infer_instance
  -- Porting note: No idea why it does not find this instance...
[GOAL]
α β : HeytAlgCat
e : ↑α ≃o ↑β
⊢ {
        toLatticeHom :=
          { 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) },
        map_bot' := (_ : ↑e ⊥ = ⊥), map_himp' := (_ : ∀ (a b : ↑α), ↑e (a ⇨ b) = ↑e a ⇨ ↑e b) } ≫
      {
        toLatticeHom :=
          {
            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) },
        map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥),
        map_himp' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⇨ b) = ↑(OrderIso.symm e) a ⇨ ↑(OrderIso.symm e) b) } =
    𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : HeytAlgCat
e : ↑α ≃o ↑β
x✝ : (forget HeytAlgCat).obj α
⊢ ↑({
            toLatticeHom :=
              { 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) },
            map_bot' := (_ : ↑e ⊥ = ⊥), map_himp' := (_ : ∀ (a b : ↑α), ↑e (a ⇨ b) = ↑e a ⇨ ↑e b) } ≫
          {
            toLatticeHom :=
              {
                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) },
            map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥),
            map_himp' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⇨ b) = ↑(OrderIso.symm e) a ⇨ ↑(OrderIso.symm e) b) })
      x✝ =
    ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : HeytAlgCat
e : ↑α ≃o ↑β
⊢ {
        toLatticeHom :=
          {
            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) },
        map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥),
        map_himp' := (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⇨ b) = ↑(OrderIso.symm e) a ⇨ ↑(OrderIso.symm e) b) } ≫
      {
        toLatticeHom :=
          { 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) },
        map_bot' := (_ : ↑e ⊥ = ⊥), map_himp' := (_ : ∀ (a b : ↑α), ↑e (a ⇨ b) = ↑e a ⇨ ↑e b) } =
    𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : HeytAlgCat
e : ↑α ≃o ↑β
x✝ : (forget HeytAlgCat).obj β
⊢ ↑({
            toLatticeHom :=
              {
                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) },
            map_bot' := (_ : ↑(OrderIso.symm e) ⊥ = ⊥),
            map_himp' :=
              (_ : ∀ (a b : ↑β), ↑(OrderIso.symm e) (a ⇨ b) = ↑(OrderIso.symm e) a ⇨ ↑(OrderIso.symm e) b) } ≫
          {
            toLatticeHom :=
              { 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) },
            map_bot' := (_ : ↑e ⊥ = ⊥), map_himp' := (_ : ∀ (a b : ↑α), ↑e (a ⇨ b) = ↑e a ⇨ ↑e b) })
      x✝ =
    ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
