awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
x : X
hx_1 : x ∈ (colimitCocone F).cocone.pt
hx : ∃ (i : J), x ∈ F.obj i
hsurj :
  ∀ (i : J) (hi : x ∈ F.obj i),
    ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
      Subtype.mk (p := fun (x : X) ↦ x ∈ (colimitCocone F).cocone.pt) x hx_1 =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
          xi
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
    Subtype.mk (p := fun (x : X) ↦ x ∈ (colimitCocone F).cocone.pt) x hx_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        xi

Tactic:
obtain ⟨i, hi⟩ := hx
-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
x : X
hx : x ∈ (colimitCocone F).cocone.pt
i : J
hi : x ∈ F.obj i
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
    Subtype.mk (p := fun (x : X) ↦ x ∈ (colimitCocone F).cocone.pt) x hx =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        xi

Tactic:
⟨i, ⟨x, hi⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
x : X
hx : x ∈ (colimitCocone F).cocone.pt
i : J
hi : x ∈ F.obj i
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
    Subtype.mk (p := fun (x : X) ↦ x ∈ (colimitCocone F).cocone.pt) x hx =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        xi

Tactic:
exact ⟨i, ⟨x, hi⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
i j : J
x : X
hx : x ∈ F.obj i
y : X
hy : y ∈ F.obj j
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj.{w', u, w, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
        i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj j))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) y hy) :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          j))
⊢ x = y

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
i j : J
x : X
hx : x ∈ F.obj i
hy : x ∈ F.obj j
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj.{w', u, w, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
        i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj j))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) x hy) :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          j))
⊢ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map f) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
              (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
        (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map g) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) x hy) :
        (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))

Tactic:
⟨IsFiltered.max i j, IsFiltered.leftToMax i j, IsFiltered.rightToMax i j, rfl⟩

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.IsFiltered.max, Exists.intro, CategoryTheory.IsFiltered.leftToMax, rfl
-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
i j : J
x : X
hx : x ∈ F.obj i
hy : x ∈ F.obj j
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj.{w', u, w, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
        i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj j))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) x hy) :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{w', u, w, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
          j))
⊢ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map f) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
              (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj i) x hx) :
        (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map g) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          (Subtype.mk (p := fun (x : X) ↦ x ∈ F.obj j) x hy) :
        (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))

Tactic:
exact ⟨IsFiltered.max i j, IsFiltered.leftToMax i j, IsFiltered.rightToMax i j, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c c' : BinaryBicone.{uC', uC} P Q
f g : c ⟶ c'
w : f.hom = g.hom
mk :
  ∀ (hom : c.pt ⟶ c'.pt) (wfst : hom ≫ c'.fst = c.fst) (wsnd : hom ≫ c'.snd = c.snd) (winl : c.inl ≫ hom = c'.inl)
    (winr : c.inr ≫ hom = c'.inr)
    (w :
      { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' }.hom = g.hom),
    { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c c' : BinaryBicone.{uC', uC} P Q
g : c ⟶ c'
hom : c.pt ⟶ c'.pt
wfst : hom ≫ c'.fst = c.fst
wsnd : hom ≫ c'.snd = c.snd
winl : c.inl ≫ hom = c'.inl
winr : c.inr ≫ hom = c'.inr
w : { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' }.hom = g.hom
mk :
  ∀ (hom_1 : c.pt ⟶ c'.pt) (wfst_1 : hom_1 ≫ c'.fst = c.fst) (wsnd_1 : hom_1 ≫ c'.snd = c.snd)
    (winl_1 : c.inl ≫ hom_1 = c'.inl) (winr_1 : c.inr ≫ hom_1 = c'.inr)
    (w :
      { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' }.hom =
        { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 }.hom),
    { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' } =
      { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 }
⊢ { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' } = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c c' : BinaryBicone.{uC', uC} P Q
hom : c.pt ⟶ c'.pt
wfst : hom ≫ c'.fst = c.fst
wsnd : hom ≫ c'.snd = c.snd
winl : c.inl ≫ hom = c'.inl
winr : c.inr ≫ hom = c'.inr
hom_1 : c.pt ⟶ c'.pt
wfst_1 : hom_1 ≫ c'.fst = c.fst
wsnd_1 : hom_1 ≫ c'.snd = c.snd
winl_1 : c.inl ≫ hom_1 = c'.inl
winr_1 : c.inr ≫ hom_1 = c'.inr
w :
  { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' }.hom =
    { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 }.hom
⊢ { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr : BinaryBiconeMorphism c c' } =
    { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inl ≫ A.fst) = 𝟙 (F.obj P)
rw₁ : F.map (𝟙 P) = 𝟙 (F.obj P)
rw₂ rw₃ : Eq.{uD' + 1} (α := F.obj P ⟶ F.obj P) (𝟙 (F.obj P)) (𝟙 (F.obj P))
⊢ F.map A.inl ≫ F.map A.fst = 𝟙 (F.obj P)

Tactic:
rw [← F.map_comp, A.inl_fst, F.map_id]

Premises used: CategoryTheory.Limits.BinaryBicone.inl_fst, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inl ≫ A.snd) = 0
rw₁ : Eq (α := F.obj P ⟶ F.obj Q) (F.map 0) 0
rw₂ rw₃ : Eq.{uD' + 1} (α := F.obj P ⟶ F.obj Q) 0 0
⊢ F.map A.inl ≫ F.map A.snd = 0

Tactic:
rw [← F.map_comp, A.inl_snd, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.BinaryBicone.inl_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inr ≫ A.fst) = 0
rw₁ : Eq (α := F.obj Q ⟶ F.obj P) (F.map 0) 0
rw₂ rw₃ : Eq.{uD' + 1} (α := F.obj Q ⟶ F.obj P) 0 0
⊢ F.map A.inr ≫ F.map A.fst = 0

Tactic:
rw [← F.map_comp, A.inr_fst, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.BinaryBicone.inr_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
A : BinaryBicone.{uC', uC} P Q
rw : F.map (A.inr ≫ A.snd) = 𝟙 (F.obj Q)
rw₁ : F.map (𝟙 Q) = 𝟙 (F.obj Q)
rw₂ rw₃ : Eq.{uD' + 1} (α := F.obj Q ⟶ F.obj Q) (𝟙 (F.obj Q)) (𝟙 (F.obj Q))
⊢ F.map A.inr ≫ F.map A.snd = 𝟙 (F.obj Q)

Tactic:
rw [← F.map_comp, A.inr_snd, F.map_id]

Premises used: CategoryTheory.Limits.BinaryBicone.inr_snd, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
X Y : BinaryBicone.{uC', uC} P Q
f : X ⟶ Y
⊢ Eq (α :=
    BinaryBicone.pt
        { pt := F.obj X.pt, fst := F.map X.fst, snd := F.map X.snd, inl := F.map X.inl, inr := F.map X.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone.{uD', uD} (F.obj P) (F.obj Q) } ⟶
      F.obj P)
    (F.map f.hom ≫
      BinaryBicone.fst
        { pt := F.obj Y.pt, fst := F.map Y.fst, snd := F.map Y.snd, inl := F.map Y.inl, inr := F.map Y.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })
    (BinaryBicone.fst
      { pt := F.obj X.pt, fst := F.map X.fst, snd := F.map X.snd, inl := F.map X.inl, inr := F.map X.inr, inl_fst := ⋯,
        inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })

Tactic:
simp [-BinaryBiconeMorphism.wfst, ← f.wfst]

Premises used: CategoryTheory.Limits.BinaryBiconeMorphism.wfst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
X Y : BinaryBicone.{uC', uC} P Q
f : X ⟶ Y
⊢ Eq (α :=
    BinaryBicone.pt
        { pt := F.obj X.pt, fst := F.map X.fst, snd := F.map X.snd, inl := F.map X.inl, inr := F.map X.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone.{uD', uD} (F.obj P) (F.obj Q) } ⟶
      F.obj Q)
    (F.map f.hom ≫
      BinaryBicone.snd
        { pt := F.obj Y.pt, fst := F.map Y.fst, snd := F.map Y.snd, inl := F.map Y.inl, inr := F.map Y.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })
    (BinaryBicone.snd
      { pt := F.obj X.pt, fst := F.map X.fst, snd := F.map X.snd, inl := F.map X.inl, inr := F.map X.inr, inl_fst := ⋯,
        inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })

Tactic:
simp [-BinaryBiconeMorphism.wsnd, ← f.wsnd]

Premises used: CategoryTheory.Limits.BinaryBiconeMorphism.wsnd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
X Y : BinaryBicone.{uC', uC} P Q
f : X ⟶ Y
⊢ Eq (α :=
    F.obj P ⟶
      BinaryBicone.pt
        { pt := F.obj Y.pt, fst := F.map Y.fst, snd := F.map Y.snd, inl := F.map Y.inl, inr := F.map Y.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })
    (BinaryBicone.inl
        { pt := F.obj X.pt, fst := F.map X.fst, snd := F.map X.snd, inl := F.map X.inl, inr := F.map X.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ } ≫
      F.map f.hom)
    (BinaryBicone.inl
      { pt := F.obj Y.pt, fst := F.map Y.fst, snd := F.map Y.snd, inl := F.map Y.inl, inr := F.map Y.inr, inl_fst := ⋯,
        inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })

Tactic:
simp [-BinaryBiconeMorphism.winl, ← f.winl]

Premises used: CategoryTheory.Limits.BinaryBiconeMorphism.winl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
X Y : BinaryBicone.{uC', uC} P Q
f : X ⟶ Y
⊢ Eq (α :=
    F.obj Q ⟶
      BinaryBicone.pt
        { pt := F.obj Y.pt, fst := F.map Y.fst, snd := F.map Y.snd, inl := F.map Y.inl, inr := F.map Y.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })
    (BinaryBicone.inr
        { pt := F.obj X.pt, fst := F.map X.fst, snd := F.map X.snd, inl := F.map X.inl, inr := F.map X.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ } ≫
      F.map f.hom)
    (BinaryBicone.inr
      { pt := F.obj Y.pt, fst := F.map Y.fst, snd := F.map Y.snd, inl := F.map Y.inl, inr := F.map Y.inr, inl_fst := ⋯,
        inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })

Tactic:
simp [-BinaryBiconeMorphism.winr, ← f.winr]

Premises used: CategoryTheory.Limits.BinaryBiconeMorphism.winr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Full
inst_6 : F.Faithful
X Y : BinaryBicone.{uC', uC} P Q
t :
  Quiver.Hom (V := BinaryBicone.{uD', uD} (F.obj P) (F.obj Q)) (obj (functoriality P Q F) X)
    (obj (functoriality P Q F) Y)
⊢ F.map (F.preimage t.hom ≫ Y.fst) = F.map X.fst

Tactic:
simpa using t.wfst

Premises used: CategoryTheory.Limits.BinaryBiconeMorphism.wfst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Full
inst_6 : F.Faithful
X Y : BinaryBicone.{uC', uC} P Q
t :
  Quiver.Hom (V := BinaryBicone.{uD', uD} (F.obj P) (F.obj Q)) (obj (functoriality P Q F) X)
    (obj (functoriality P Q F) Y)
⊢ F.map (F.preimage t.hom ≫ Y.snd) = F.map X.snd

Tactic:
simpa using t.wsnd

Premises used: CategoryTheory.Limits.BinaryBiconeMorphism.wsnd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Full
inst_6 : F.Faithful
X Y : BinaryBicone.{uC', uC} P Q
t :
  Quiver.Hom (V := BinaryBicone.{uD', uD} (F.obj P) (F.obj Q)) (obj (functoriality P Q F) X)
    (obj (functoriality P Q F) Y)
⊢ F.map (X.inl ≫ F.preimage t.hom) = F.map Y.inl

Tactic:
simpa using t.winl

Premises used: CategoryTheory.Limits.BinaryBiconeMorphism.winl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q : C
F : Functor.{uC', uD', uC, uD} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Full
inst_6 : F.Faithful
X Y : BinaryBicone.{uC', uC} P Q
t :
  Quiver.Hom (V := BinaryBicone.{uD', uD} (F.obj P) (F.obj Q)) (obj (functoriality P Q F) X)
    (obj (functoriality P Q F) Y)
⊢ F.map (X.inr ≫ F.preimage t.hom) = F.map Y.inr

Tactic:
simpa using t.winr

Premises used: CategoryTheory.Limits.BinaryBiconeMorphism.winr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ c.toCone.pt = c.pt

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ c.toCone.π.app { as := WalkingPair.left } = c.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ c.toCone.π.app { as := WalkingPair.right } = c.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ BinaryFan.fst c.toCone = c.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ BinaryFan.snd c.toCone = c.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ c.toCocone.pt = c.pt

Tactic:
rfl

Premises used: rfl