-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
c : Cone F
none :
  Eq.{v + 1} (α :=
    c.pt.left ⟶
      Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
    (Option.rec (motive := fun (x : WidePullbackShape J) ↦
        c.pt.left ⟶
          Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
            (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
        c.pt.hom (fun (val : J) ↦ Hom.left (c.π.app { as := val })) Option.none :
      c.pt.left ⟶
        Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
    (CategoryStruct.comp (Y :=
        Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
        (Option.rec (motive := fun (x : WidePullbackShape J) ↦
          c.pt.left ⟶
            Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
              (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
          c.pt.hom (fun (val : J) ↦ Hom.left (c.π.app { as := val })) Option.none)
        (@WidePullbackShape.Hom.rec _
          (fun (a a_1 : WidePullbackShape J) (x : a.Hom a_1) ↦
            (h : Option.none = a) →
              (h : Option.none = a_1) →
                (h :
                    HEq (α := Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)
                      (WidePullbackShape.Hom.id Option.none) x) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                      C)
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                      C))
          (fun (X : WidePullbackShape J) (h : Option.none = X) ↦
            Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : Option.none = x) ↦
              (h : Option.none = x) →
                (h :
                    HEq (α := Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)
                      (WidePullbackShape.Hom.id Option.none) (β := x.Hom x) (𝟙 x)) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                      C)
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                      C))
              (fun (h : Eq.{w + 1} (α := WidePullbackShape J) Option.none Option.none) ↦
                Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : Option.none = x) ↦
                  (f : Option.none ⟶ x) →
                    (h :
                        HEq f (β := WidePullbackShape.Hom (J := J) Option.none Option.none)
                          (𝟙 Option.none : Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                            (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                          C)
                        (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                            (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x :
                          C))
                  (fun (f : Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)
                      (h :
                        HEq f (β := WidePullbackShape.Hom (J := J) Option.none Option.none)
                          (𝟙 Option.none : Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)) ↦
                    𝟙
                      (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none))
                  ⋯ (WidePullbackShape.Hom.id Option.none))
              h)
          (fun (j : J) (h : Option.none = some j) ↦
            Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : some j = x) ↦
              (f : x ⟶ Option.none) →
                (h : Eq.{w + 1} (α := WidePullbackShape J) Option.none Option.none) →
                  (h : f ≍ WidePullbackShape.Hom.term j) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x :
                        C)
                      (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                        C))
              (fun (f : some j ⟶ Option.none) (h : Eq.{w + 1} (α := WidePullbackShape J) Option.none Option.none) ↦
                Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : Option.none = x) ↦
                  (f : some j ⟶ x) →
                    (h : f ≍ WidePullbackShape.Hom.term j) →
                      (F.obj { as := j : Discrete J }).left ⟶
                        Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
                  (fun (f : some j ⟶ Option.none) (h : f ≍ WidePullbackShape.Hom.term j) ↦ (F.obj { as := j }).hom) ⋯ f)
              ⋯ (WidePullbackShape.Hom.id Option.none))
          Option.none _ (WidePullbackShape.Hom.id Option.none) ⋯ ⋯ ⋯) :
      c.pt.left ⟶
        Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
none₁ none₂ :
  Eq.{v + 1} (α :=
    c.pt.left ⟶
      Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
    (Option.rec (motive := fun (x : WidePullbackShape J) ↦
        c.pt.left ⟶
          Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
            (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
        c.pt.hom (fun (val : J) ↦ Hom.left (c.π.app { as := val })) Option.none :
      c.pt.left ⟶
        Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
    (Option.rec (motive := fun (x : WidePullbackShape J) ↦
        c.pt.left ⟶
          Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
            (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
        c.pt.hom (fun (val : J) ↦ Hom.left (c.π.app { as := val })) Option.none :
      c.pt.left ⟶
        Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
⊢ Eq.{v + 1} (α :=
    c.pt.left ⟶
      Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
    (𝟙 c.pt.left ≫
      Option.rec (motive := fun (x : WidePullbackShape J) ↦
        c.pt.left ⟶
          Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
            (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
        c.pt.hom (fun (val : J) ↦ Hom.left (c.π.app { as := val })) Option.none)
    (CategoryStruct.comp (Y :=
      Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none)
      (Option.rec (motive := fun (x : WidePullbackShape J) ↦
        c.pt.left ⟶
          Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
            (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
        c.pt.hom (fun (val : J) ↦ Hom.left (c.π.app { as := val })) Option.none)
      (@WidePullbackShape.Hom.rec _
        (fun (a a_1 : WidePullbackShape J) (x : a.Hom a_1) ↦
          (h : Option.none = a) →
            (h : Option.none = a_1) →
              (h :
                  HEq (α := Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)
                    (WidePullbackShape.Hom.id Option.none) x) →
                Quiver.Hom.{v, u} (V := C)
                  (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                    C)
                  (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                    C))
        (fun (X : WidePullbackShape J) (h : Option.none = X) ↦
          Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : Option.none = x) ↦
            (h : Option.none = x) →
              (h :
                  HEq (α := Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)
                    (WidePullbackShape.Hom.id Option.none) (β := x.Hom x) (𝟙 x)) →
                Quiver.Hom.{v, u} (V := C)
                  (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                    C)
                  (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                    C))
            (fun (h : Eq.{w + 1} (α := WidePullbackShape J) Option.none Option.none) ↦
              Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : Option.none = x) ↦
                (f : Option.none ⟶ x) →
                  (h :
                      HEq f (β := WidePullbackShape.Hom (J := J) Option.none Option.none)
                        (𝟙 Option.none : Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                        C)
                      (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x :
                        C))
                (fun (f : Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)
                    (h :
                      HEq f (β := WidePullbackShape.Hom (J := J) Option.none Option.none)
                        (𝟙 Option.none : Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)) ↦
                  𝟙
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none))
                ⋯ (WidePullbackShape.Hom.id Option.none))
            h)
        (fun (j : J) (h : Option.none = some j) ↦
          Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : some j = x) ↦
            (f : x ⟶ Option.none) →
              (h : Eq.{w + 1} (α := WidePullbackShape J) Option.none Option.none) →
                (h : f ≍ WidePullbackShape.Hom.term j) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x :
                      C)
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Option.none :
                      C))
            (fun (f : some j ⟶ Option.none) (h : Eq.{w + 1} (α := WidePullbackShape J) Option.none Option.none) ↦
              Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : Option.none = x) ↦
                (f : some j ⟶ x) →
                  (h : f ≍ WidePullbackShape.Hom.term j) →
                    (F.obj { as := j : Discrete J }).left ⟶
                      Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
                (fun (f : some j ⟶ Option.none) (h : f ≍ WidePullbackShape.Hom.term j) ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ (WidePullbackShape.Hom.id Option.none))
        Option.none _ (WidePullbackShape.Hom.id Option.none) ⋯ ⋯ ⋯))

Tactic:
rw [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp