[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
X Y : WidePullbackShape J
f : X ⟶ Y
⊢ ((Functor.const (WidePullbackShape J)).obj c.pt.left).map f ≫
      (fun X => Option.casesOn X c.pt.hom fun j => (NatTrans.app c.π { as := j }).left) Y =
    (fun X => Option.casesOn X c.pt.hom fun j => (NatTrans.app c.π { as := j }).left) X ≫
      (widePullbackDiagramOfDiagramOver B F).map f
[PROOFSTEP]
dsimp
[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
X Y : WidePullbackShape J
f : X ⟶ Y
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) Y =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) X ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        X = a →
          Y = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) X ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) Y))
        (fun X_1 h =>
          Eq.rec (motive := fun x x_1 =>
            Y = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) X ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : X ⟶ x) →
                  HEq f (𝟙 X) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) X ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id X = f) ▸ 𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) X))
                (_ : X = Y) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ Y) →
              Y = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = Y) f)
            (_ : some j = X) f)
        f (_ : X = X) (_ : Y = Y) (_ : HEq f f)
[PROOFSTEP]
cases X
[GOAL]
case none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
Y : WidePullbackShape J
f : none ⟶ Y
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) Y =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        none = a →
          Y = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) Y))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            Y = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : none ⟶ x) →
                  HEq f (𝟙 none) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id none = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) none))
                (_ : none = Y) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ Y) →
              Y = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = Y) f)
            (_ : some j = none) f)
        f (_ : none = none) (_ : Y = Y) (_ : HEq f f)
[PROOFSTEP]
cases Y
[GOAL]
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
Y : WidePullbackShape J
val✝ : J
f : some val✝ ⟶ Y
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) Y =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝ = a →
          Y = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) Y))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            Y = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝ ⟶ x) →
                  HEq f (𝟙 (some val✝)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
                (_ : some val✝ = Y) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ Y) →
              Y = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = Y) f)
            (_ : some j = some val✝) f)
        f (_ : some val✝ = some val✝) (_ : Y = Y) (_ : HEq f f)
[PROOFSTEP]
cases Y
[GOAL]
case none.none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
f : none ⟶ none
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        none = a →
          none = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) none))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            none = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : none ⟶ x) →
                  HEq f (𝟙 none) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id none = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) none))
                (_ : none = none) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ none) →
              none = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = none) f)
            (_ : some j = none) f)
        f (_ : none = none) (_ : none = none) (_ : HEq f f)
[PROOFSTEP]
cases f
[GOAL]
case none.some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
f : none ⟶ some val✝
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        none = a →
          some val✝ = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            some val✝ = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : none ⟶ x) →
                  HEq f (𝟙 none) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id none = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) none))
                (_ : none = some val✝) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ some val✝) →
              some val✝ = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = some val✝) f)
            (_ : some j = none) f)
        f (_ : none = none) (_ : some val✝ = some val✝) (_ : HEq f f)
[PROOFSTEP]
cases f
[GOAL]
case some.none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
f : some val✝ ⟶ none
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝ = a →
          none = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) none))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            none = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝ ⟶ x) →
                  HEq f (𝟙 (some val✝)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
                (_ : some val✝ = none) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ none) →
              none = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = none) f)
            (_ : some j = some val✝) f)
        f (_ : some val✝ = some val✝) (_ : none = none) (_ : HEq f f)
[PROOFSTEP]
cases f
[GOAL]
case some.some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝¹ val✝ : J
f : some val✝¹ ⟶ some val✝
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝¹) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝¹ = a →
          some val✝ = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝¹) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            some val✝ = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝¹) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝¹ ⟶ x) →
                  HEq f (𝟙 (some val✝¹)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝¹) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝¹) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝¹)))
                (_ : some val✝¹ = some val✝) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ some val✝) →
              some val✝ = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = some val✝) f)
            (_ : some j = some val✝¹) f)
        f (_ : some val✝¹ = some val✝¹) (_ : some val✝ = some val✝) (_ : HEq f f)
[PROOFSTEP]
cases f
[GOAL]
case none.none.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        none = a →
          none = a_1 →
            HEq (WidePullbackShape.Hom.id none) t →
              (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) none))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            none = x →
              HEq (WidePullbackShape.Hom.id none) (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : none ⟶ x) →
                  HEq f (𝟙 none) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id none = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) none))
                (_ : none = none) (WidePullbackShape.Hom.id none))
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ none) →
              none = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = none) f)
            (_ : some j = none) (WidePullbackShape.Hom.id none))
        (WidePullbackShape.Hom.id none) (_ : none = none) (_ : none = none)
        (_ : HEq (WidePullbackShape.Hom.id none) (WidePullbackShape.Hom.id none))
[PROOFSTEP]
rw [Category.id_comp, Category.comp_id]
[GOAL]
case some.none.term
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝ = a →
          none = a_1 →
            HEq (WidePullbackShape.Hom.term val✝) t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) none))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            none = x →
              HEq (WidePullbackShape.Hom.term val✝) (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝ ⟶ x) →
                  HEq f (𝟙 (some val✝)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
                (_ : some val✝ = none) (WidePullbackShape.Hom.term val✝))
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ none) →
              none = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = none) f)
            (_ : some j = some val✝) (WidePullbackShape.Hom.term val✝))
        (WidePullbackShape.Hom.term val✝) (_ : some val✝ = some val✝) (_ : none = none)
        (_ : HEq (WidePullbackShape.Hom.term val✝) (WidePullbackShape.Hom.term val✝))
[PROOFSTEP]
rw [Over.w, Category.id_comp]
[GOAL]
case some.some.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝ = a →
          some val✝ = a_1 →
            HEq (WidePullbackShape.Hom.id (some val✝)) t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            some val✝ = x →
              HEq (WidePullbackShape.Hom.id (some val✝)) (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝ ⟶ x) →
                  HEq f (𝟙 (some val✝)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
                (_ : some val✝ = some val✝) (WidePullbackShape.Hom.id (some val✝)))
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ some val✝) →
              some val✝ = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = some val✝) f)
            (_ : some j = some val✝) (WidePullbackShape.Hom.id (some val✝)))
        (WidePullbackShape.Hom.id (some val✝)) (_ : some val✝ = some val✝) (_ : some val✝ = some val✝)
        (_ : HEq (WidePullbackShape.Hom.id (some val✝)) (WidePullbackShape.Hom.id (some val✝)))
[PROOFSTEP]
rw [Category.id_comp, Category.comp_id]
[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : WidePullbackShape J
⊢ f.Hom.left ≫ NatTrans.app (conesEquivInverseObj B F Y✝).π j = NatTrans.app (conesEquivInverseObj B F X✝).π j
[PROOFSTEP]
cases' j with j
[GOAL]
case none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
⊢ f.Hom.left ≫ NatTrans.app (conesEquivInverseObj B F Y✝).π none = NatTrans.app (conesEquivInverseObj B F X✝).π none
[PROOFSTEP]
simp
[GOAL]
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ f.Hom.left ≫ NatTrans.app (conesEquivInverseObj B F Y✝).π (some j) =
    NatTrans.app (conesEquivInverseObj B F X✝).π (some j)
[PROOFSTEP]
dsimp
[GOAL]
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ f.Hom.left ≫ (NatTrans.app Y✝.π { as := j }).left = (NatTrans.app X✝.π { as := j }).left
[PROOFSTEP]
rw [← f.w ⟨j⟩]
[GOAL]
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ f.Hom.left ≫ (NatTrans.app Y✝.π { as := j }).left = (f.Hom ≫ NatTrans.app Y✝.π { as := j }).left
[PROOFSTEP]
rfl
[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone (widePullbackDiagramOfDiagramOver B F)
x✝² x✝¹ : Discrete J
X Y : J
x✝ : { as := X } ⟶ { as := Y }
f : { as := X }.as = { as := Y }.as
⊢ ((Functor.const (Discrete J)).obj (mk (NatTrans.app c.π none))).map { down := { down := f } } ≫
      (fun x =>
          match x with
          | { as := j } => homMk (NatTrans.app c.π (some j)))
        { as := Y } =
    (fun x =>
          match x with
          | { as := j } => homMk (NatTrans.app c.π (some j)))
        { as := X } ≫
      F.map { down := { down := f } }
[PROOFSTEP]
dsimp at f ⊢
[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone (widePullbackDiagramOfDiagramOver B F)
x✝² x✝¹ : Discrete J
X Y : J
x✝ : { as := X } ⟶ { as := Y }
f : X = Y
⊢ 𝟙 (mk (NatTrans.app c.π none)) ≫ homMk (NatTrans.app c.π (some Y)) =
    homMk (NatTrans.app c.π (some X)) ≫ F.map { down := { down := f } }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ ∀ (j : WidePullbackShape J),
    NatTrans.app ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π j =
      (Iso.mk (𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt)
            (𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt)).hom ≫
        NatTrans.app ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π j
[PROOFSTEP]
rintro (j | j)
[GOAL]
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ NatTrans.app ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π none =
    (Iso.mk (𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt)
          (𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt)).hom ≫
      NatTrans.app ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π none
[PROOFSTEP]
aesop_cat
[GOAL]
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
j : J
⊢ NatTrans.app ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π (some j) =
    (Iso.mk (𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt)
          (𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt)).hom ≫
      NatTrans.app ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π (some j)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
⊢ m = (fun s => homMk s.pt.hom) s
[PROOFSTEP]
simp only
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
⊢ m = homMk s.pt.hom
[PROOFSTEP]
ext
[GOAL]
case h
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
⊢ m.left = (homMk s.pt.hom).left
[PROOFSTEP]
rw [Over.homMk_left _]
[GOAL]
case h
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
⊢ m.left = s.pt.hom
[PROOFSTEP]
have := m.w
[GOAL]
case h
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
this :
  (𝟭 C).map m.left ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt.hom =
    s.pt.hom ≫ (Functor.fromPUnit B).map m.right
⊢ m.left = s.pt.hom
[PROOFSTEP]
dsimp at this 
[GOAL]
case h
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
this : m.left ≫ 𝟙 B = s.pt.hom ≫ 𝟙 B
⊢ m.left = s.pt.hom
[PROOFSTEP]
rwa [Category.comp_id, Category.comp_id] at this 
