awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd :=
  of
    (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f) :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          ⊤) :
      Type u)
e : X ⟶ I :=
  ofHom
    {
      toFun := fun (x : (↑X.1 : Type u)) ↦
        Subtype.mk (p := fun (x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y) ↦
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                    (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                    (↑X.toLinOrd : Type u)) f) :
                (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                  (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
              ⊤)
            x)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f :
              (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
            x)
          ⋯,
      monotone' := ⋯ }
m : I ⟶ Y :=
  ofHom
    {
      toFun :=
        fun
          (y :
            (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                        (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                        (↑X.toLinOrd : Type u)) f) :
                    (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                      (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
                  ⊤) :
              Type u)) ↦
        (↑y : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y),
      monotone' := ⋯ }
⊢ Epi e

Tactic:
haveI : Epi e := by
      rw [epi_iff_surjective]
      rintro ⟨_, y, h, rfl⟩
      exact ⟨y, rfl⟩
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd :=
  of
    (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f) :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          ⊤) :
      Type u)
e : X ⟶ I :=
  ofHom
    {
      toFun := fun (x : (↑X.1 : Type u)) ↦
        Subtype.mk (p := fun (x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y) ↦
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                    (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                    (↑X.toLinOrd : Type u)) f) :
                (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                  (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
              ⊤)
            x)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f :
              (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
            x)
          ⋯,
      monotone' := ⋯ }
m : I ⟶ Y :=
  ofHom
    {
      toFun :=
        fun
          (y :
            (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                        (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                        (↑X.toLinOrd : Type u)) f) :
                    (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                      (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
                  ⊤) :
              Type u)) ↦
        (↑y : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y),
      monotone' := ⋯ }
this : Epi e
⊢ StrongEpi e

Tactic:
haveI : StrongEpi e := strongEpi_of_epi e
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd :=
  of
    (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f) :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          ⊤) :
      Type u)
e : X ⟶ I :=
  ofHom
    {
      toFun := fun (x : (↑X.1 : Type u)) ↦
        Subtype.mk (p := fun (x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y) ↦
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                    (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                    (↑X.toLinOrd : Type u)) f) :
                (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                  (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
              ⊤)
            x)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f :
              (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
            x)
          ⋯,
      monotone' := ⋯ }
m : I ⟶ Y :=
  ofHom
    {
      toFun :=
        fun
          (y :
            (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                        (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                        (↑X.toLinOrd : Type u)) f) :
                    (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                      (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
                  ⊤) :
              Type u)) ↦
        (↑y : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y),
      monotone' := ⋯ }
this_1 : Epi e
this : StrongEpi e
⊢ Mono m

Tactic:
haveI : Mono m := ConcreteCategory.mono_of_injective _ (fun x y h => Subtype.ext h)
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd :=
  of
    (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f) :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          ⊤) :
      Type u)
e : X ⟶ I :=
  ofHom
    {
      toFun := fun (x : (↑X.1 : Type u)) ↦
        Subtype.mk (p := fun (x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y) ↦
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                    (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                    (↑X.toLinOrd : Type u)) f) :
                (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                  (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
              ⊤)
            x)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f :
              (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
            x)
          ⋯,
      monotone' := ⋯ }
m : I ⟶ Y :=
  ofHom
    {
      toFun :=
        fun
          (y :
            (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                        (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                        (↑X.toLinOrd : Type u)) f) :
                    (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                      (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
                  ⊤) :
              Type u)) ↦
        (↑y : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y),
      monotone' := ⋯ }
this_1 : Epi e
this_2 : StrongEpi e
this : Mono m
⊢ Nonempty.{u + 2} (StrongEpiMonoFactorisation f)

Tactic:
⟨⟨I, m, e, rfl⟩⟩

Premises used: CategoryTheory.Limits.MonoFactorisation.mk, CategoryTheory.Limits.StrongEpiMonoFactorisation.mk, Nonempty.intro, rfl
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd :=
  of
    (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f) :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          ⊤) :
      Type u)
e : X ⟶ I :=
  ofHom
    {
      toFun := fun (x : (↑X.1 : Type u)) ↦
        Subtype.mk (p := fun (x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y) ↦
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                    (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                    (↑X.toLinOrd : Type u)) f) :
                (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                  (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
              ⊤)
            x)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f :
              (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
            x)
          ⋯,
      monotone' := ⋯ }
m : I ⟶ Y :=
  ofHom
    {
      toFun :=
        fun
          (y :
            (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                        (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                        (↑X.toLinOrd : Type u)) f) :
                    (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                      (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
                  ⊤) :
              Type u)) ↦
        (↑y : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y),
      monotone' := ⋯ }
this_1 : Epi e
this_2 : StrongEpi e
this : Mono m
⊢ Nonempty.{u + 2} (StrongEpiMonoFactorisation f)

Tactic:
exact ⟨⟨I, m, e, rfl⟩⟩
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
⊢ NonemptyFinLinOrd.dual ⋙
      forget₂ NonemptyFinLinOrd (FC := fun (x1 x2 : NonemptyFinLinOrd.{u_1}) ↦
        (↑x1.toLinOrd : Type u_1) →o (↑x2.toLinOrd : Type u_1)) (CC := fun (X : NonemptyFinLinOrd.{u_1}) ↦
        (↑X.toLinOrd : Type u_1)) LinOrd (FD := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1))
        (CD := LinOrd.carrier) =
    forget₂ NonemptyFinLinOrd (FC := fun (x1 x2 : NonemptyFinLinOrd.{u_1}) ↦
        (↑x1.toLinOrd : Type u_1) →o (↑x2.toLinOrd : Type u_1)) (CC := fun (X : NonemptyFinLinOrd.{u_1}) ↦
        (↑X.toLinOrd : Type u_1)) LinOrd (FD := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1))
        (CD := LinOrd.carrier) ⋙
      LinOrd.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.inducedFunctor, NonemptyFinLinOrd.dual, OrderDual, rfl
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
⊢ { carrier := α, str := inst : ωCPO.{u_1} }.carrier = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
h :
  ∀ (t : s.pt.carrier),
    Eq (α := (product f).pt.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
            (a : s.pt.carrier) → (product f).pt.carrier)
          t :
        (product f).pt.carrier)
      ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
              (product f).pt
              {
                toFun := fun (t : s.pt.carrier) (j : J) ↦
                  (ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X :=
                        Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
                        (s.π.app { as := j }) :
                      (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
                        ((Discrete.functor f).obj { as := j }).carrier)
                    t,
                monotone' := ⋯, map_ωSup' := ⋯ } :
            (a : s.pt.carrier) → (product f).pt.carrier)
          t :
        (product f).pt.carrier)
⊢ m =
    {
      toFun := fun (t : s.pt.carrier) (j : J) ↦
        (ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X :=
              Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
              (s.π.app { as := j }) :
            (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
              ((Discrete.functor f).obj { as := j }).carrier)
          t,
      monotone' := ⋯, map_ωSup' := ⋯ }

Tactic:
ext t
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
h :
  ∀ (j : J),
    Eq (α := (f j).carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
            (a : s.pt.carrier) → (product f).pt.carrier)
          t j :
        (f j).carrier)
      ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
              (product f).pt
              {
                toFun := fun (t : s.pt.carrier) (j : J) ↦
                  (ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X :=
                        Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
                        (s.π.app { as := j }) :
                      (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
                        ((Discrete.functor f).obj { as := j }).carrier)
                    t,
                monotone' := ⋯, map_ωSup' := ⋯ } :
            (a : s.pt.carrier) → (product f).pt.carrier)
          t j :
        (f j).carrier)
⊢ Eq (α := (product f).pt.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t :
      (product f).pt.carrier)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
            (product f).pt
            {
              toFun := fun (t : s.pt.carrier) (j : J) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X :=
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
                      (s.π.app { as := j }) :
                    (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
                      ((Discrete.functor f).obj { as := j }).carrier)
                  t,
              monotone' := ⋯, map_ωSup' := ⋯ } :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t :
      (product f).pt.carrier)

Tactic:
funext j
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
h :
  Eq (α := (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t j :
      (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X :=
            Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
            (s.π.app { as := j }) :
          (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
            ((Discrete.functor f).obj { as := j }).carrier)
        t :
      (Functor.obj (Discrete.functor f) { as := j : Discrete J }).carrier)
⊢ Eq (α := (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t j :
      (f j).carrier)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) carrier _ _ s.pt
            (product f).pt
            {
              toFun := fun (t : s.pt.carrier) (j : J) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X :=
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
                      (s.π.app { as := j }) :
                    (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
                      ((Discrete.functor f).obj { as := j }).carrier)
                  t,
              monotone' := ⋯, map_ωSup' := ⋯ } :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t j :
      (f j).carrier)

Tactic:
change m t j = (s.π.app ⟨j⟩) t

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Discrete.mk, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
h :
  Eq (α := (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t j :
      (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (Y :=
            Functor.obj (Discrete.functor f) { as := j : Discrete J }) (m ≫ (product f).π.app { as := j }) :
          (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
            ((Discrete.functor f).obj { as := j }).carrier)
        t :
      (Functor.obj (Discrete.functor f) { as := j : Discrete J }).carrier)
⊢ Eq (α := (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t j :
      (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (X :=
            Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
            (s.π.app { as := j }) :
          (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
            ((Discrete.functor f).obj { as := j }).carrier)
        t :
      (Functor.obj (Discrete.functor f) { as := j : Discrete J }).carrier)

Tactic:
rw [← w ⟨j⟩]

Premises used: CategoryTheory.Discrete.mk
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
⊢ Eq (α := (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) m :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t j :
      (f j).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ωCPO.{v}) ↦ x1.carrier →𝒄 x2.carrier) (CC := carrier) (Y :=
            Functor.obj (Discrete.functor f) { as := j : Discrete J }) (m ≫ (product f).π.app { as := j }) :
          (a : (((Functor.const (Discrete J)).obj s.pt).obj { as := j }).carrier) →
            ((Discrete.functor f).obj { as := j }).carrier)
        t :
      (Functor.obj (Discrete.functor f) { as := j : Discrete J }).carrier)

Tactic:
rfl
-- Module: Mathlib.Order.Category.OmegaCompletePartialOrder
Goal:
J : Type v
f : J → ωCPO
⊢ HasProduct f

Tactic:
HasLimit.mk ⟨_, isProduct _ f⟩

Premises used: ωCPO.HasProducts.isProduct, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk
-- 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 : β)
rw : ωSup (c.map (↑f : α →o β)) = ωSup (c.map (↑g : α →o β))
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (ωSup c) : β) ((g : (a : α) → β) (ωSup c) : β)

Tactic:
rw [f.continuous, g.continuous]

Premises used: OmegaCompletePartialOrder.ContinuousHom.continuous