awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Decidable (f = g)
have left₄ : (j : J) →
  Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (BiconeHom.left j) (BiconeHom.left j))
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- 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))
⊢ Decidable (f = g)
have right₄ : (j : J) →
  Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (BiconeHom.right j) (BiconeHom.right j))
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- 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))
⊢ Decidable (f = g)
have diagram₄ : {j k : J} → (f f_1 : j ⟶ k) → Decidable (BiconeHom.diagram f = BiconeHom.diagram f_1)
Tactic: classical cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance
Cleared hypotheses: j, k, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y Z : Bicone J
f : BiconeHom.{v₁, u₁} J X Y
g : BiconeHom.{v₁, u₁} J Y Z
⊢ BiconeHom.{v₁, u₁} J X Z
have left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Z) → BiconeHom.{v₁, u₁} J Bicone.left Z
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y Z : Bicone J
f : BiconeHom.{v₁, u₁} J X Y
g : BiconeHom.{v₁, u₁} J Y Z
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Z) → BiconeHom.{v₁, u₁} J Bicone.left Z
⊢ BiconeHom.{v₁, u₁} J X Z
have right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Z) → BiconeHom.{v₁, u₁} J Bicone.right Z
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y Z : Bicone J
f : BiconeHom.{v₁, u₁} J X Y
g : BiconeHom.{v₁, u₁} J Y Z
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Z) → BiconeHom.{v₁, u₁} J Bicone.left Z
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Z) → BiconeHom.{v₁, u₁} J Bicone.right Z
⊢ BiconeHom.{v₁, u₁} J X Z
have left : (j : J) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z) → BiconeHom.{v₁, u₁} J Bicone.left Z
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y Z : Bicone J
f : BiconeHom.{v₁, u₁} J X Y
g : BiconeHom.{v₁, u₁} J Y Z
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Z) → BiconeHom.{v₁, u₁} J Bicone.left Z
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Z) → BiconeHom.{v₁, u₁} J Bicone.right Z
left : (j : J) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z) → BiconeHom.{v₁, u₁} J Bicone.left Z
⊢ BiconeHom.{v₁, u₁} J X Z
have right : (j : J) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z) → BiconeHom.{v₁, u₁} J Bicone.right Z
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y Z : Bicone J
f : BiconeHom.{v₁, u₁} J X Y
g : BiconeHom.{v₁, u₁} J Y Z
left_id : (g : BiconeHom.{v₁, u₁} J Bicone.left Z) → BiconeHom.{v₁, u₁} J Bicone.left Z
right_id : (g : BiconeHom.{v₁, u₁} J Bicone.right Z) → BiconeHom.{v₁, u₁} J Bicone.right Z
left : (j : J) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z) → BiconeHom.{v₁, u₁} J Bicone.left Z
right : (j : J) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z) → BiconeHom.{v₁, u₁} J Bicone.right Z
⊢ BiconeHom.{v₁, u₁} J X Z
have diagram : {j k : J} → (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram k) Z) → BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j : J
g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z
⊢ BiconeHom.{v₁, u₁} J Bicone.left Z
have left : {k : J} → (j ⟶ k) → BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram k)
Tactic: cases g
Cleared hypotheses: Z, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j : J
g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z
⊢ BiconeHom.{v₁, u₁} J Bicone.right Z
have right : {k : J} → (j ⟶ k) → BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram k)
Tactic: cases g
Cleared hypotheses: Z, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j k : J
f : j ⟶ k
g : BiconeHom.{v₁, u₁} J (Bicone.diagram k) Z
⊢ BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z
have diagram : {k_1 : J} → (g : k ⟶ k_1) → BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k_1)
Tactic: rcases g with (_ | _ | _ | _ | g)
Cleared hypotheses: Z, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f
have left_id : Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (𝟙 Bicone.left ≫ BiconeHom.left_id) BiconeHom.left_id
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (𝟙 Bicone.left ≫ BiconeHom.left_id) BiconeHom.left_id
⊢ 𝟙 X ≫ f = f
have right_id : Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (𝟙 Bicone.right ≫ BiconeHom.right_id) BiconeHom.right_id
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (𝟙 Bicone.left ≫ BiconeHom.left_id) BiconeHom.left_id
right_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (𝟙 Bicone.right ≫ BiconeHom.right_id)
    BiconeHom.right_id
⊢ 𝟙 X ≫ f = f
have left : ∀ (j : J), Eq (α := Bicone.left ⟶ Bicone.diagram j) (𝟙 Bicone.left ≫ BiconeHom.left j) (BiconeHom.left j)
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (𝟙 Bicone.left ≫ BiconeHom.left_id) BiconeHom.left_id
right_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (𝟙 Bicone.right ≫ BiconeHom.right_id)
    BiconeHom.right_id
left : ∀ (j : J), Eq (α := Bicone.left ⟶ Bicone.diagram j) (𝟙 Bicone.left ≫ BiconeHom.left j) (BiconeHom.left j)
⊢ 𝟙 X ≫ f = f
have right : ∀ (j : J), Eq (α := Bicone.right ⟶ Bicone.diagram j) (𝟙 Bicone.right ≫ BiconeHom.right j) (BiconeHom.right j)
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (𝟙 Bicone.left ≫ BiconeHom.left_id) BiconeHom.left_id
right_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (𝟙 Bicone.right ≫ BiconeHom.right_id)
    BiconeHom.right_id
left : ∀ (j : J), Eq (α := Bicone.left ⟶ Bicone.diagram j) (𝟙 Bicone.left ≫ BiconeHom.left j) (BiconeHom.left j)
right : ∀ (j : J), Eq (α := Bicone.right ⟶ Bicone.diagram j) (𝟙 Bicone.right ≫ BiconeHom.right j) (BiconeHom.right j)
⊢ 𝟙 X ≫ f = f
have diagram : ∀ {j k : J} (f : j ⟶ k), 𝟙 (Bicone.diagram j) ≫ BiconeHom.diagram f = BiconeHom.diagram f
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
have left_id : Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (BiconeHom.left_id ≫ 𝟙 Bicone.left) BiconeHom.left_id
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (BiconeHom.left_id ≫ 𝟙 Bicone.left) BiconeHom.left_id
⊢ f ≫ 𝟙 Y = f
have right_id : Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (BiconeHom.right_id ≫ 𝟙 Bicone.right) BiconeHom.right_id
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (BiconeHom.left_id ≫ 𝟙 Bicone.left) BiconeHom.left_id
right_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (BiconeHom.right_id ≫ 𝟙 Bicone.right)
    BiconeHom.right_id
⊢ f ≫ 𝟙 Y = f
have left : ∀ (j : J), Eq (α := Bicone.left ⟶ Bicone.diagram j) (BiconeHom.left j ≫ 𝟙 (Bicone.diagram j)) (BiconeHom.left j)
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (BiconeHom.left_id ≫ 𝟙 Bicone.left) BiconeHom.left_id
right_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (BiconeHom.right_id ≫ 𝟙 Bicone.right)
    BiconeHom.right_id
left : ∀ (j : J), Eq (α := Bicone.left ⟶ Bicone.diagram j) (BiconeHom.left j ≫ 𝟙 (Bicone.diagram j)) (BiconeHom.left j)
⊢ f ≫ 𝟙 Y = f
have right : ∀ (j : J), Eq (α := Bicone.right ⟶ Bicone.diagram j) (BiconeHom.right j ≫ 𝟙 (Bicone.diagram j)) (BiconeHom.right j)
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
X Y : Bicone J
f : X ⟶ Y
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (BiconeHom.left_id ≫ 𝟙 Bicone.left) BiconeHom.left_id
right_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (BiconeHom.right_id ≫ 𝟙 Bicone.right)
    BiconeHom.right_id
left : ∀ (j : J), Eq (α := Bicone.left ⟶ Bicone.diagram j) (BiconeHom.left j ≫ 𝟙 (Bicone.diagram j)) (BiconeHom.left j)
right :
  ∀ (j : J), Eq (α := Bicone.right ⟶ Bicone.diagram j) (BiconeHom.right j ≫ 𝟙 (Bicone.diagram j)) (BiconeHom.right j)
⊢ f ≫ 𝟙 Y = f
have diagram : ∀ {j k : J} (f : j ⟶ k), BiconeHom.diagram f ≫ 𝟙 (Bicone.diagram k) = BiconeHom.diagram f
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
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
have left_id : ∀ (g : Bicone.left ⟶ Y), Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ g) ≫ h) (BiconeHom.left_id ≫ g ≫ h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
W X Y Z : Bicone J
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
left_id : ∀ (g : Bicone.left ⟶ Y), Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ g) ≫ h) (BiconeHom.left_id ≫ g ≫ h)
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have right_id : ∀ (g : Bicone.right ⟶ Y), Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ g) ≫ h) (BiconeHom.right_id ≫ g ≫ h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
W X Y Z : Bicone J
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
left_id : ∀ (g : Bicone.left ⟶ Y), Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ g) ≫ h) (BiconeHom.left_id ≫ g ≫ h)
right_id :
  ∀ (g : Bicone.right ⟶ Y), Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ g) ≫ h) (BiconeHom.right_id ≫ g ≫ h)
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have left : ∀ (j : J) (g : Bicone.diagram j ⟶ Y), Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left j ≫ g) ≫ h) (BiconeHom.left j ≫ g ≫ h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
W X Y Z : Bicone J
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
left_id : ∀ (g : Bicone.left ⟶ Y), Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ g) ≫ h) (BiconeHom.left_id ≫ g ≫ h)
right_id :
  ∀ (g : Bicone.right ⟶ Y), Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ g) ≫ h) (BiconeHom.right_id ≫ g ≫ h)
left :
  ∀ (j : J) (g : Bicone.diagram j ⟶ Y),
    Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left j ≫ g) ≫ h) (BiconeHom.left j ≫ g ≫ h)
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have right : ∀ (j : J) (g : Bicone.diagram j ⟶ Y),
  Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right j ≫ g) ≫ h) (BiconeHom.right j ≫ g ≫ h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
W X Y Z : Bicone J
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
left_id : ∀ (g : Bicone.left ⟶ Y), Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ g) ≫ h) (BiconeHom.left_id ≫ g ≫ h)
right_id :
  ∀ (g : Bicone.right ⟶ Y), Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ g) ≫ h) (BiconeHom.right_id ≫ g ≫ h)
left :
  ∀ (j : J) (g : Bicone.diagram j ⟶ Y),
    Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left j ≫ g) ≫ h) (BiconeHom.left j ≫ g ≫ h)
right :
  ∀ (j : J) (g : Bicone.diagram j ⟶ Y),
    Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right j ≫ g) ≫ h) (BiconeHom.right j ≫ g ≫ h)
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have diagram : ∀ {j k : J} (f : j ⟶ k) (g : Bicone.diagram k ⟶ Y),
  Eq (α := Bicone.diagram j ⟶ Z) ((BiconeHom.diagram f ≫ g) ≫ h) (BiconeHom.diagram f ≫ g ≫ h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Y Z : Bicone J
h : Y ⟶ Z
g : Bicone.left ⟶ Y
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ g) ≫ h) (BiconeHom.left_id ≫ g ≫ h)
have left_id : ∀ (h : Bicone.left ⟶ Z),
  Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h) (BiconeHom.left_id ≫ BiconeHom.left_id ≫ h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Y Z : Bicone J
h : Y ⟶ Z
g : Bicone.left ⟶ Y
left_id :
  ∀ (h : Bicone.left ⟶ Z),
    Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h) (BiconeHom.left_id ≫ BiconeHom.left_id ≫ h)
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ g) ≫ h) (BiconeHom.left_id ≫ g ≫ h)
have left_id₁ : ∀ (j : J) (h : Bicone.diagram j ⟶ Z),
  Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ BiconeHom.left j) ≫ h) (BiconeHom.left_id ≫ BiconeHom.left j ≫ h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Y Z : Bicone J
h : Y ⟶ Z
g : Bicone.right ⟶ Y
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ g) ≫ h) (BiconeHom.right_id ≫ g ≫ h)
have right_id : ∀ (h : Bicone.right ⟶ Z),
  Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h)
    (BiconeHom.right_id ≫ BiconeHom.right_id ≫ h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Y Z : Bicone J
h : Y ⟶ Z
g : Bicone.right ⟶ Y
right_id :
  ∀ (h : Bicone.right ⟶ Z),
    Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h)
      (BiconeHom.right_id ≫ BiconeHom.right_id ≫ h)
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ g) ≫ h) (BiconeHom.right_id ≫ g ≫ h)
have right_id₁ : ∀ (j : J) (h : Bicone.diagram j ⟶ Z),
  Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ BiconeHom.right j) ≫ h) (BiconeHom.right_id ≫ BiconeHom.right j ≫ h)
Tactic: cases g
Cleared hypotheses: Y, h, g