Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      Bicone.left = a →
        Bicone.left = a_1 →
          𝟙 Bicone.left ≍ x →
            ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
              Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
      (𝟙 Bicone.left)
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.left) →
            Bicone.left = Bicone.left →
              f ≍ BiconeHom.left_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left_id →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 Bicone.left))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.left) →
            Bicone.left = Bicone.right →
              f ≍ BiconeHom.right_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right_id →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 Bicone.left))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.left) →
            Bicone.left = Bicone.diagram j →
              f ≍ BiconeHom.left j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left j →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₁.π.app j) ⋯ f)
          ⋯ (𝟙 Bicone.left))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.left) →
            Bicone.left = Bicone.diagram j →
              f ≍ BiconeHom.right j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right j →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₂.π.app j) ⋯ f)
          ⋯ (𝟙 Bicone.left))
      (fun {j k} f h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f_1 : X ⟶ Bicone.left) →
            Bicone.left = Bicone.diagram k →
              f_1 ≍ BiconeHom.diagram f →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f_1 h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f_2 : Bicone.diagram j ⟶ Y) →
                f_2 ≍ BiconeHom.diagram f →
                  ((Bicone.casesOn (Bicone.diagram j) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f_2 h ↦ F.map f) ⋯ f_1)
          ⋯ (𝟙 Bicone.left))
      ⋯ ⋯ ⋯ =
    𝟙 (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j)

pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      Bicone.right = a →
        Bicone.right = a_1 →
          𝟙 Bicone.right ≍ x →
            ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
              Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
      (𝟙 Bicone.right)
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.right) →
            Bicone.right = Bicone.left →
              f ≍ BiconeHom.left_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left_id →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 Bicone.right))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.right) →
            Bicone.right = Bicone.right →
              f ≍ BiconeHom.right_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right_id →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 Bicone.right))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.right) →
            Bicone.right = Bicone.diagram j →
              f ≍ BiconeHom.left j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left j →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₁.π.app j) ⋯ f)
          ⋯ (𝟙 Bicone.right))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.right) →
            Bicone.right = Bicone.diagram j →
              f ≍ BiconeHom.right j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right j →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₂.π.app j) ⋯ f)
          ⋯ (𝟙 Bicone.right))
      (fun {j k} f h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f_1 : X ⟶ Bicone.right) →
            Bicone.right = Bicone.diagram k →
              f_1 ≍ BiconeHom.diagram f →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f_1 h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f_2 : Bicone.diagram j ⟶ Y) →
                f_2 ≍ BiconeHom.diagram f →
                  ((Bicone.casesOn (Bicone.diagram j) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f_2 h ↦ F.map f) ⋯ f_1)
          ⋯ (𝟙 Bicone.right))
      ⋯ ⋯ ⋯ =
    𝟙 (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j)

pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
val✝ : J
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      Bicone.diagram val✝ = a →
        Bicone.diagram val✝ = a_1 →
          𝟙 (Bicone.diagram val✝) ≍ x →
            ((Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
              Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
      (𝟙 (Bicone.diagram val✝))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.left →
              f ≍ BiconeHom.left_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left_id →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.right →
              f ≍ BiconeHom.right_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right_id →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.diagram j →
              f ≍ BiconeHom.left j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left j →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₁.π.app j) ⋯ f)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.diagram j →
              f ≍ BiconeHom.right j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right j →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₂.π.app j) ⋯ f)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      (fun {j k} f h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f_1 : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.diagram k →
              f_1 ≍ BiconeHom.diagram f →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f_1 h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f_2 : Bicone.diagram j ⟶ Y) →
                f_2 ≍ BiconeHom.diagram f →
                  ((Bicone.casesOn (Bicone.diagram j) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f_2 h ↦ F.map f) ⋯ f_1)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      ⋯ ⋯ ⋯ =
    𝟙 (Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j)

Tactic:
<;>

Goal state after:
case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      Bicone.left = a →
        Bicone.left = a_1 →
          𝟙 Bicone.left ≍ x →
            ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
              Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
      (𝟙 Bicone.left)
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.left) →
            Bicone.left = Bicone.left →
              f ≍ BiconeHom.left_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left_id →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 Bicone.left))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.left) →
            Bicone.left = Bicone.right →
              f ≍ BiconeHom.right_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right_id →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 Bicone.left))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.left) →
            Bicone.left = Bicone.diagram j →
              f ≍ BiconeHom.left j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left j →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₁.π.app j) ⋯ f)
          ⋯ (𝟙 Bicone.left))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.left) →
            Bicone.left = Bicone.diagram j →
              f ≍ BiconeHom.right j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right j →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₂.π.app j) ⋯ f)
          ⋯ (𝟙 Bicone.left))
      (fun {j k} f h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f_1 : X ⟶ Bicone.left) →
            Bicone.left = Bicone.diagram k →
              f_1 ≍ BiconeHom.diagram f →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f_1 h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f_2 : Bicone.diagram j ⟶ Y) →
                f_2 ≍ BiconeHom.diagram f →
                  ((Bicone.casesOn (Bicone.diagram j) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f_2 h ↦ F.map f) ⋯ f_1)
          ⋯ (𝟙 Bicone.left))
      ⋯ ⋯ ⋯ =
    𝟙 (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j)

case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      Bicone.right = a →
        Bicone.right = a_1 →
          𝟙 Bicone.right ≍ x →
            ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
              Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
      (𝟙 Bicone.right)
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.right) →
            Bicone.right = Bicone.left →
              f ≍ BiconeHom.left_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left_id →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 Bicone.right))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.right) →
            Bicone.right = Bicone.right →
              f ≍ BiconeHom.right_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right_id →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 Bicone.right))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.right) →
            Bicone.right = Bicone.diagram j →
              f ≍ BiconeHom.left j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left j →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₁.π.app j) ⋯ f)
          ⋯ (𝟙 Bicone.right))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.right) →
            Bicone.right = Bicone.diagram j →
              f ≍ BiconeHom.right j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right j →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₂.π.app j) ⋯ f)
          ⋯ (𝟙 Bicone.right))
      (fun {j k} f h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f_1 : X ⟶ Bicone.right) →
            Bicone.right = Bicone.diagram k →
              f_1 ≍ BiconeHom.diagram f →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f_1 h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f_2 : Bicone.diagram j ⟶ Y) →
                f_2 ≍ BiconeHom.diagram f →
                  ((Bicone.casesOn (Bicone.diagram j) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f_2 h ↦ F.map f) ⋯ f_1)
          ⋯ (𝟙 Bicone.right))
      ⋯ ⋯ ⋯ =
    𝟙 (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j)

case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
val✝ : J
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      Bicone.diagram val✝ = a →
        Bicone.diagram val✝ = a_1 →
          𝟙 (Bicone.diagram val✝) ≍ x →
            ((Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
              Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
      (𝟙 (Bicone.diagram val✝))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.left →
              f ≍ BiconeHom.left_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left_id →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.right →
              f ≍ BiconeHom.right_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right_id →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ 𝟙 (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j)) ⋯ f)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.diagram j →
              f ≍ BiconeHom.left j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.left ⟶ Y) →
                f ≍ BiconeHom.left j →
                  ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₁.π.app j) ⋯ f)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.diagram j →
              f ≍ BiconeHom.right j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.right ⟶ Y) →
                f ≍ BiconeHom.right j →
                  ((Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f h ↦ c₂.π.app j) ⋯ f)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      (fun {j k} f h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f_1 : X ⟶ Bicone.diagram val✝) →
            Bicone.diagram val✝ = Bicone.diagram k →
              f_1 ≍ BiconeHom.diagram f →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                  Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f_1 h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f_2 : Bicone.diagram j ⟶ Y) →
                f_2 ≍ BiconeHom.diagram f →
                  ((Bicone.casesOn (Bicone.diagram j) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
                    Bicone.casesOn Y c₁.pt c₂.pt fun j ↦ F.obj j))
              (fun f_2 h ↦ F.map f) ⋯ f_1)
          ⋯ (𝟙 (Bicone.diagram val✝)))
      ⋯ ⋯ ⋯ =
    𝟙 (Bicone.casesOn (Bicone.diagram val✝) c₁.pt c₂.pt fun j ↦ F.obj j)