-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom.{v₁, u₁} J j k
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₁ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₁ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₁ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₁ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₁ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₂ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₂ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₂ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₂ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₂ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₃ : (g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) → Decidable (BiconeHom.left_id = g)
right_id₃ : (g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) → Decidable (BiconeHom.right_id = g)
left₃ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) → Decidable (BiconeHom.left j = g)
right₃ : (j : J) → (g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) → Decidable (BiconeHom.right j = g)
diagram₃ :
  {j k : J} →
    (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)) → Decidable (BiconeHom.diagram f = g)
left_id₄ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) BiconeHom.left_id BiconeHom.left_id)
right_id₄ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) BiconeHom.right_id BiconeHom.right_id)
left₄ :
  (j : J) →
    Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (BiconeHom.left j) (BiconeHom.left j))
right₄ :
  (j : J) →
    Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (BiconeHom.right j) (BiconeHom.right j))
diagram₄ : {j k : J} → (f f_1 : j ⟶ k) → Decidable (BiconeHom.diagram f = BiconeHom.diagram f_1)
left_id₅ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) BiconeHom.left_id BiconeHom.left_id)
right_id₅ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) BiconeHom.right_id BiconeHom.right_id)
left₅ :
  (j : J) →
    Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (BiconeHom.left j) (BiconeHom.left j))
right₅ :
  (j : J) →
    Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (BiconeHom.right j) (BiconeHom.right j))
diagram₅ : {j k : J} → (f f_1 : j ⟶ k) → Decidable (BiconeHom.diagram f = BiconeHom.diagram f_1)
left_id₆ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) BiconeHom.left_id BiconeHom.left_id)
right_id₆ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) BiconeHom.right_id BiconeHom.right_id)
left₆ :
  (j : J) →
    Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (BiconeHom.left j) (BiconeHom.left j))
right₆ :
  (j : J) →
    Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (BiconeHom.right j) (BiconeHom.right j))
diagram₆ : {j k : J} → (f f_1 : j ⟶ k) → Decidable (BiconeHom.diagram f = BiconeHom.diagram f_1)
left_id₇ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) BiconeHom.left_id BiconeHom.left_id)
right_id₇ : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) BiconeHom.right_id BiconeHom.right_id)
left₇ :
  (j : J) →
    Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (BiconeHom.left j) (BiconeHom.left j))
right₇ :
  (j : J) →
    Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (BiconeHom.right j) (BiconeHom.right j))
diagram₇ : {j k : J} → (f f_1 : j ⟶ k) → Decidable (BiconeHom.diagram f = BiconeHom.diagram f_1)
left_id₈ right_id₈ : Decidable True
left₈ right₈ : J → Decidable True
⊢ Decidable (f = g)
have diagram₈ : {j k : J} → (f f_1 : j ⟶ k) → Decidable (f = f_1)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g