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
Y Z : Bicone J
h : Y ⟶ Z
j : J
g : Bicone.diagram j ⟶ Y
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left j ≫ g) ≫ h) (BiconeHom.left j ≫ g ≫ h)
have left : ∀ {k : J} (f : j ⟶ k) (h : Bicone.diagram k ⟶ Z),
  Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left j ≫ BiconeHom.diagram f) ≫ h) (BiconeHom.left j ≫ BiconeHom.diagram f ≫ 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
j : J
g : Bicone.diagram j ⟶ Y
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right j ≫ g) ≫ h) (BiconeHom.right j ≫ g ≫ h)
have right : ∀ {k : J} (f : j ⟶ k) (h : Bicone.diagram k ⟶ Z),
  Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right j ≫ BiconeHom.diagram f) ≫ h)
    (BiconeHom.right j ≫ BiconeHom.diagram f ≫ 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
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)
have diagram : ∀ {k_1 : J} (f_1 : k ⟶ k_1) (h : Bicone.diagram k_1 ⟶ Z),
  Eq (α := Bicone.diagram j ⟶ Z) ((BiconeHom.diagram f ≫ BiconeHom.diagram f_1) ≫ h)
    (BiconeHom.diagram f ≫ BiconeHom.diagram f_1 ≫ 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
Z : Bicone J
h : Bicone.left ⟶ Z
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h) (BiconeHom.left_id ≫ BiconeHom.left_id ≫ h)
have left_id : Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
  ((BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left_id)
  (BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left_id)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
h : Bicone.left ⟶ Z
left_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
    ((BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left_id)
    (BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left_id)
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h) (BiconeHom.left_id ≫ BiconeHom.left_id ≫ h)
have left_id₁ : ∀ (j : J),
  Eq (α := Bicone.left ⟶ Bicone.diagram j) ((BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left j)
    (BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left j)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
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)
have left_id : ∀ {k : J} (f : j ⟶ k),
  Eq (α := Bicone.left ⟶ Bicone.diagram k) ((BiconeHom.left_id ≫ BiconeHom.left j) ≫ BiconeHom.diagram f)
    (BiconeHom.left_id ≫ BiconeHom.left j ≫ BiconeHom.diagram f)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
h : Bicone.right ⟶ Z
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h)
    (BiconeHom.right_id ≫ BiconeHom.right_id ≫ h)
have right_id : Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
  ((BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right_id)
  (BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right_id)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
h : Bicone.right ⟶ Z
right_id :
  Eq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
    ((BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right_id)
    (BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right_id)
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h)
    (BiconeHom.right_id ≫ BiconeHom.right_id ≫ h)
have right_id₁ : ∀ (j : J),
  Eq (α := Bicone.right ⟶ Bicone.diagram j) ((BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right j)
    (BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right j)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
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)
have right_id : ∀ {k : J} (f : j ⟶ k),
  Eq (α := Bicone.right ⟶ Bicone.diagram k) ((BiconeHom.right_id ≫ BiconeHom.right j) ≫ BiconeHom.diagram f)
    (BiconeHom.right_id ≫ BiconeHom.right j ≫ BiconeHom.diagram f)
Tactic: cases h
Cleared hypotheses: Z, h
-- 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
h : Bicone.diagram k ⟶ Z
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left j ≫ BiconeHom.diagram f) ≫ h) (BiconeHom.left j ≫ BiconeHom.diagram f ≫ h)
have left : ∀ {k_1 : J} (f_1 : k ⟶ k_1),
  Eq (α := Bicone.left ⟶ Bicone.diagram k_1) ((BiconeHom.left j ≫ BiconeHom.diagram f) ≫ BiconeHom.diagram f_1)
    (BiconeHom.left j ≫ BiconeHom.diagram f ≫ BiconeHom.diagram f_1)
Tactic: cases h
Cleared hypotheses: Z, h
-- 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
h : Bicone.diagram k ⟶ Z
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right j ≫ BiconeHom.diagram f) ≫ h)
    (BiconeHom.right j ≫ BiconeHom.diagram f ≫ h)
have right : ∀ {k_1 : J} (f_1 : k ⟶ k_1),
  Eq (α := Bicone.right ⟶ Bicone.diagram k_1) ((BiconeHom.right j ≫ BiconeHom.diagram f) ≫ BiconeHom.diagram f_1)
    (BiconeHom.right j ≫ BiconeHom.diagram f ≫ BiconeHom.diagram f_1)
Tactic: cases h
Cleared hypotheses: Z, h
-- 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
k_1 : J
f_1 : k ⟶ k_1
h : Bicone.diagram k_1 ⟶ Z
⊢ Eq (α := Bicone.diagram j ⟶ Z) ((BiconeHom.diagram f ≫ BiconeHom.diagram f_1) ≫ h)
    (BiconeHom.diagram f ≫ BiconeHom.diagram f_1 ≫ h)
have diagram : ∀ {k_2 : J} (f_2 : k_1 ⟶ k_2),
  Eq (α := Bicone.diagram j ⟶ Bicone.diagram k_2)
    ((BiconeHom.diagram f ≫ BiconeHom.diagram f_1) ≫ BiconeHom.diagram f_2)
    (BiconeHom.diagram f ≫ BiconeHom.diagram f_1 ≫ BiconeHom.diagram f_2)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X Y : Bicone J
f : X ⟶ Y
⊢ Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
have left_id : Quiver.Hom.{v₁, u₁} (V := C)
  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X Y : Bicone J
f : X ⟶ Y
left_id :
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
⊢ Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
have right_id : Quiver.Hom.{v₁, u₁} (V := C)
  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X Y : Bicone J
f : X ⟶ Y
left_id :
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
right_id :
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
⊢ Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
have left : (j : J) →
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X Y : Bicone J
f : X ⟶ Y
left_id :
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
right_id :
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
left :
  (j : J) →
    Quiver.Hom.{v₁, u₁} (V := C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
⊢ Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
have right : (j : J) →
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X Y : Bicone J
f : X ⟶ Y
left_id :
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
right_id :
  Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
left :
  (j : J) →
    Quiver.Hom.{v₁, u₁} (V := C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
right :
  (j : J) →
    Quiver.Hom.{v₁, u₁} (V := C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
⊢ Quiver.Hom.{v₁, u₁} (V := C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
have diagram : {j k : J} →
  (f : j ⟶ k) →
    Quiver.Hom.{v₁, u₁} (V := C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram k) c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
j k : Bicone J
⊢ Fintype (j ⟶ k)
have left : Fintype (Bicone.left ⟶ k)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
j k : Bicone J
left : Fintype (Bicone.left ⟶ k)
⊢ Fintype (j ⟶ k)
have right : Fintype (Bicone.right ⟶ k)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
j k : Bicone J
left : Fintype (Bicone.left ⟶ k)
right : Fintype (Bicone.right ⟶ k)
⊢ Fintype (j ⟶ k)
have diagram : (val : J) → Fintype (Bicone.diagram val ⟶ k)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
⊢ Fintype (Bicone.left ⟶ k)
have left : Fintype (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
left : Fintype (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
⊢ Fintype (Bicone.left ⟶ k)
have left₁ : Fintype (Quiver.Hom (V := Bicone J) Bicone.left Bicone.right)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
left : Fintype (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
left₁ : Fintype (Quiver.Hom (V := Bicone J) Bicone.left Bicone.right)
⊢ Fintype (Bicone.left ⟶ k)
have left₂ : (val : J) → Fintype (Bicone.left ⟶ Bicone.diagram val)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
⊢ Fintype (Bicone.right ⟶ k)
have right : Fintype (Quiver.Hom (V := Bicone J) Bicone.right Bicone.left)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
right : Fintype (Quiver.Hom (V := Bicone J) Bicone.right Bicone.left)
⊢ Fintype (Bicone.right ⟶ k)
have right₁ : Fintype (Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
right : Fintype (Quiver.Hom (V := Bicone J) Bicone.right Bicone.left)
right₁ : Fintype (Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
⊢ Fintype (Bicone.right ⟶ k)
have right₂ : (val : J) → Fintype (Bicone.right ⟶ Bicone.diagram val)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
val : J
⊢ Fintype (Bicone.diagram val ⟶ k)
have diagram : Fintype (Bicone.diagram val ⟶ Bicone.left)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
val : J
diagram : Fintype (Bicone.diagram val ⟶ Bicone.left)
⊢ Fintype (Bicone.diagram val ⟶ k)
have diagram₁ : Fintype (Bicone.diagram val ⟶ Bicone.right)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
k : Bicone J
val : J
diagram : Fintype (Bicone.diagram val ⟶ Bicone.left)
diagram₁ : Fintype (Bicone.diagram val ⟶ Bicone.right)
⊢ Fintype (Bicone.diagram val ⟶ k)
have diagram₂ : (val_1 : J) → Fintype (Bicone.diagram val ⟶ Bicone.diagram val_1)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left
⊢ Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)) {BiconeHom.left_id} f
have left_id : Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)) {BiconeHom.left_id} BiconeHom.left_id
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
f : Bicone.left ⟶ Bicone.diagram val
⊢ Membership.mem (γ := Finset (Bicone.left ⟶ Bicone.diagram val)) {BiconeHom.left val} f
have left : Membership.mem (γ := Finset (Bicone.left ⟶ Bicone.diagram val)) {BiconeHom.left val} (BiconeHom.left val)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right
⊢ Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)) {BiconeHom.right_id} f
have right_id : Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)) {BiconeHom.right_id}
  BiconeHom.right_id
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
f : Bicone.right ⟶ Bicone.diagram val
⊢ Membership.mem (γ := Finset (Bicone.right ⟶ Bicone.diagram val)) {BiconeHom.right val} f
have right : Membership.mem (γ := Finset (Bicone.right ⟶ Bicone.diagram val)) {BiconeHom.right val} (BiconeHom.right val)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val val_1 : J
f : Bicone.diagram val ⟶ Bicone.diagram val_1
⊢ Membership.mem (γ := Finset (Bicone.diagram val ⟶ Bicone.diagram val_1))
    (Finset.image BiconeHom.diagram Fintype.elems) f
have diagram : ∀ (f : val ⟶ val_1),
  Membership.mem (γ := Finset (Bicone.diagram val ⟶ Bicone.diagram val_1))
    (Finset.image BiconeHom.diagram Fintype.elems) (BiconeHom.diagram f)
Tactic: rcases f with (_ | _ | _ | _ | f)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val val_1 : J
f : val ⟶ val_1
⊢ Membership.mem (γ := Finset (Bicone.diagram val ⟶ Bicone.diagram val_1))
    (Finset.image BiconeHom.diagram Fintype.elems) (BiconeHom.diagram f)
have diagram : ∃ (a : val ⟶ val_1),
  Membership.mem (γ := Finset (val ⟶ val_1)) Fintype.elems a ∧ BiconeHom.diagram a = BiconeHom.diagram f
Tactic: simp only [Finset.mem_image]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val val_1 : J
f : val ⟶ val_1
⊢ ∃ (a : val ⟶ val_1),
    Membership.mem (γ := Finset (val ⟶ val_1)) Fintype.elems a ∧ BiconeHom.diagram a = BiconeHom.diagram f
have h : Membership.mem (γ := Finset (val ⟶ val_1)) Fintype.elems f ∧ BiconeHom.diagram f = BiconeHom.diagram f
Tactic: use f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Chosen.End (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
⊢ f = g
have apply : ∀ (j : WalkingMultispan (multispanShapeCoend.{v_2, u_1} J)),
  (ChosenCoendsOfShape.cowedge F).ι.app j ≫ f = (ChosenCoendsOfShape.cowedge F).ι.app j ≫ g
Tactic: apply (ChosenCoendsOfShape.isCoend F).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Chosen.End (hypothesis)
Goal:
J_1 : Type u_1
C_1 : Type u_2
inst : Category.{v_1, u_2} C_1
inst_1 : Category.{v_2, u_1} J_1
F_1 : J_1ᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J_1 C_1
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J_1 C_1
X_1 : C_1
f_1 : (j : J_1) → (F_1.obj (op j)).obj j ⟶ X_1
hf_1 : ∀ ⦃i j : J_1⦄ (g : i ⟶ j), (F_1.map g.op).app i ≫ f_1 i = (F_1.obj (op j)).map g ≫ f_1 j
J : Type u_3
C : Type u_4
inst_3 : Category.{v_3, u_4} C
inst_4 : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
inst_5 : ChosenEndsOfShape.{v_4, u_3, v_3, u_4} J C
X : C
f_2 : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f_2 i ≫ (F.obj (op i)).map g = f_2 j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
⊢ Eq (α := chosenEnd F ⟶ (G.obj (op j)).obj j')
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : chosenEnd F ⟶ (G.obj (op x)).obj x)) j ≫
      (G.obj (op j)).map φ)
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : chosenEnd F ⟶ (G.obj (op x)).obj x)) j' ≫
      (G.map φ.op).app j')
have e : (F.obj (op j)).map φ ≫ NatTrans.app (f.app (op j)) j' = NatTrans.app (f.app (op j)) j ≫ (G.obj (op j)).map φ
Tactic: have e := (f.app (op j)).naturality φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Chosen.End (goal)
Goal:
J_1 : Type u_1
C_1 : Type u_2
inst : Category.{v_1, u_2} C_1
inst_1 : Category.{v_2, u_1} J_1
F_1 : J_1ᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J_1 C_1
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J_1 C_1
X_1 : C_1
f_1 : (j : J_1) → (F_1.obj (op j)).obj j ⟶ X_1
hf_1 : ∀ ⦃i j : J_1⦄ (g : i ⟶ j), (F_1.map g.op).app i ≫ f_1 i = (F_1.obj (op j)).map g ≫ f_1 j
J : Type u_3
C : Type u_4
inst_3 : Category.{v_3, u_4} C
inst_4 : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
inst_5 : ChosenEndsOfShape.{v_4, u_3, v_3, u_4} J C
X : C
f_2 : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f_2 i ≫ (F.obj (op i)).map g = f_2 j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ NatTrans.app (f.app (op j)) j' = NatTrans.app (f.app (op j)) j ≫ (G.obj (op j)).map φ
⊢ Eq (α := chosenEnd F ⟶ (G.obj (op j)).obj j')
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : chosenEnd F ⟶ (G.obj (op x)).obj x)) j ≫
      (G.obj (op j)).map φ)
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : chosenEnd F ⟶ (G.obj (op x)).obj x)) j' ≫
      (G.map φ.op).app j')
have simp : Eq (α := chosenEnd F ⟶ (G.obj (op j)).obj j') (π F j ≫ NatTrans.app (f.app (op j)) j ≫ (G.obj (op j)).map φ)
  (π F j' ≫ NatTrans.app (f.app (op j')) j' ≫ (G.map φ.op).app j')
Tactic: simp only [Category.assoc]