Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: 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

pp: 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✝

pp: 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✝

pp: 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

pp: 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✝

pp: 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✝

pp: 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✝

pp: 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✝

pp: 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✝

Tactic:
<;>

Goal state after:
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

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✝

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✝

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

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✝

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✝

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✝

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✝

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✝