Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
Z✝ : Bicone J
g : Bicone.left ⟶ Z✝
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      Bicone.left = a →
        Z✝ = a_1 →
          BiconeHom.left_id ≫ g ≍ x →
            ((Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Z✝ c₁.pt c₂.pt fun j ↦ F.obj j))
      (BiconeHom.left_id ≫ 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)
          ⋯ (BiconeHom.left_id ≫ 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)
          ⋯ (BiconeHom.left_id ≫ 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)
          ⋯ (BiconeHom.left_id ≫ 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)
          ⋯ (BiconeHom.left_id ≫ 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)
          ⋯ (BiconeHom.left_id ≫ g))
      ⋯ ⋯ ⋯ =
    BiconeHom.casesOn (motive := fun a a_1 x ↦
        Bicone.left = a →
          Bicone.left = a_1 →
            BiconeHom.left_id ≍ 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))
        BiconeHom.left_id
        (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)
            ⋯ BiconeHom.left_id)
        (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)
            ⋯ BiconeHom.left_id)
        (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)
            ⋯ BiconeHom.left_id)
        (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)
            ⋯ BiconeHom.left_id)
        (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)
            ⋯ BiconeHom.left_id)
        ⋯ ⋯ ⋯ ≫
      BiconeHom.casesOn (motive := fun a a_1 x ↦
        Bicone.left = a →
          Z✝ = a_1 →
            g ≍ x →
              ((Bicone.casesOn Bicone.left 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:
exact (Category.id_comp _).symm

Goal state after: