[GOAL]
J : Type u₁
inst✝ : Fintype J
j : Bicone J
⊢ j ∈ List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems
[PROOFSTEP]
cases j
[GOAL]
case left
J : Type u₁
inst✝ : Fintype J
⊢ Bicone.left ∈ List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems
[PROOFSTEP]
simp
[GOAL]
case right
J : Type u₁
inst✝ : Fintype J
⊢ Bicone.right ∈ List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems
[PROOFSTEP]
simp
[GOAL]
case diagram
J : Type u₁
inst✝ : Fintype J
val✝ : J
⊢ Bicone.diagram val✝ ∈ List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems
[PROOFSTEP]
simp
[GOAL]
case diagram
J : Type u₁
inst✝ : Fintype J
val✝ : J
⊢ val✝ ∈ Fintype.elems
[PROOFSTEP]
apply Fintype.complete
[GOAL]
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom J j k
⊢ Decidable (f = g)
[PROOFSTEP]
cases f
[GOAL]
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
g : BiconeHom J Bicone.left Bicone.left
⊢ Decidable (left_id = g)
[PROOFSTEP]
cases g
[GOAL]
case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
g : BiconeHom J Bicone.right Bicone.right
⊢ Decidable (right_id = g)
[PROOFSTEP]
cases g
[GOAL]
case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
g : BiconeHom J Bicone.left (Bicone.diagram j✝)
⊢ Decidable (left j✝ = g)
[PROOFSTEP]
cases g
[GOAL]
case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
g : BiconeHom J Bicone.right (Bicone.diagram j✝)
⊢ Decidable (right j✝ = g)
[PROOFSTEP]
cases g
[GOAL]
case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram j✝) (Bicone.diagram k✝)
⊢ Decidable (diagram f✝ = g)
[PROOFSTEP]
cases g
[GOAL]
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (left_id = left_id)
[PROOFSTEP]
simp
[GOAL]
case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (right_id = right_id)
[PROOFSTEP]
simp
[GOAL]
case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (left j✝ = left j✝)
[PROOFSTEP]
simp
[GOAL]
case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (right j✝ = right j✝)
[PROOFSTEP]
simp
[GOAL]
case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (diagram f✝¹ = diagram f✝)
[PROOFSTEP]
simp
[GOAL]
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable True
[PROOFSTEP]
infer_instance
[GOAL]
case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable True
[PROOFSTEP]
infer_instance
[GOAL]
case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable True
[PROOFSTEP]
infer_instance
[GOAL]
case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable True
[PROOFSTEP]
infer_instance
[GOAL]
case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (f✝¹ = f✝)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type u₁
inst✝ : Category.{v₁, u₁} J
X✝ Y✝ Z✝ : Bicone J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ X✝ ⟶ Z✝
[PROOFSTEP]
rcases f with (_ | _ | _ | _ | f)
[GOAL]
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : Bicone.left ⟶ Z✝
⊢ Bicone.left ⟶ Z✝
[PROOFSTEP]
exact g
[GOAL]
case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : Bicone.right ⟶ Z✝
⊢ Bicone.right ⟶ Z✝
[PROOFSTEP]
exact g
[GOAL]
case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : Bicone.diagram j✝ ⟶ Z✝
⊢ Bicone.left ⟶ Z✝
[PROOFSTEP]
cases g
[GOAL]
case left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ Bicone.left ⟶ Bicone.diagram k✝
[PROOFSTEP]
apply BiconeHom.left
[GOAL]
case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : Bicone.diagram j✝ ⟶ Z✝
⊢ Bicone.right ⟶ Z✝
[PROOFSTEP]
cases g
[GOAL]
case right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ Bicone.right ⟶ Bicone.diagram k✝
[PROOFSTEP]
apply BiconeHom.right
[GOAL]
case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : Bicone.diagram k✝ ⟶ Z✝
⊢ Bicone.diagram j✝ ⟶ Z✝
[PROOFSTEP]
rcases g with (_ | _ | _ | _ | g)
[GOAL]
case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝¹ : J
f : j✝ ⟶ k✝¹
k✝ : J
g : k✝¹ ⟶ k✝
⊢ Bicone.diagram j✝ ⟶ Bicone.diagram k✝
[PROOFSTEP]
exact BiconeHom.diagram (f ≫ g)
[GOAL]
J : Type u₁
inst✝ : Category.{v₁, u₁} J
X✝ Y✝ : Bicone J
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f
[PROOFSTEP]
cases f
[GOAL]
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ 𝟙 Bicone.left ≫ BiconeHom.left_id = BiconeHom.left_id
[PROOFSTEP]
simp
[GOAL]
case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ 𝟙 Bicone.right ≫ BiconeHom.right_id = BiconeHom.right_id
[PROOFSTEP]
simp
[GOAL]
case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ 𝟙 Bicone.left ≫ BiconeHom.left j✝ = BiconeHom.left j✝
[PROOFSTEP]
simp
[GOAL]
case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ 𝟙 Bicone.right ≫ BiconeHom.right j✝ = BiconeHom.right j✝
[PROOFSTEP]
simp
[GOAL]
case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ 𝟙 (Bicone.diagram j✝) ≫ BiconeHom.diagram f✝ = BiconeHom.diagram f✝
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝ : Category.{v₁, u₁} J
X✝ Y✝ : Bicone J
f : X✝ ⟶ Y✝
⊢ f ≫ 𝟙 Y✝ = f
[PROOFSTEP]
cases f
[GOAL]
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ BiconeHom.left_id ≫ 𝟙 Bicone.left = BiconeHom.left_id
[PROOFSTEP]
simp
[GOAL]
case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ BiconeHom.right_id ≫ 𝟙 Bicone.right = BiconeHom.right_id
[PROOFSTEP]
simp
[GOAL]
case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ BiconeHom.left j✝ ≫ 𝟙 (Bicone.diagram j✝) = BiconeHom.left j✝
[PROOFSTEP]
simp
[GOAL]
case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ BiconeHom.right j✝ ≫ 𝟙 (Bicone.diagram j✝) = BiconeHom.right j✝
[PROOFSTEP]
simp
[GOAL]
case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ BiconeHom.diagram f✝ ≫ 𝟙 (Bicone.diagram k✝) = BiconeHom.diagram f✝
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝ : Category.{v₁, u₁} J
W✝ X✝ Y✝ Z✝ : Bicone J
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases f
[GOAL]
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.left ⟶ Y✝
⊢ (BiconeHom.left_id ≫ g) ≫ h = BiconeHom.left_id ≫ g ≫ h
[PROOFSTEP]
cases g
[GOAL]
case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.right ⟶ Y✝
⊢ (BiconeHom.right_id ≫ g) ≫ h = BiconeHom.right_id ≫ g ≫ h
[PROOFSTEP]
cases g
[GOAL]
case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.left j✝ ≫ g) ≫ h = BiconeHom.left j✝ ≫ g ≫ h
[PROOFSTEP]
cases g
[GOAL]
case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.right j✝ ≫ g) ≫ h = BiconeHom.right j✝ ≫ g ≫ h
[PROOFSTEP]
cases g
[GOAL]
case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : Bicone.diagram k✝ ⟶ Y✝
⊢ (BiconeHom.diagram f✝ ≫ g) ≫ h = BiconeHom.diagram f✝ ≫ g ≫ h
[PROOFSTEP]
cases g
[GOAL]
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.left ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h = BiconeHom.left_id ≫ BiconeHom.left_id ≫ h
[PROOFSTEP]
cases h
[GOAL]
case left_id.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left j✝) ≫ h = BiconeHom.left_id ≫ BiconeHom.left j✝ ≫ h
[PROOFSTEP]
cases h
[GOAL]
case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.right ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h = BiconeHom.right_id ≫ BiconeHom.right_id ≫ h
[PROOFSTEP]
cases h
[GOAL]
case right_id.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right j✝) ≫ h = BiconeHom.right_id ≫ BiconeHom.right j✝ ≫ h
[PROOFSTEP]
cases h
[GOAL]
case left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.left j✝ ≫ BiconeHom.diagram f✝ ≫ h
[PROOFSTEP]
cases h
[GOAL]
case right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.right j✝ ≫ BiconeHom.diagram f✝ ≫ h
[PROOFSTEP]
cases h
[GOAL]
case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝ ≫ h
[PROOFSTEP]
cases h
[GOAL]
case left_id.left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left_id =
    BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left_id
[PROOFSTEP]
simp
[GOAL]
case left_id.left_id.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left j✝ =
    BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left j✝
[PROOFSTEP]
simp
[GOAL]
case left_id.left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left j✝) ≫ BiconeHom.diagram f✝ =
    BiconeHom.left_id ≫ BiconeHom.left j✝ ≫ BiconeHom.diagram f✝
[PROOFSTEP]
simp
[GOAL]
case right_id.right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right_id =
    BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right_id
[PROOFSTEP]
simp
[GOAL]
case right_id.right_id.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right j✝ =
    BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right j✝
[PROOFSTEP]
simp
[GOAL]
case right_id.right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right j✝) ≫ BiconeHom.diagram f✝ =
    BiconeHom.right_id ≫ BiconeHom.right j✝ ≫ BiconeHom.diagram f✝
[PROOFSTEP]
simp
[GOAL]
case left.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.left j✝ ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝
[PROOFSTEP]
simp
[GOAL]
case right.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.right j✝ ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝
[PROOFSTEP]
simp
[GOAL]
case diagram.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝² : J
f✝² : j✝ ⟶ k✝²
k✝¹ : J
f✝¹ : k✝² ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.diagram f✝² ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.diagram f✝² ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝
[PROOFSTEP]
simp
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X✝ Y✝ : Bicone J
f : X✝ ⟶ Y✝
⊢ (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X✝ ⟶
    (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y✝
[PROOFSTEP]
rcases f with (_ | _ | _ | _ | f)
[GOAL]
case left_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
    (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case right_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
    (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
    (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j✝)
[PROOFSTEP]
exact c₁.π.app _
[GOAL]
case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
    (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j✝)
[PROOFSTEP]
exact c₂.π.app _
[GOAL]
case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j✝) ⟶
    (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram k✝)
[PROOFSTEP]
exact F.map f
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X : Bicone J
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.obj
        X)
[PROOFSTEP]
cases X
[GOAL]
case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (𝟙 Bicone.left) =
    𝟙
      ({ obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.obj
        Bicone.left)
[PROOFSTEP]
simp
[GOAL]
case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (𝟙 Bicone.right) =
    𝟙
      ({ obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.obj
        Bicone.right)
[PROOFSTEP]
simp
[GOAL]
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
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (𝟙 (Bicone.diagram val✝)) =
    𝟙
      ({ obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.obj
        (Bicone.diagram val✝))
[PROOFSTEP]
simp
[GOAL]
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✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (f ≫ g) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        f ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
rcases f with (_ | _ | _ | _ | _)
[GOAL]
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✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (BiconeHom.left_id ≫ g) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        BiconeHom.left_id ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
exact (Category.id_comp _).symm
[GOAL]
case right_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.right ⟶ Z✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (BiconeHom.right_id ≫ g) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        BiconeHom.right_id ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
exact (Category.id_comp _).symm
[GOAL]
case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
Z✝ : Bicone J
j✝ : J
g : Bicone.diagram j✝ ⟶ Z✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (BiconeHom.left j✝ ≫ g) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.left j✝) ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
cases g
[GOAL]
case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.left j✝) ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.diagram f✝)
[PROOFSTEP]
exact (Category.id_comp _).symm.trans (c₁.π.naturality _)
[GOAL]
case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
Z✝ : Bicone J
j✝ : J
g : Bicone.diagram j✝ ⟶ Z✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (BiconeHom.right j✝ ≫ g) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.right j✝) ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
cases g
[GOAL]
case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.right j✝) ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.diagram f✝)
[PROOFSTEP]
exact (Category.id_comp _).symm.trans (c₂.π.naturality _)
[GOAL]
case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : Bicone.diagram k✝ ⟶ Z✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (BiconeHom.diagram f✝ ≫ g) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.diagram f✝) ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
cases g
[GOAL]
case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
          map := fun {X Y} f =>
            BiconeHom.casesOn (motive := fun a a_1 x =>
              X = a →
                Y = a_1 →
                  HEq f x →
                    ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                      (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
              f
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.left →
                      HEq f BiconeHom.left_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.left_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                      (_ : Bicone.left = Y) f)
                  (_ : Bicone.left = X) f)
              (fun h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.right →
                      HEq f BiconeHom.right_id →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h =>
                        (_ : BiconeHom.right_id = f) ▸
                          𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                      (_ : Bicone.right = Y) f)
                  (_ : Bicone.right = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.left j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.left ⟶ Y) →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.left = X) f)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram j →
                      HEq f (BiconeHom.right j) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.right ⟶ Y) →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                  (_ : Bicone.right = X) f)
              (fun {j k} f_1 h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = Bicone.diagram k →
                      HEq f (BiconeHom.diagram f_1) →
                        ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                          (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : Bicone.diagram j ⟶ Y) →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                      (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                  (_ : Bicone.diagram j = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝) =
    { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.diagram f✝¹) ≫
      { obj := fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j,
            map := fun {X Y} f =>
              BiconeHom.casesOn (motive := fun a a_1 x =>
                X = a →
                  Y = a_1 →
                    HEq f x →
                      ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                        (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                f
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.left →
                        HEq f BiconeHom.left_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f BiconeHom.left_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.left_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left))
                        (_ : Bicone.left = Y) f)
                    (_ : Bicone.left = X) f)
                (fun h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.right →
                        HEq f BiconeHom.right_id →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f BiconeHom.right_id →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h =>
                          (_ : BiconeHom.right_id = f) ▸
                            𝟙 ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right))
                        (_ : Bicone.right = Y) f)
                    (_ : Bicone.right = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.left j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.left ⟶ Y) →
                          HEq f (BiconeHom.left j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.left ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.left j = f) ▸ NatTrans.app c₁.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.left = X) f)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram j →
                        HEq f (BiconeHom.right j) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.right ⟶ Y) →
                          HEq f (BiconeHom.right j) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Bicone.right ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.right j = f) ▸ NatTrans.app c₂.π j) (_ : Bicone.diagram j = Y) f)
                    (_ : Bicone.right = X) f)
                (fun {j k} f_1 h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = Bicone.diagram k →
                        HEq f (BiconeHom.diagram f_1) →
                          ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶
                            (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : Bicone.diagram j ⟶ Y) →
                          HEq f (BiconeHom.diagram f_1) →
                            ((fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (Bicone.diagram j) ⟶
                              (fun X => Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y))
                        (fun f h => (_ : BiconeHom.diagram f_1 = f) ▸ F.map f_1) (_ : Bicone.diagram k = Y) f)
                    (_ : Bicone.diagram j = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (BiconeHom.diagram f✝)
[PROOFSTEP]
apply F.map_comp
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
j k : Bicone J
⊢ Fintype (j ⟶ k)
[PROOFSTEP]
cases j
[GOAL]
case left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
⊢ Fintype (Bicone.left ⟶ k)
[PROOFSTEP]
cases k
[GOAL]
case right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
⊢ Fintype (Bicone.right ⟶ k)
[PROOFSTEP]
cases k
[GOAL]
case diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ k)
[PROOFSTEP]
cases k
[GOAL]
case left.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.left)
[PROOFSTEP]
exact
  { elems := { BiconeHom.left_id }
    complete := fun f => by cases f; simp }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.left ⟶ Bicone.left
⊢ f ∈ {BiconeHom.left_id}
[PROOFSTEP]
cases f
[GOAL]
case left_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.left_id ∈ {BiconeHom.left_id}
[PROOFSTEP]
simp
[GOAL]
case left.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.left ⟶ Bicone.right)
[PROOFSTEP]
exact
  { elems := ∅
    complete := fun f => by cases f }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.left ⟶ Bicone.right
⊢ f ∈ ∅
[PROOFSTEP]
cases f
[GOAL]
case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val✝)
[PROOFSTEP]
exact
  { elems := {BiconeHom.left _}
    complete := fun f => by cases f; simp }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.left ⟶ Bicone.diagram val✝
⊢ f ∈ {BiconeHom.left val✝}
[PROOFSTEP]
cases f
[GOAL]
case left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.left val✝ ∈ {BiconeHom.left val✝}
[PROOFSTEP]
simp
[GOAL]
case right.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.left)
[PROOFSTEP]
exact
  { elems := ∅
    complete := fun f => by cases f }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.right ⟶ Bicone.left
⊢ f ∈ ∅
[PROOFSTEP]
cases f
[GOAL]
case right.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ Fintype (Bicone.right ⟶ Bicone.right)
[PROOFSTEP]
exact
  { elems := { BiconeHom.right_id }
    complete := fun f => by cases f; simp }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.right ⟶ Bicone.right
⊢ f ∈ {BiconeHom.right_id}
[PROOFSTEP]
cases f
[GOAL]
case right_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.right_id ∈ {BiconeHom.right_id}
[PROOFSTEP]
simp
[GOAL]
case right.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val✝)
[PROOFSTEP]
exact
  { elems := {BiconeHom.right _}
    complete := fun f => by cases f; simp }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.right ⟶ Bicone.diagram val✝
⊢ f ∈ {BiconeHom.right val✝}
[PROOFSTEP]
cases f
[GOAL]
case right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.right val✝ ∈ {BiconeHom.right val✝}
[PROOFSTEP]
simp
[GOAL]
case diagram.left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.left)
[PROOFSTEP]
exact
  { elems := ∅
    complete := fun f => by cases f }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.diagram val✝ ⟶ Bicone.left
⊢ f ∈ ∅
[PROOFSTEP]
cases f
[GOAL]
case diagram.right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ Bicone.right)
[PROOFSTEP]
exact
  { elems := ∅
    complete := fun f => by cases f }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.diagram val✝ ⟶ Bicone.right
⊢ f ∈ ∅
[PROOFSTEP]
cases f
[GOAL]
case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)
[PROOFSTEP]
exact
  { elems := Finset.image BiconeHom.diagram Fintype.elems
    complete := fun f => by
      rcases f with (_ | _ | _ | _ | f)
      simp only [Finset.mem_image]
      use f
      simpa using Fintype.complete _ }
[GOAL]
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
f : Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝
⊢ f ∈ Finset.image BiconeHom.diagram Fintype.elems
[PROOFSTEP]
rcases f with (_ | _ | _ | _ | f)
[GOAL]
case diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
f : val✝¹ ⟶ val✝
⊢ BiconeHom.diagram f ∈ Finset.image BiconeHom.diagram Fintype.elems
[PROOFSTEP]
simp only [Finset.mem_image]
[GOAL]
case diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
f : val✝¹ ⟶ val✝
⊢ ∃ a, a ∈ Fintype.elems ∧ BiconeHom.diagram a = BiconeHom.diagram f
[PROOFSTEP]
use f
[GOAL]
case h
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
f : val✝¹ ⟶ val✝
⊢ f ∈ Fintype.elems ∧ BiconeHom.diagram f = BiconeHom.diagram f
[PROOFSTEP]
simpa using Fintype.complete _
