Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X✝ Y✝ Z✝ : Bicone J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      X✝ = a →
        Z✝ = a_1 →
          f ≫ g ≍ x → ((Bicone.casesOn X✝ c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ c₁.pt c₂.pt fun j ↦ F.obj j))
      (f ≫ g)
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) →
            Z✝ = Bicone.left →
              f ≍ BiconeHom.left_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
          ⋯ (f ≫ g))
      (fun h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) →
            Z✝ = Bicone.right →
              f ≍ BiconeHom.right_id →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
          ⋯ (f ≫ g))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) →
            Z✝ = Bicone.diagram j →
              f ≍ BiconeHom.left j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
          ⋯ (f ≫ g))
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) →
            Z✝ = Bicone.diagram j →
              f ≍ BiconeHom.right j →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
          ⋯ (f ≫ g))
      (fun {j k} f_1 h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) →
            Z✝ = Bicone.diagram k →
              f ≍ BiconeHom.diagram f_1 →
                ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ c₁.pt c₂.pt fun j ↦ F.obj j))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : Bicone.diagram j ⟶ Y) →
                f ≍ BiconeHom.diagram f_1 →
                  ((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 h ↦ F.map f_1) ⋯ f)
          ⋯ (f ≫ g))
      ⋯ ⋯ ⋯ =
    BiconeHom.casesOn (motive := fun a a_1 x ↦
        X✝ = a →
          Y✝ = a_1 →
            f ≍ x → ((Bicone.casesOn X✝ c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Y✝ c₁.pt c₂.pt fun j ↦ F.obj j))
        f
        (fun h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Y✝) →
              Y✝ = Bicone.left →
                f ≍ BiconeHom.left_id →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Y✝ 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)
            ⋯ f)
        (fun h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Y✝) →
              Y✝ = Bicone.right →
                f ≍ BiconeHom.right_id →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Y✝ 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)
            ⋯ f)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Y✝) →
              Y✝ = Bicone.diagram j →
                f ≍ BiconeHom.left j →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Y✝ 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)
            ⋯ f)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Y✝) →
              Y✝ = Bicone.diagram j →
                f ≍ BiconeHom.right j →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Y✝ 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)
            ⋯ f)
        (fun {j k} f_1 h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Y✝) →
              Y✝ = Bicone.diagram k →
                f ≍ BiconeHom.diagram f_1 →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Y✝ c₁.pt c₂.pt fun j ↦ F.obj j))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : Bicone.diagram j ⟶ Y) →
                  f ≍ BiconeHom.diagram f_1 →
                    ((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 h ↦ F.map f_1) ⋯ f)
            ⋯ f)
        ⋯ ⋯ ⋯ ≫
      BiconeHom.casesOn (motive := fun a a_1 x ↦
        Y✝ = a →
          Z✝ = a_1 →
            g ≍ x → ((Bicone.casesOn Y✝ c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ c₁.pt c₂.pt fun j ↦ F.obj j))
        g
        (fun h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) →
              Z✝ = Bicone.left →
                f ≍ BiconeHom.left_id →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
            ⋯ g)
        (fun h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) →
              Z✝ = Bicone.right →
                f ≍ BiconeHom.right_id →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
            ⋯ g)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) →
              Z✝ = Bicone.diagram j →
                f ≍ BiconeHom.left j →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
            ⋯ g)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) →
              Z✝ = Bicone.diagram j →
                f ≍ BiconeHom.right j →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
            ⋯ g)
        (fun {j k} f h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f_1 : X ⟶ Z✝) →
              Z✝ = Bicone.diagram k →
                f_1 ≍ BiconeHom.diagram f →
                  ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ 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)
            ⋯ g)
        ⋯ ⋯ ⋯

Tactic:
rcases f with (_ | _ | _ | _ | _)
    · exact (Category.id_comp _).symm
    · exact (Category.id_comp _).symm
    · cases g
      exact (Category.id_comp _).symm.trans (c₁.π.naturality _)
    · cases g
      exact (Category.id_comp _).symm.trans (c₂.π.naturality _)
    · cases g
      apply F.map_comp

Goal state after: