awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
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)
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
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)
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ g) ≫ h) (BiconeHom.left_id ≫ g ≫ h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
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)
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ g) ≫ h) (BiconeHom.right_id ≫ g ≫ h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Y Z : Bicone J
h : Y ⟶ Z
j : J
g : Bicone.diagram j ⟶ Y
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)
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left j ≫ g) ≫ h) (BiconeHom.left j ≫ g ≫ h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Y Z : Bicone J
h : Y ⟶ Z
j : J
g : Bicone.diagram j ⟶ Y
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)
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right j ≫ g) ≫ h) (BiconeHom.right j ≫ g ≫ h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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
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)
⊢ Eq (α := Bicone.diagram j ⟶ Z) ((BiconeHom.diagram f ≫ g) ≫ h) (BiconeHom.diagram f ≫ g ≫ h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
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)
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h) (BiconeHom.left_id ≫ BiconeHom.left_id ≫ h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j : J
h : Bicone.diagram j ⟶ Z
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)
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left_id ≫ BiconeHom.left j) ≫ h) (BiconeHom.left_id ≫ BiconeHom.left j ≫ h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
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)
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h)
    (BiconeHom.right_id ≫ BiconeHom.right_id ≫ h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j : J
h : Bicone.diagram j ⟶ Z
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)
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right_id ≫ BiconeHom.right j) ≫ h) (BiconeHom.right_id ≫ BiconeHom.right j ≫ h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j k : J
f : j ⟶ k
h : Bicone.diagram k ⟶ Z
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)
⊢ Eq (α := Bicone.left ⟶ Z) ((BiconeHom.left j ≫ BiconeHom.diagram f) ≫ h) (BiconeHom.left j ≫ BiconeHom.diagram f ≫ h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j k : J
f : j ⟶ k
h : Bicone.diagram k ⟶ Z
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)
⊢ Eq (α := Bicone.right ⟶ Z) ((BiconeHom.right j ≫ BiconeHom.diagram f) ≫ h)
    (BiconeHom.right j ≫ BiconeHom.diagram f ≫ h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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
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)
⊢ Eq (α := Bicone.diagram j ⟶ Z) ((BiconeHom.diagram f ≫ BiconeHom.diagram f_1) ≫ h)
    (BiconeHom.diagram f ≫ BiconeHom.diagram f_1 ≫ h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f : j ⟶ k
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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f : j ⟶ k
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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f : j ⟶ k
k_1 : J
f_1 : k ⟶ k_1
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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
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)
⊢ 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)

Tactic:
rcases f with (_ | _ | _ | _ | f)
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ 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:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ 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:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
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:
exact c₁.π.app _

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
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:
exact c₂.π.app _

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
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:
exact F.map f

Premises used: CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
diagram : (val : J) → Fintype (Bicone.diagram val ⟶ k)
⊢ Fintype (j ⟶ k)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
left₂ : (val : J) → Fintype (Bicone.left ⟶ Bicone.diagram val)
⊢ Fintype (Bicone.left ⟶ k)

Tactic:
cases k
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
right₂ : (val : J) → Fintype (Bicone.right ⟶ Bicone.diagram val)
⊢ Fintype (Bicone.right ⟶ k)

Tactic:
cases k
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
diagram₂ : (val_1 : J) → Fintype (Bicone.diagram val ⟶ Bicone.diagram val_1)
⊢ Fintype (Bicone.diagram val ⟶ k)

Tactic:
cases k
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left
left_id :
  Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)) {BiconeHom.left_id}
    BiconeHom.left_id
⊢ Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)) {BiconeHom.left_id} f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
⊢ Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)) {BiconeHom.left_id}
    BiconeHom.left_id

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
⊢ Fintype (Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)

Tactic:
exact
      { elems := {BiconeHom.left_id}
        complete := fun f => by cases f; simp }
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.right
⊢ Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.left Bicone.right)) ∅ f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
⊢ Fintype (Quiver.Hom (V := Bicone J) Bicone.left Bicone.right)

Tactic:
exact
    { elems := ∅
      complete := fun f => by cases f }
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
f : Bicone.left ⟶ Bicone.diagram val
left : Membership.mem (γ := Finset (Bicone.left ⟶ Bicone.diagram val)) {BiconeHom.left val} (BiconeHom.left val)
⊢ Membership.mem (γ := Finset (Bicone.left ⟶ Bicone.diagram val)) {BiconeHom.left val} f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
⊢ Membership.mem (γ := Finset (Bicone.left ⟶ Bicone.diagram val)) {BiconeHom.left val} (BiconeHom.left val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val)

Tactic:
exact
    { elems := {BiconeHom.left _}
      complete := fun f => by cases f; simp }
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.left
⊢ Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.right Bicone.left)) ∅ f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
⊢ Fintype (Quiver.Hom (V := Bicone J) Bicone.right Bicone.left)

Tactic:
exact
    { elems := ∅
      complete := fun f => by cases f }
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right
right_id :
  Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)) {BiconeHom.right_id}
    BiconeHom.right_id
⊢ Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)) {BiconeHom.right_id} f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
⊢ Membership.mem (γ := Finset (Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)) {BiconeHom.right_id}
    BiconeHom.right_id

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
⊢ Fintype (Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)

Tactic:
exact
      { elems := {BiconeHom.right_id}
        complete := fun f => by cases f; simp }
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
f : Bicone.right ⟶ Bicone.diagram val
right : Membership.mem (γ := Finset (Bicone.right ⟶ Bicone.diagram val)) {BiconeHom.right val} (BiconeHom.right val)
⊢ Membership.mem (γ := Finset (Bicone.right ⟶ Bicone.diagram val)) {BiconeHom.right val} f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
⊢ Membership.mem (γ := Finset (Bicone.right ⟶ Bicone.diagram val)) {BiconeHom.right val} (BiconeHom.right val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
⊢ Fintype (Bicone.right ⟶ Bicone.diagram val)

Tactic:
exact
    { elems := {BiconeHom.right _}
      complete := fun f => by cases f; simp }
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
f : Bicone.diagram val ⟶ Bicone.left
⊢ Membership.mem (γ := Finset (Bicone.diagram val ⟶ Bicone.left)) ∅ f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
⊢ Fintype (Bicone.diagram val ⟶ Bicone.left)

Tactic:
exact
    { elems := ∅
      complete := fun f => by cases f }
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
f : Bicone.diagram val ⟶ Bicone.right
⊢ Membership.mem (γ := Finset (Bicone.diagram val ⟶ Bicone.right)) ∅ f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val : J
⊢ Fintype (Bicone.diagram val ⟶ Bicone.right)

Tactic:
exact
    { elems := ∅
      complete := fun f => by cases f }
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val val_1 : J
f : Bicone.diagram val ⟶ Bicone.diagram val_1
diagram :
  ∀ (f : val ⟶ val_1),
    Membership.mem (γ := Finset (Bicone.diagram val ⟶ Bicone.diagram val_1))
      (Finset.image BiconeHom.diagram Fintype.elems) (BiconeHom.diagram f)
⊢ Membership.mem (γ := Finset (Bicone.diagram val ⟶ Bicone.diagram val_1))
    (Finset.image BiconeHom.diagram Fintype.elems) f

Tactic:
rcases f with (_ | _ | _ | _ | f)
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val val_1 : J
f : val ⟶ val_1
diagram :
  ∃ (a : val ⟶ val_1),
    Membership.mem (γ := Finset (val ⟶ val_1)) Fintype.elems a ∧ BiconeHom.diagram a = BiconeHom.diagram f
⊢ Membership.mem (γ := Finset (Bicone.diagram val ⟶ Bicone.diagram val_1))
    (Finset.image BiconeHom.diagram Fintype.elems) (BiconeHom.diagram f)

Tactic:
simp only [Finset.mem_image]

Premises used: Finset.mem_image
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val val_1 : J
f : val ⟶ val_1
h : Membership.mem (γ := Finset (val ⟶ val_1)) Fintype.elems f ∧ BiconeHom.diagram f = BiconeHom.diagram f
⊢ ∃ (a : val ⟶ val_1),
    Membership.mem (γ := Finset (val ⟶ val_1)) Fintype.elems a ∧ BiconeHom.diagram a = BiconeHom.diagram f

Tactic:
use f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val val_1 : J
f : val ⟶ val_1
⊢ Membership.mem (γ := Finset (val ⟶ val_1)) Fintype.elems f ∧ BiconeHom.diagram f = BiconeHom.diagram f

Tactic:
simpa using Fintype.complete _

Premises used: Fintype.complete
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type v₁
inst : SmallCategory J
inst_1 : FinCategory J
val val_1 : J
⊢ Fintype (Bicone.diagram val ⟶ Bicone.diagram val_1)

Tactic:
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 _ }
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
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
i j : J
f : i ⟶ j
⊢ Eq (α := (F.obj (op j)).obj i ⟶ chosenCoend F) ((F.map f.op).app i ≫ ι F i) ((F.obj (op j)).map f ≫ ι F j)

Tactic:
(ChosenCoendsOfShape.cowedge F).condition f

Premises used: CategoryTheory.Limits.chosenCoend.ι, CategoryTheory.Limits.ChosenCoendsOfShape.cowedge, CategoryTheory.Limits.chosenCoend, CategoryTheory.Limits.Cowedge.condition