awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ i ∈ c, Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) i : β) ((g : (a : α) → β) i : β)
e_a : Eq (α := Chain β) (c.map (↑f : α →o β)) (c.map (↑g : α →o β))
⊢ ωSup (c.map (↑f : α →o β)) = ωSup (c.map (↑g : α →o β))

Tactic:
congr 1
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ i ∈ c, Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) i : β) ((g : (a : α) → β) i : β)
e_a : ∀ (x : ℕ), Eq (α := β) ((c.map (↑f : α →o β) : (a : ℕ) → β) x : β) ((c.map (↑g : α →o β) : (a : ℕ) → β) x : β)
⊢ Eq (α := Chain β) (c.map (↑f : α →o β)) (c.map (↑g : α →o β))

Tactic:
ext x
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ i ∈ c, Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) i : β) ((g : (a : α) → β) i : β)
x : ℕ
⊢ Eq (α := β) ((c.map (↑f : α →o β) : (a : ℕ) → β) x : β) ((c.map (↑g : α →o β) : (a : ℕ) → β) x : β)

Tactic:
apply hc _ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
x : s.pt.carrier
⊢ Eq (α := Y.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) f :
          (a : X.carrier) → Y.carrier)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
              (a : s.pt.carrier) → X.carrier)
            x :
          X.carrier) :
      Y.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) g :
          (a : X.carrier) → Y.carrier)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
              (a : s.pt.carrier) → X.carrier)
            x :
          X.carrier) :
      Y.carrier)

Tactic:
apply ContinuousHom.congr_fun s.condition

Premises used: CategoryTheory.Limits.Fork.condition, OmegaCompletePartialOrder.ContinuousHom.congr_fun
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
h :
  ∀ (x : s.pt.carrier),
    Eq (α := X.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X := s.pt)
              ({
                  toFun := fun (x : s.pt.carrier) ↦
                    Subtype.mk (p := fun (a : X.carrier) ↦
                      Eq (α := Y.carrier)
                        ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                                f :
                              (a : X.carrier) → Y.carrier)
                            a :
                          Y.carrier)
                        ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                                g :
                              (a : X.carrier) → Y.carrier)
                            a :
                          Y.carrier))
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                            s.ι :
                          (a : s.pt.carrier) → X.carrier)
                        x)
                      ⋯,
                  monotone' := ⋯, map_ωSup' := ⋯ } ≫
                (equalizer f g).ι) :
            (a : s.pt.carrier) → X.carrier)
          x :
        X.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
            (a : s.pt.carrier) → X.carrier)
          x :
        X.carrier)
⊢ {
        toFun := fun (x : s.pt.carrier) ↦
          Subtype.mk (p := fun (a : X.carrier) ↦
            Eq (α := Y.carrier)
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) f :
                    (a : X.carrier) → Y.carrier)
                  a :
                Y.carrier)
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) g :
                    (a : X.carrier) → Y.carrier)
                  a :
                Y.carrier))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
                (a : s.pt.carrier) → X.carrier)
              x)
            ⋯,
        monotone' := ⋯, map_ωSup' := ⋯ } ≫
      (equalizer f g).ι =
    s.ι

Tactic:
ext
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
x : s.pt.carrier
⊢ Eq (α := X.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X := s.pt)
            ({
                toFun := fun (x : s.pt.carrier) ↦
                  Subtype.mk (p := fun (a : X.carrier) ↦
                    Eq (α := Y.carrier)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                              f :
                            (a : X.carrier) → Y.carrier)
                          a :
                        Y.carrier)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                              g :
                            (a : X.carrier) → Y.carrier)
                          a :
                        Y.carrier))
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                          s.ι :
                        (a : s.pt.carrier) → X.carrier)
                      x)
                    ⋯,
                monotone' := ⋯, map_ωSup' := ⋯ } ≫
              (equalizer f g).ι) :
          (a : s.pt.carrier) → X.carrier)
        x :
      X.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
          (a : s.pt.carrier) → X.carrier)
        x :
      X.carrier)

Tactic:
rfl
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m : s.pt ⟶ (equalizer f g).pt
hm : m ≫ (equalizer f g).ι = s.ι
h :
  ∀ (x : s.pt.carrier),
    Eq (α := (equalizer f g).pt.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
            (a : s.pt.carrier) → (equalizer f g).pt.carrier)
          x :
        (equalizer f g).pt.carrier)
      ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
              (equalizer f g).pt
              {
                toFun := fun (x : s.pt.carrier) ↦
                  Subtype.mk (p := fun (a : X.carrier) ↦
                    Eq (α := Y.carrier)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                              f :
                            (a : X.carrier) → Y.carrier)
                          a :
                        Y.carrier)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                              g :
                            (a : X.carrier) → Y.carrier)
                          a :
                        Y.carrier))
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                          s.ι :
                        (a : s.pt.carrier) → X.carrier)
                      x)
                    ⋯,
                monotone' := ⋯, map_ωSup' := ⋯ } :
            (a : s.pt.carrier) → (equalizer f g).pt.carrier)
          x :
        (equalizer f g).pt.carrier)
⊢ m =
    {
      toFun := fun (x : s.pt.carrier) ↦
        Subtype.mk (p := fun (a : X.carrier) ↦
          Eq (α := Y.carrier)
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) f :
                  (a : X.carrier) → Y.carrier)
                a :
              Y.carrier)
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) g :
                  (a : X.carrier) → Y.carrier)
                a :
              Y.carrier))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
              (a : s.pt.carrier) → X.carrier)
            x)
          ⋯,
      monotone' := ⋯, map_ωSup' := ⋯ }

Tactic:
ext x : 2
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m : s.pt ⟶ (equalizer f g).pt
hm : m ≫ (equalizer f g).ι = s.ι
x : s.pt.carrier
apply :
  Eq.{v + 1} (α := X.carrier)
    (↑((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
            (a : s.pt.carrier) → (equalizer f g).pt.carrier)
          x) :
      X.carrier)
    (↑((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
              (equalizer f g).pt
              {
                toFun := fun (x : s.pt.carrier) ↦
                  Subtype.mk (p := fun (a : X.carrier) ↦
                    Eq (α := Y.carrier)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                              f :
                            (a : X.carrier) → Y.carrier)
                          a :
                        Y.carrier)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                              g :
                            (a : X.carrier) → Y.carrier)
                          a :
                        Y.carrier))
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                          s.ι :
                        (a : s.pt.carrier) → X.carrier)
                      x)
                    ⋯,
                monotone' := ⋯, map_ωSup' := ⋯ } :
            (a : s.pt.carrier) → (equalizer f g).pt.carrier)
          x) :
      X.carrier)
⊢ Eq (α := (equalizer f g).pt.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (equalizer f g).pt.carrier)
        x :
      (equalizer f g).pt.carrier)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
            (equalizer f g).pt
            {
              toFun := fun (x : s.pt.carrier) ↦
                Subtype.mk (p := fun (a : X.carrier) ↦
                  Eq (α := Y.carrier)
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) f :
                          (a : X.carrier) → Y.carrier)
                        a :
                      Y.carrier)
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) g :
                          (a : X.carrier) → Y.carrier)
                        a :
                      Y.carrier))
                  ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) s.ι :
                      (a : s.pt.carrier) → X.carrier)
                    x)
                  ⋯,
              monotone' := ⋯, map_ωSup' := ⋯ } :
          (a : s.pt.carrier) → (equalizer f g).pt.carrier)
        x :
      (equalizer f g).pt.carrier)

Tactic:
apply Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m : s.pt ⟶ (equalizer f g).pt
hm : m ≫ (equalizer f g).ι = s.ι
x : s.pt.carrier
⊢ Eq.{v + 1} (α := X.carrier)
    (↑((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
            (a : s.pt.carrier) → (equalizer f g).pt.carrier)
          x) :
      X.carrier)
    (↑((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
              (equalizer f g).pt
              {
                toFun := fun (x : s.pt.carrier) ↦
                  Subtype.mk (p := fun (a : X.carrier) ↦
                    Eq (α := Y.carrier)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                              f :
                            (a : X.carrier) → Y.carrier)
                          a :
                        Y.carrier)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                              g :
                            (a : X.carrier) → Y.carrier)
                          a :
                        Y.carrier))
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier)
                          s.ι :
                        (a : s.pt.carrier) → X.carrier)
                      x)
                    ⋯,
                monotone' := ⋯, map_ωSup' := ⋯ } :
            (a : s.pt.carrier) → (equalizer f g).pt.carrier)
          x) :
      X.carrier)

Tactic:
apply ContinuousHom.congr_fun hm

Premises used: OmegaCompletePartialOrder.ContinuousHom.congr_fun
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
⊢ HasProducts ωCPO

Tactic:
fun _ => { has_limit := fun _ => hasLimit_of_iso Discrete.natIsoFunctor.symm }

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Discrete.natIsoFunctor, CategoryTheory.Iso.symm
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
X Y : ωCPO
f g : X ⟶ Y
⊢ HasLimit (parallelPair f g)

Tactic:
HasLimit.mk ⟨_, HasEqualizers.isEqualizer f g⟩

Premises used: ωCPO.HasEqualizers.isEqualizer, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
⊢ HasEqualizers ωCPO

Tactic:
hasEqualizers_of_hasLimit_parallelPair _

Premises used: CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
⊢ HasLimits ωCPO

Tactic:
has_limits_of_hasEqualizers_and_products

Premises used: CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : PartOrd
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y Z : PartOrd
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
            g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
            f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y : PartOrd
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
              f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
              g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : Type u
inst : PartialOrder X
⊢ (↑{ carrier := X, str := inst : PartOrd.{u} } : Type u) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : PartOrd
⊢ Hom.hom (𝟙 X) = OrderHom.id

Tactic:
rfl

Premises used: OrderHom.id, rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : PartOrd
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y Z : PartOrd
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y Z : PartOrd
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u_1)
⊢ Eq (α := (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑X : Type u_1)) → (↑Z : Type u_1))
        x :
      (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
            g :
          (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC :=
                carrier) f :
              (a : (↑X : Type u_1)) → (↑Y : Type u_1))
            x :
          (↑Y : Type u_1)) :
      (↑Z : Type u_1))

Tactic:
simp
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y : PartOrd
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: PartOrd.Hom.ext
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y : Type u
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X →o Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y : PartOrd
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : Type u
inst : PartialOrder X
⊢ ofHom OrderHom.id = 𝟙 { carrier := X, str := inst : PartOrd.{u} }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y Z : Type u
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : PartialOrder Z
f : X →o Y
g : Y →o Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y : Type u
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X →o Y
x : X
⊢ Eq (α := (↑{ carrier := Y, str := inst_1 } : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u}) ↦ (↑x1 : Type u) →o (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑{ carrier := X, str := inst } : Type u)) → (↑{ carrier := Y, str := inst_1 } : Type u))
        x :
      (↑{ carrier := Y, str := inst_1 } : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y : PartOrd
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑Y : Type u_1)) → (↑X : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
              e.hom :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y : PartOrd
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
              e.inv :
            (a : (↑Y : Type u_1)) → (↑X : Type u_1))
          s :
        (↑X : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Order.Category.PartOrd
Goal:
⊢ PartOrd.dual ⋙
      forget₂ PartOrd (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := PartOrd.carrier)
        Preord (FD := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := Preord.carrier) =
    forget₂ PartOrd (FC := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := PartOrd.carrier)
        Preord (FD := fun (x1 x2 : Preord.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := Preord.carrier) ⋙
      Preord.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, PartOrd.dual, OrderDual, rfl
-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : Preord
hf :
  ∀
    (x :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u)),
    Eq (α :=
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
      ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization) :
            (a :
                (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                      str := instPartialOrderAntisymmetrization } :
                  Type u)) →
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u))
          x :
        (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
              str := instPartialOrderAntisymmetrization } :
          Type u))
      ((PartOrd.Hom.hom
              (𝟙
                { carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization : PartOrd.{u} }) :
            (a :
                (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                      str := instPartialOrderAntisymmetrization } :
                  Type u)) →
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u))
          x :
        (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
              str := instPartialOrderAntisymmetrization } :
          Type u))
⊢ PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization =
    𝟙
      { carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
        str := instPartialOrderAntisymmetrization }

Tactic:
ext x