awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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
have rw : Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X) (β :=
  (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) I)
  (⇑(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)) e) :
    (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
      (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) I)
Tactic: rw [epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
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' := ⋯ }
⊢ Nonempty.{u + 2} (StrongEpiMonoFactorisation f)
have this : Epi e
Tactic: haveI : Epi e := by
      rw [epi_iff_surjective]
      rintro ⟨_, y, h, rfl⟩
      exact ⟨y, rfl⟩
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
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
⊢ Nonempty.{u + 2} (StrongEpiMonoFactorisation f)
have this₁ : StrongEpi e
Tactic: haveI : StrongEpi e := strongEpi_of_epi e
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
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
⊢ Nonempty.{u + 2} (StrongEpiMonoFactorisation f)
have this₁ : Mono m
Tactic: haveI : Mono m := ConcreteCategory.mono_of_injective _ (fun x y h => Subtype.ext h)
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
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
⊢ 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' := ⋯ }
have 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' := sorry, map_ωSup' := sorry } :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t :
      (product f).pt.carrier)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
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
⊢ 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)
have 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' := sorry, map_ωSup' := sorry } :
          (a : s.pt.carrier) → (product f).pt.carrier)
        t j :
      (f j).carrier)
Tactic: funext j
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
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 _ 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)
have 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)
Tactic: change m t j = (s.π.app ⟨j⟩) t
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
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) (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)
have 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)
Tactic: rw [← w ⟨j⟩]
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
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 : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (ωSup c) : β) ((g : (a : α) → β) (ωSup c) : β)
have rw : ωSup (c.map (↑f : α →o β)) = ωSup (c.map (↑g : α →o β))
Tactic: rw [f.continuous, g.continuous]
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
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 : β)
⊢ ωSup (c.map (↑f : α →o β)) = ωSup (c.map (↑g : α →o β))
have e_a : Eq (α := Chain β) (c.map (↑f : α →o β)) (c.map (↑g : α →o β))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
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 : β)
⊢ Eq (α := Chain β) (c.map (↑f : α →o β)) (c.map (↑g : α →o β))
have e_a : ∀ (x : ℕ), Eq (α := β) ((c.map (↑f : α →o β) : (a : ℕ) → β) x : β) ((c.map (↑g : α →o β) : (a : ℕ) → β) x : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Category.OmegaCompletePartialOrder (goal)
Goal:
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
⊢ {
        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.ι
have 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)
                    sorry,
                monotone' := sorry, map_ωSup' := sorry } ≫
              (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: ext