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 : Bicone J
⊢ BiconeHom.casesOn (motive := fun a a_1 x ↦
      X = a →
        X = a_1 →
          𝟙 X ≍ x → ((Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j))
      (𝟙 X)
      (fun h ↦
        Eq.ndrec (motive := fun {X_1} ↦
          (f : X_1 ⟶ X) →
            X = Bicone.left →
              f ≍ BiconeHom.left_id →
                ((Bicone.casesOn X_1 c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn X 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)
          ⋯ (𝟙 X))
      (fun h ↦
        Eq.ndrec (motive := fun {X_1} ↦
          (f : X_1 ⟶ X) →
            X = Bicone.right →
              f ≍ BiconeHom.right_id →
                ((Bicone.casesOn X_1 c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn X 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)
          ⋯ (𝟙 X))
      (fun j h ↦
        Eq.ndrec (motive := fun {X_1} ↦
          (f : X_1 ⟶ X) →
            X = Bicone.diagram j →
              f ≍ BiconeHom.left j →
                ((Bicone.casesOn X_1 c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn X 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)
          ⋯ (𝟙 X))
      (fun j h ↦
        Eq.ndrec (motive := fun {X_1} ↦
          (f : X_1 ⟶ X) →
            X = Bicone.diagram j →
              f ≍ BiconeHom.right j →
                ((Bicone.casesOn X_1 c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn X 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)
          ⋯ (𝟙 X))
      (fun {j k} f h ↦
        Eq.ndrec (motive := fun {X_1} ↦
          (f_1 : X_1 ⟶ X) →
            X = Bicone.diagram k →
              f_1 ≍ BiconeHom.diagram f →
                ((Bicone.casesOn X_1 c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn X 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)
          ⋯ (𝟙 X))
      ⋯ ⋯ ⋯ =
    𝟙 (Bicone.casesOn X c₁.pt c₂.pt fun j ↦ F.obj j)

Tactic:
cases X <;> simp

Goal state after: