Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none.none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z 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 ↦ Hom.left (c.π.app { as := val })) none =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        none = a →
          none = a_1 →
            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 X h ↦
          Eq.rec (motive := fun x x_1 ↦
            none = x →
              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) →
                  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 ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) none)) ⋯ f)
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ none) →
              none = none →
                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) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯

pp: case none.some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z 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 ↦ Hom.left (c.π.app { as := val })) (some val✝) =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        none = a →
          some val✝ = a_1 →
            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 X h ↦
          Eq.rec (motive := fun x x_1 ↦
            some val✝ = x →
              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) →
                  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 ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) none)) ⋯ f)
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ some val✝) →
              some val✝ = none →
                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) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯

pp: case some.none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z 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 ↦ Hom.left (c.π.app { as := val })) none =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        some val✝ = a →
          none = a_1 →
            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 X h ↦
          Eq.rec (motive := fun x x_1 ↦
            none = x →
              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) →
                  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 ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝))) ⋯ f)
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ none) →
              none = none →
                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) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯

pp: case some.some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z 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 ↦ Hom.left (c.π.app { as := val })) (some val✝) =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝¹) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        some val✝¹ = a →
          some val✝ = a_1 →
            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 X h ↦
          Eq.rec (motive := fun x x_1 ↦
            some val✝ = x →
              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) →
                  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 ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝¹))) ⋯ f)
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ some val✝) →
              some val✝ = none →
                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) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯

Tactic:
<;>

Goal state after:
case none.none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z 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 ↦ Hom.left (c.π.app { as := val })) none =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        none = a →
          none = a_1 →
            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 X h ↦
          Eq.rec (motive := fun x x_1 ↦
            none = x →
              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) →
                  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 ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) none)) ⋯ f)
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ none) →
              none = none →
                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) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯

case none.some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z 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 ↦ Hom.left (c.π.app { as := val })) (some val✝) =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        none = a →
          some val✝ = a_1 →
            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 X h ↦
          Eq.rec (motive := fun x x_1 ↦
            some val✝ = x →
              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) →
                  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 ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) none)) ⋯ f)
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ some val✝) →
              some val✝ = none →
                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) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯

case some.none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z 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 ↦ Hom.left (c.π.app { as := val })) none =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        some val✝ = a →
          none = a_1 →
            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 X h ↦
          Eq.rec (motive := fun x x_1 ↦
            none = x →
              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) →
                  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 ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝))) ⋯ f)
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ none) →
              none = none →
                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) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯

case some.some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z 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 ↦ Hom.left (c.π.app { as := val })) (some val✝) =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝¹) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        some val✝¹ = a →
          some val✝ = a_1 →
            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 X h ↦
          Eq.rec (motive := fun x x_1 ↦
            some val✝ = x →
              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) →
                  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 ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝¹))) ⋯ f)
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ some val✝) →
              some val✝ = none →
                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) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯