awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial.{v, u} A
this :
  HasLiftingProperty (A :=
      pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom))
      (ι (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom)) h ↔
    HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B (Arrow.mk g).left) (B ◁ (Arrow.mk g).hom) h
⊢ HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B K) (B ◁ g) h ↔
    HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)

Tactic:
Adjunction.hasLiftingProperty_iff (ihom.adjunction B) g h

Premises used: CategoryTheory.Adjunction.hasLiftingProperty_iff, CategoryTheory.ihom.adjunction
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial.{v, u} A
this :
  HasLiftingProperty (A :=
      pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom))
      (ι (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom)) h ↔
    HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B (Arrow.mk g).left) (B ◁ (Arrow.mk g).hom) h
⊢ HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B K) (B ◁ g) h ↔
    HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)

Tactic:
exact Adjunction.hasLiftingProperty_iff (ihom.adjunction B) g h

Premises used: CategoryTheory.Adjunction.hasLiftingProperty_iff, CategoryTheory.ihom.adjunction
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
h : X ⟶ Y
i : IsInitial.{v, u} K
rw :
  HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom h ↔ HasLiftingProperty (Arrow.mk (i.to L) □ Arrow.mk f).hom h
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom h ↔ HasLiftingProperty (X := L ⟹ X) f (map (ihom L) h)

Tactic:
rw [← hasLiftingProperty_mk_isInitial_iff i]

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
h : X ⟶ Y
i : IsInitial.{v, u} K
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom h ↔ HasLiftingProperty (Arrow.mk (i.to L) □ Arrow.mk f).hom h

Tactic:
HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) h

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding, CategoryTheory.Limits.PushoutCocone.IsColimit.desc, CategoryTheory.Functor.PushoutObjObj.ι, CategoryTheory.Limits.colimit, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left, CategoryTheory.IsPushout.desc
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
h : X ⟶ Y
i : IsInitial.{v, u} K
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom h ↔ HasLiftingProperty (Arrow.mk (i.to L) □ Arrow.mk f).hom h

Tactic:
exact HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) h

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal.{v, u} Y
rw :
  HasLiftingProperty g (Opposite.op (Arrow.mk f) ⋔ Arrow.mk (t.from X)).hom ↔
    HasLiftingProperty (X := B ⟹ X) (Y := A ⟹ X) g (NatTrans.app (MonoidalClosed.pre f) X)
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom (t.from X) ↔
    HasLiftingProperty (X := B ⟹ X) (Y := A ⟹ X) g (NatTrans.app (MonoidalClosed.pre f) X)

Tactic:
rw [hasLiftingProperty_mk_iff]

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty g (Opposite.op (Arrow.mk f) ⋔ Arrow.mk (t.from X)).hom ↔
    HasLiftingProperty (X := B ⟹ X) (Y := A ⟹ X) g (NatTrans.app (MonoidalClosed.pre f) X)

Tactic:
HasLiftingProperty.iff_of_arrow_iso_right g (PullbackHom.isTerminalIso _ t)

Premises used: CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right, CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty g (Opposite.op (Arrow.mk f) ⋔ Arrow.mk (t.from X)).hom ↔
    HasLiftingProperty (X := B ⟹ X) (Y := A ⟹ X) g (NatTrans.app (MonoidalClosed.pre f) X)

Tactic:
exact HasLiftingProperty.iff_of_arrow_iso_right g (PullbackHom.isTerminalIso _ t)

Premises used: CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right, CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
i : IsInitial.{v, u} A
t : IsTerminal.{v, u} Y
rw : HasLiftingProperty (X := B ⟹ X) g (map (ihom B) (t.from X)) ↔ HasLiftingProperty (X := B ⟹ X) g (t.from (B ⟹ X))
⊢ HasLiftingProperty (Arrow.mk (i.to B) □ Arrow.mk g).hom (t.from X) ↔
    HasLiftingProperty (X := B ⟹ X) g (t.from (B ⟹ X))

Tactic:
rw [hasLiftingProperty_mk_isInitial_iff]

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
i : IsInitial.{v, u} A
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty (X := B ⟹ X) g (map (ihom B) (t.from X)) ↔ HasLiftingProperty (X := B ⟹ X) g (t.from (B ⟹ X))

Tactic:
HasLiftingProperty.iff_of_arrow_iso_right g
    (Arrow.isoMk' _ _ (Iso.refl _) ((IsTerminal.isTerminalObj (ihom B) _ t).uniqueUpToIso t)
      (t.hom_ext _ _))

Premises used: CategoryTheory.Limits.IsTerminal.uniqueUpToIso, CategoryTheory.Iso.refl, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right, CategoryTheory.Limits.IsTerminal.isTerminalObj, CategoryTheory.Arrow.isoMk', CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.ihom
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
i : IsInitial.{v, u} A
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty (X := B ⟹ X) g (map (ihom B) (t.from X)) ↔ HasLiftingProperty (X := B ⟹ X) g (t.from (B ⟹ X))

Tactic:
exact HasLiftingProperty.iff_of_arrow_iso_right g
    (Arrow.isoMk' _ _ (Iso.refl _) ((IsTerminal.isTerminalObj (ihom B) _ t).uniqueUpToIso t)
      (t.hom_ext _ _))

Premises used: CategoryTheory.Limits.IsTerminal.uniqueUpToIso, CategoryTheory.Iso.refl, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right, CategoryTheory.Limits.IsTerminal.isTerminalObj, CategoryTheory.Arrow.isoMk', CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.ihom
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
i : IsInitial.{v, u} K
t : IsTerminal.{v, u} Y
rw : HasLiftingProperty (X := L ⟹ X) f (map (ihom L) (t.from X)) ↔ HasLiftingProperty (X := L ⟹ X) f (t.from (L ⟹ X))
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom (t.from X) ↔
    HasLiftingProperty (X := L ⟹ X) f (t.from (L ⟹ X))

Tactic:
rw [hasLiftingProperty_mk_isInitial_iff']

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff'
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
i : IsInitial.{v, u} K
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty (X := L ⟹ X) f (map (ihom L) (t.from X)) ↔ HasLiftingProperty (X := L ⟹ X) f (t.from (L ⟹ X))

Tactic:
HasLiftingProperty.iff_of_arrow_iso_right f
    (Arrow.isoMk' _ _ (Iso.refl _) ((IsTerminal.isTerminalObj (ihom L) _ t).uniqueUpToIso t)
      (t.hom_ext _ _))

Premises used: CategoryTheory.Limits.IsTerminal.uniqueUpToIso, CategoryTheory.Iso.refl, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right, CategoryTheory.Limits.IsTerminal.isTerminalObj, CategoryTheory.Arrow.isoMk', CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.ihom
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
i : IsInitial.{v, u} K
t : IsTerminal.{v, u} Y
⊢ HasLiftingProperty (X := L ⟹ X) f (map (ihom L) (t.from X)) ↔ HasLiftingProperty (X := L ⟹ X) f (t.from (L ⟹ X))

Tactic:
exact HasLiftingProperty.iff_of_arrow_iso_right f
    (Arrow.isoMk' _ _ (Iso.refl _) ((IsTerminal.isTerminalObj (ihom L) _ t).uniqueUpToIso t)
      (t.hom_ext _ _))

Premises used: CategoryTheory.Limits.IsTerminal.uniqueUpToIso, CategoryTheory.Iso.refl, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right, CategoryTheory.Limits.IsTerminal.isTerminalObj, CategoryTheory.Arrow.isoMk', CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.ihom
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Fintype J
j : Bicone J
left :
  Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.left
right :
  Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.right
diagram :
  ∀ (val : J),
    Membership.mem (γ := Finset (Bicone J))
      (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) (Bicone.diagram val)
⊢ Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Fintype J
⊢ Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.left

Tactic:
simp [Fintype.complete]

Premises used: Fintype.complete
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Fintype J
⊢ Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) Bicone.right

Tactic:
simp [Fintype.complete]

Premises used: Fintype.complete
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Fintype J
val : J
⊢ Membership.mem (γ := Finset (Bicone J))
    (List.toFinset [Bicone.left, Bicone.right] ∪ Finset.image Bicone.diagram Fintype.elems) (Bicone.diagram val)

Tactic:
simp [Fintype.complete]

Premises used: Fintype.complete
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
⊢ Decidable (f = g)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
g : BiconeHom.{v₁, u₁} J Bicone.left Bicone.left
left_id : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) BiconeHom.left_id BiconeHom.left_id)
⊢ Decidable (BiconeHom.left_id = g)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
g : BiconeHom.{v₁, u₁} J Bicone.right Bicone.right
right_id : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) BiconeHom.right_id BiconeHom.right_id)
⊢ Decidable (BiconeHom.right_id = g)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
g : BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)
left : Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (BiconeHom.left j) (BiconeHom.left j))
⊢ Decidable (BiconeHom.left j = g)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
g : BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)
right :
  Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (BiconeHom.right j) (BiconeHom.right j))
⊢ Decidable (BiconeHom.right j = g)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f : j ⟶ k
g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k)
diagram : (f_1 : j ⟶ k) → Decidable (BiconeHom.diagram f = BiconeHom.diagram f_1)
⊢ Decidable (BiconeHom.diagram f = g)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
left_id : Decidable True
⊢ Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left Bicone.left) BiconeHom.left_id BiconeHom.left_id)

Tactic:
simp only [diagram.injEq]

Premises used: CategoryTheory.BiconeHom.diagram.injEq
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
right_id : Decidable True
⊢ Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right Bicone.right) BiconeHom.right_id BiconeHom.right_id)

Tactic:
simp only [diagram.injEq]

Premises used: CategoryTheory.BiconeHom.diagram.injEq
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
left : Decidable True
⊢ Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram j)) (BiconeHom.left j) (BiconeHom.left j))

Tactic:
simp only [diagram.injEq]

Premises used: CategoryTheory.BiconeHom.diagram.injEq
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
right : Decidable True
⊢ Decidable (Eq (α := BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram j)) (BiconeHom.right j) (BiconeHom.right j))

Tactic:
simp only [diagram.injEq]

Premises used: CategoryTheory.BiconeHom.diagram.injEq
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f f_1 : j ⟶ k
diagram : Decidable (f = f_1)
⊢ Decidable (BiconeHom.diagram f = BiconeHom.diagram f_1)

Tactic:
simp only [diagram.injEq]

Premises used: CategoryTheory.BiconeHom.diagram.injEq
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ Decidable True

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : J
⊢ Decidable True

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f f_1 : j ⟶ k
⊢ Decidable (f = f_1)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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
diagram :
  {j k : J} → (f : j ⟶ k) → (g : BiconeHom.{v₁, u₁} J (Bicone.diagram k) Z) → BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z
⊢ BiconeHom.{v₁, u₁} J X Z

Tactic:
rcases f with (_ | _ | _ | _ | f)
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
g : BiconeHom.{v₁, u₁} J Bicone.left Z
⊢ BiconeHom.{v₁, u₁} J Bicone.left Z

Tactic:
exact g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
g : BiconeHom.{v₁, u₁} J Bicone.right Z
⊢ BiconeHom.{v₁, u₁} J Bicone.right Z

Tactic:
exact g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j : J
g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z
left : {k : J} → (j ⟶ k) → BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram k)
⊢ BiconeHom.{v₁, u₁} J Bicone.left Z

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f : j ⟶ k
⊢ BiconeHom.{v₁, u₁} J Bicone.left (Bicone.diagram k)

Tactic:
apply BiconeHom.left

Premises used: CategoryTheory.BiconeHom.left
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
Z : Bicone J
j : J
g : BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z
right : {k : J} → (j ⟶ k) → BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram k)
⊢ BiconeHom.{v₁, u₁} J Bicone.right Z

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f : j ⟶ k
⊢ BiconeHom.{v₁, u₁} J Bicone.right (Bicone.diagram k)

Tactic:
apply BiconeHom.right

Premises used: CategoryTheory.BiconeHom.right
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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
diagram : {k_1 : J} → (g : k ⟶ k_1) → BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k_1)
⊢ BiconeHom.{v₁, u₁} J (Bicone.diagram j) Z

Tactic:
rcases g with (_ | _ | _ | _ | g)
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
f : j ⟶ k
k_1 : J
g : k ⟶ k_1
⊢ BiconeHom.{v₁, u₁} J (Bicone.diagram j) (Bicone.diagram k_1)

Tactic:
exact BiconeHom.diagram (f ≫ g)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.BiconeHom.diagram
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
diagram : ∀ {j k : J} (f : j ⟶ k), 𝟙 (Bicone.diagram j) ≫ BiconeHom.diagram f = BiconeHom.diagram f
⊢ 𝟙 X ≫ f = f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Bicones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
⊢ Eq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (𝟙 Bicone.left ≫ BiconeHom.left_id) BiconeHom.left_id

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) (𝟙 Bicone.right ≫ 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.left ⟶ Bicone.diagram j) (𝟙 Bicone.left ≫ BiconeHom.left j) (BiconeHom.left j)

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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Bicones
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)
diagram : ∀ {j k : J} (f : j ⟶ k), BiconeHom.diagram f ≫ 𝟙 (Bicone.diagram k) = BiconeHom.diagram f
⊢ f ≫ 𝟙 Y = f

Tactic:
cases f
-- 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 ≫ 𝟙 Bicone.left) BiconeHom.left_id

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 ≫ 𝟙 Bicone.right)
    BiconeHom.right_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 j ≫ 𝟙 (Bicone.diagram j)) (BiconeHom.left j)

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 j ≫ 𝟙 (Bicone.diagram j)) (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
⊢ BiconeHom.diagram f ≫ 𝟙 (Bicone.diagram k) = BiconeHom.diagram f

Tactic:
simp