-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.biconeMk_map : ∀ (J : Type v₁) [inst : CategoryTheory.SmallCategory J] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  {F : CategoryTheory.Functor J C} (c₁ c₂ : CategoryTheory.Limits.Cone F) {X Y : CategoryTheory.Bicone J} (f : X ⟶ Y),
  (CategoryTheory.biconeMk J c₁ c₂).map f =
    CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 x =>
      X = a →
        Y = a_1 →
          f ≍ x →
            ((CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) ⟶
              CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
      f
      (fun h =>
        Eq.ndrec (motive := fun {X} =>
          (f : X ⟶ Y) →
            Y = CategoryTheory.Bicone.left →
              f ≍ CategoryTheory.BiconeHom.left_id →
                ((CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) ⟶
                  CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : CategoryTheory.Bicone.left ⟶ Y) →
                f ≍ CategoryTheory.BiconeHom.left_id →
                  ((CategoryTheory.Bicone.casesOn CategoryTheory.Bicone.left c₁.pt c₂.pt fun j => F.obj j) ⟶
                    CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
              (fun f h =>
                CategoryTheory.CategoryStruct.id
                  (CategoryTheory.Bicone.casesOn CategoryTheory.Bicone.left c₁.pt c₂.pt fun j => F.obj j))
              ⋯ f)
          ⋯ f)
      (fun h =>
        Eq.ndrec (motive := fun {X} =>
          (f : X ⟶ Y) →
            Y = CategoryTheory.Bicone.right →
              f ≍ CategoryTheory.BiconeHom.right_id →
                ((CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) ⟶
                  CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : CategoryTheory.Bicone.right ⟶ Y) →
                f ≍ CategoryTheory.BiconeHom.right_id →
                  ((CategoryTheory.Bicone.casesOn CategoryTheory.Bicone.right c₁.pt c₂.pt fun j => F.obj j) ⟶
                    CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
              (fun f h =>
                CategoryTheory.CategoryStruct.id
                  (CategoryTheory.Bicone.casesOn CategoryTheory.Bicone.right c₁.pt c₂.pt fun j => F.obj j))
              ⋯ f)
          ⋯ f)
      (fun j h =>
        Eq.ndrec (motive := fun {X} =>
          (f : X ⟶ Y) →
            Y = CategoryTheory.Bicone.diagram j →
              f ≍ CategoryTheory.BiconeHom.left j →
                ((CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) ⟶
                  CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : CategoryTheory.Bicone.left ⟶ Y) →
                f ≍ CategoryTheory.BiconeHom.left j →
                  ((CategoryTheory.Bicone.casesOn CategoryTheory.Bicone.left c₁.pt c₂.pt fun j => F.obj j) ⟶
                    CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
              (fun f h => c₁.π.app j) ⋯ f)
          ⋯ f)
      (fun j h =>
        Eq.ndrec (motive := fun {X} =>
          (f : X ⟶ Y) →
            Y = CategoryTheory.Bicone.diagram j →
              f ≍ CategoryTheory.BiconeHom.right j →
                ((CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) ⟶
                  CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : CategoryTheory.Bicone.right ⟶ Y) →
                f ≍ CategoryTheory.BiconeHom.right j →
                  ((CategoryTheory.Bicone.casesOn CategoryTheory.Bicone.right c₁.pt c₂.pt fun j => F.obj j) ⟶
                    CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
              (fun f h => c₂.π.app j) ⋯ f)
          ⋯ f)
      (fun {j k} f_1 h =>
        Eq.ndrec (motive := fun {X} =>
          (f : X ⟶ Y) →
            Y = CategoryTheory.Bicone.diagram k →
              f ≍ CategoryTheory.BiconeHom.diagram f_1 →
                ((CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) ⟶
                  CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : CategoryTheory.Bicone.diagram j ⟶ Y) →
                f ≍ CategoryTheory.BiconeHom.diagram f_1 →
                  ((CategoryTheory.Bicone.casesOn (CategoryTheory.Bicone.diagram j) c₁.pt c₂.pt fun j => F.obj j) ⟶
                    CategoryTheory.Bicone.casesOn Y c₁.pt c₂.pt fun j => F.obj j))
              (fun f h => F.map f_1) ⋯ f)
          ⋯ f)
      ⋯ ⋯ ⋯