[GOAL]
⊢ ConcreteCategory ωCPO
[PROOFSTEP]
unfold ωCPO
[GOAL]
⊢ ConcreteCategory (Bundled OmegaCompletePartialOrder)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
⊢ m =
    (fun s =>
        {
          toOrderHom :=
            { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
              monotone' :=
                (_ :
                  ∀ (x y : ↑s.pt),
                    x ≤ y → ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) },
          cont :=
            (_ :
              ∀ (x : Chain ↑s.pt),
                ↑{ toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                        monotone' :=
                          (_ :
                            ∀ (x y : ↑s.pt),
                              x ≤ y →
                                ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) }
                    (ωSup x) =
                  ωSup
                    (Chain.map x
                      { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                        monotone' :=
                          (_ :
                            ∀ (x y : ↑s.pt),
                              x ≤ y →
                                ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) })) })
      s
[PROOFSTEP]
ext t
[GOAL]
case w
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
t : (forget ωCPO).obj s.pt
⊢ ↑m t =
    ↑((fun s =>
            {
              toOrderHom :=
                { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                  monotone' :=
                    (_ :
                      ∀ (x y : ↑s.pt),
                        x ≤ y → ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) },
              cont :=
                (_ :
                  ∀ (x : Chain ↑s.pt),
                    ↑{ toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                            monotone' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  x ≤ y →
                                    ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) }
                        (ωSup x) =
                      ωSup
                        (Chain.map x
                          { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                            monotone' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  x ≤ y →
                                    ∀ (j : J),
                                      ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) })) })
          s)
      t
[PROOFSTEP]
funext j
[GOAL]
case w.h
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
t : (forget ωCPO).obj s.pt
j : J
⊢ ↑m t j =
    ↑((fun s =>
            {
              toOrderHom :=
                { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                  monotone' :=
                    (_ :
                      ∀ (x y : ↑s.pt),
                        x ≤ y → ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) },
              cont :=
                (_ :
                  ∀ (x : Chain ↑s.pt),
                    ↑{ toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                            monotone' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  x ≤ y →
                                    ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) }
                        (ωSup x) =
                      ωSup
                        (Chain.map x
                          { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                            monotone' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  x ≤ y →
                                    ∀ (j : J),
                                      ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) })) })
          s)
      t j
[PROOFSTEP]
change m.toFun t j = (s.π.app ⟨j⟩).toFun t
[GOAL]
case w.h
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
t : (forget ωCPO).obj s.pt
j : J
⊢ OrderHom.toFun m.toOrderHom t j = OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t
[PROOFSTEP]
rw [← w ⟨j⟩]
[GOAL]
case w.h
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
t : (forget ωCPO).obj s.pt
j : J
⊢ OrderHom.toFun m.toOrderHom t j = OrderHom.toFun (m ≫ NatTrans.app (product f).π { as := j }).toOrderHom t
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
⊢ ↑f (ωSup c) = ↑g (ωSup c)
[PROOFSTEP]
rw [f.continuous, g.continuous]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
⊢ ωSup (Chain.map c ↑f) = ωSup (Chain.map c ↑g)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
⊢ Chain.map c ↑f = Chain.map c ↑g
[PROOFSTEP]
apply OrderHom.ext
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
⊢ ↑(Chain.map c ↑f) = ↑(Chain.map c ↑g)
[PROOFSTEP]
funext x
[GOAL]
case e_a.h.h
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
x : ℕ
⊢ ↑(Chain.map c ↑f) x = ↑(Chain.map c ↑g) x
[PROOFSTEP]
apply hc _ ⟨_, rfl⟩
[GOAL]
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
x : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)
⊢ OrderHom.toFun f.toOrderHom (OrderHom.toFun (Fork.ι s).toOrderHom x) =
    OrderHom.toFun g.toOrderHom (OrderHom.toFun (Fork.ι s).toOrderHom x)
[PROOFSTEP]
apply ContinuousHom.congr_fun s.condition
[GOAL]
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
⊢ {
        toOrderHom :=
          {
            toFun := fun x =>
              { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
            monotone' :=
              (_ :
                ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                  x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) },
        cont :=
          (_ :
            ∀ (x : Chain ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
              ↑{
                      toFun := fun x =>
                        { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                          property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                      monotone' :=
                        (_ :
                          ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                            x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) }
                  (ωSup x) =
                ωSup
                  (Chain.map x
                    {
                      toFun := fun x =>
                        { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                          property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                      monotone' :=
                        (_ :
                          ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                            x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) })) } ≫
      Fork.ι (equalizer f g) =
    Fork.ι s
[PROOFSTEP]
ext
[GOAL]
case w
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
x✝ : (forget ωCPO).obj (((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)
⊢ ↑({
            toOrderHom :=
              {
                toFun := fun x =>
                  { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                    property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                monotone' :=
                  (_ :
                    ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                      x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) },
            cont :=
              (_ :
                ∀ (x : Chain ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                  ↑{
                          toFun := fun x =>
                            { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                              property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                          monotone' :=
                            (_ :
                              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) }
                      (ωSup x) =
                    ωSup
                      (Chain.map x
                        {
                          toFun := fun x =>
                            { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                              property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                          monotone' :=
                            (_ :
                              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) })) } ≫
          Fork.ι (equalizer f g))
      x✝ =
    ↑(Fork.ι s) x✝
[PROOFSTEP]
rfl
[GOAL]
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (equalizer f g).pt).obj WalkingParallelPair.zero
hm : m✝ ≫ Fork.ι (equalizer f g) = Fork.ι s
⊢ m✝ =
    {
      toOrderHom :=
        {
          toFun := fun x =>
            { val := OrderHom.toFun (Fork.ι s).toOrderHom x, property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
          monotone' :=
            (_ :
              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) },
      cont :=
        (_ :
          ∀ (x : Chain ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
            ↑{
                    toFun := fun x =>
                      { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                        property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                    monotone' :=
                      (_ :
                        ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                          x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) }
                (ωSup x) =
              ωSup
                (Chain.map x
                  {
                    toFun := fun x =>
                      { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                        property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                    monotone' :=
                      (_ :
                        ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                          x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) })) }
[PROOFSTEP]
apply
  ContinuousHom.ext _ _ fun x =>
    Subtype.ext
      ?_
        -- Porting note: Originally `ext`
[GOAL]
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (equalizer f g).pt).obj WalkingParallelPair.zero
hm : m✝ ≫ Fork.ι (equalizer f g) = Fork.ι s
x : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)
⊢ ↑(↑m✝ x) =
    ↑(↑{
            toOrderHom :=
              {
                toFun := fun x =>
                  { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                    property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                monotone' :=
                  (_ :
                    ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                      x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) },
            cont :=
              (_ :
                ∀ (x : Chain ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                  ↑{
                          toFun := fun x =>
                            { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                              property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                          monotone' :=
                            (_ :
                              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) }
                      (ωSup x) =
                    ωSup
                      (Chain.map x
                        {
                          toFun := fun x =>
                            { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                              property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                          monotone' :=
                            (_ :
                              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) })) }
        x)
[PROOFSTEP]
apply ContinuousHom.congr_fun hm
