awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair })
    ((R.lift (BinaryFan.assocInv P t) ≫
          (BinaryFan.assoc Q s).π.app { as := WalkingPair.right : Discrete WalkingPair }) ≫
        sYZ.π.app { as := WalkingPair.right : Discrete WalkingPair } :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := sYZ.pt)
        (t.π.app { as := WalkingPair.right } :
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) t.pt)
              { as := WalkingPair.right : Discrete WalkingPair } ⟶
            Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.right : Discrete WalkingPair })
        (sYZ.π.app { as := WalkingPair.right }) :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
⊢ (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)

Tactic:
have h := R.uniq (BinaryFan.assocInv P t) m
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
rw : ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j
⊢ m = R.lift (BinaryFan.assocInv P t)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
left :
  ∀ (j : Discrete WalkingPair),
    Eq (α := (BinaryFan.assocInv P t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) j)
      ((m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app j)
      ((BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app j)
⊢ Eq (α :=
    (BinaryFan.assocInv P t).pt ⟶
      Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.left }) ((BinaryFan.assocInv P t).π.app { as := WalkingPair.left })

Tactic:
apply P.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ Eq (α :=
    (BinaryFan.assocInv P t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := sXY.pt)
      (m ≫ s.π.app { as := WalkingPair.left } :
        (BinaryFan.assocInv P t).pt ⟶
          Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.left : Discrete WalkingPair })
      (sXY.π.app { as := WalkingPair.left }))
    (CategoryStruct.comp (Y := sXY.pt)
      ((BinaryFan.assocInv P t).π.app { as := WalkingPair.left } :
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) (BinaryFan.assocInv P t).pt)
            { as := WalkingPair.left : Discrete WalkingPair } ⟶
          Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.left : Discrete WalkingPair })
      (sXY.π.app { as := WalkingPair.left }))

Tactic:
simpa using w ⟨.left⟩

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app { as := WalkingPair.right }

Tactic:
simpa using w ⟨.right⟩

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app { as := WalkingPair.right }

Tactic:
replace w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app ⟨.right⟩ := by
          simpa using w ⟨.right⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app { as := WalkingPair.right }
⊢ Eq (α :=
    (BinaryFan.assocInv P t).pt ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := sXY.pt)
      (m ≫ s.π.app { as := WalkingPair.left } :
        (BinaryFan.assocInv P t).pt ⟶
          Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.left : Discrete WalkingPair })
      (sXY.π.app { as := WalkingPair.right }))
    (CategoryStruct.comp (Y := sXY.pt)
      ((BinaryFan.assocInv P t).π.app { as := WalkingPair.left } :
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) (BinaryFan.assocInv P t).pt)
            { as := WalkingPair.left : Discrete WalkingPair } ⟶
          Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.left : Discrete WalkingPair })
      (sXY.π.app { as := WalkingPair.right }))

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app { as := WalkingPair.right }

Tactic:
replace w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app ⟨.right⟩ := by
        simpa using w ⟨.right⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app { as := WalkingPair.right }
⊢ Eq (α :=
    (BinaryFan.assocInv P t).pt ⟶
      Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.right }) ((BinaryFan.assocInv P t).π.app { as := WalkingPair.right })

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} s.pt X
Q : IsLimit t
apply :
  ∀ (j : Discrete WalkingPair),
    (t.snd ≫
          Q.lift
            (mk
              (P.lift
                { pt := X,
                  π :=
                    { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                      NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                  Cone.{0, v, 0, u} (Functor.empty C) })
              (𝟙
                (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
                  { pt := X,
                    π :=
                      { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                    Cone.{0, v, 0, u} (Functor.empty C) })))) ≫
        t.π.app j =
      𝟙 t.pt ≫ t.π.app j
⊢ t.snd ≫
      Q.lift
        (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } })
          (𝟙
            (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
              { pt := X,
                π :=
                  { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                    NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                Cone.{0, v, 0, u} (Functor.empty C) }))) =
    𝟙 t.pt

Tactic:
apply Q.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} s.pt X
Q : IsLimit t
left :
  ∀ (j : Discrete PEmpty.{1}),
    Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (Functor.empty C) j)
      (((t.snd ≫
            Q.lift
              (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } })
                (𝟙
                  (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
                    { pt := X,
                      π :=
                        { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                          NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                      Cone.{0, v, 0, u} (Functor.empty C) })))) ≫
          t.π.app { as := WalkingPair.left : Discrete WalkingPair }) ≫
        s.π.app j)
      ((𝟙 t.pt ≫ t.π.app { as := WalkingPair.left }) ≫ s.π.app j)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair s.pt X) { as := WalkingPair.left : Discrete WalkingPair })
    ((t.snd ≫
        Q.lift
          (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } })
            (𝟙
              (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
                { pt := X,
                  π :=
                    { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                      NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                  Cone.{0, v, 0, u} (Functor.empty C) })))) ≫
      t.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (𝟙 t.pt ≫ t.π.app { as := WalkingPair.left })

Tactic:
apply P.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} s.pt X
Q : IsLimit t
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair s.pt X) { as := WalkingPair.right : Discrete WalkingPair })
    ((t.snd ≫
        Q.lift
          (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } })
            (𝟙
              (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
                { pt := X,
                  π :=
                    { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                      NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                  Cone.{0, v, 0, u} (Functor.empty C) })))) ≫
      t.π.app { as := WalkingPair.right : Discrete WalkingPair })
    (𝟙 t.pt ≫ t.π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} X s.pt
Q : IsLimit t
apply :
  ∀ (j : Discrete WalkingPair),
    (t.fst ≫
          Q.lift
            (mk (𝟙 X)
              (P.lift
                { pt := X,
                  π :=
                    { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                      NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                  Cone.{0, v, 0, u} (Functor.empty C) }))) ≫
        t.π.app j =
      𝟙 t.pt ≫ t.π.app j
⊢ t.fst ≫
      Q.lift
        (mk (𝟙 X) (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } })) =
    𝟙 t.pt

Tactic:
apply Q.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} X s.pt
Q : IsLimit t
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X s.pt) { as := WalkingPair.left : Discrete WalkingPair })
    ((t.fst ≫
        Q.lift
          (mk (𝟙 X) (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } }))) ≫
      t.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (𝟙 t.pt ≫ t.π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} X s.pt
Q : IsLimit t
right :
  ∀ (j : Discrete PEmpty.{1}),
    Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (Functor.empty C) j)
      (((t.fst ≫
            Q.lift
              (mk (𝟙 X)
                (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } }))) ≫
          t.π.app { as := WalkingPair.right : Discrete WalkingPair }) ≫
        s.π.app j)
      ((𝟙 t.pt ≫ t.π.app { as := WalkingPair.right }) ≫ s.π.app j)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X s.pt) { as := WalkingPair.right : Discrete WalkingPair })
    ((t.fst ≫
        Q.lift
          (mk (𝟙 X) (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } }))) ≫
      t.π.app { as := WalkingPair.right : Discrete WalkingPair })
    (𝟙 t.pt ≫ t.π.app { as := WalkingPair.right })

Tactic:
apply P.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
j : J
⊢ B.ι j ≫ B.π j = 𝟙 (F j)

Tactic:
simpa using B.ι_π j j

Premises used: CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
j j' : J
h : j ≠ j'
⊢ B.ι j ≫ B.π j' = 0

Tactic:
simpa [h] using B.ι_π j j'

Premises used: CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
c c' : Bicone.{w, uC', uC} F
f g : c ⟶ c'
w : f.hom = g.hom
mk :
  ∀ (hom : c.pt ⟶ c'.pt) (wπ : ∀ (j : J), hom ≫ c'.π j = c.π j) (wι : ∀ (j : J), c.ι j ≫ hom = c'.ι j)
    (w : { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' }.hom = g.hom),
    { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
c c' : Bicone.{w, uC', uC} F
g : c ⟶ c'
hom : c.pt ⟶ c'.pt
wπ : ∀ (j : J), hom ≫ c'.π j = c.π j
wι : ∀ (j : J), c.ι j ≫ hom = c'.ι j
w : { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' }.hom = g.hom
mk :
  ∀ (hom_1 : c.pt ⟶ c'.pt) (wπ_1 : ∀ (j : J), hom_1 ≫ c'.π j = c.π j) (wι_1 : ∀ (j : J), c.ι j ≫ hom_1 = c'.ι j)
    (w : { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' }.hom = { hom := hom_1, wπ := wπ_1, wι := wι_1 }.hom),
    { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' } = { hom := hom_1, wπ := wπ_1, wι := wι_1 }
⊢ { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' } = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
c c' : Bicone.{w, uC', uC} F
hom : c.pt ⟶ c'.pt
wπ : ∀ (j : J), hom ≫ c'.π j = c.π j
wι : ∀ (j : J), c.ι j ≫ hom = c'.ι j
hom_1 : c.pt ⟶ c'.pt
wπ_1 : ∀ (j : J), hom_1 ≫ c'.π j = c.π j
wι_1 : ∀ (j : J), c.ι j ≫ hom_1 = c'.ι j
w : { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' }.hom = { hom := hom_1, wπ := wπ_1, wι := wι_1 }.hom
⊢ { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' } = { hom := hom_1, wπ := wπ_1, wι := wι_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
F : J → C
G : Functor.{uC', uD', uC, uD} C D
inst_4 : G.PreservesZeroMorphisms
A : Bicone.{w, uC', uC} F
i j : J
rw :
  Eq (α := G.obj (F i) ⟶ G.obj (F j)) (G.map (if h : i = j then eqToHom ⋯ else 0)) (if h : i = j then eqToHom ⋯ else 0)
⊢ G.map (A.ι i ≫ A.π j) = if h : i = j then eqToHom ⋯ else 0

Tactic:
rw [A.ι_π]

Premises used: CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
F : J → C
G : Functor.{uC', uD', uC, uD} C D
inst_4 : G.PreservesZeroMorphisms
X Y : Bicone.{w, uC', uC} F
f : X ⟶ Y
j : J
⊢ Eq (α :=
    Bicone.pt.{w, uD', uD} (J := J) (F := G.obj ∘ F)
        { pt := G.obj X.pt, π := fun (j : J) ↦ G.map (X.π j), ι := fun (j : J) ↦ G.map (X.ι j), ι_π := ⋯ :
          Bicone.{w, uD', uD} (G.obj ∘ F) } ⟶
      (G.obj ∘ F) j)
    (G.map f.hom ≫
      Bicone.π { pt := G.obj Y.pt, π := fun (j : J) ↦ G.map (Y.π j), ι := fun (j : J) ↦ G.map (Y.ι j), ι_π := ⋯ } j)
    (Bicone.π { pt := G.obj X.pt, π := fun (j : J) ↦ G.map (X.π j), ι := fun (j : J) ↦ G.map (X.ι j), ι_π := ⋯ } j)

Tactic:
simp [-BiconeMorphism.wπ, ← f.wπ j]

Premises used: CategoryTheory.Limits.BiconeMorphism.wπ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
F : J → C
G : Functor.{uC', uD', uC, uD} C D
inst_4 : G.PreservesZeroMorphisms
X Y : Bicone.{w, uC', uC} F
f : X ⟶ Y
j : J
⊢ Eq.{uD' + 1} (α :=
    (G.obj ∘ F) j ⟶
      Bicone.pt.{w, uD', uD} (J := J) (F := G.obj ∘ F)
        { pt := G.obj Y.pt, π := fun (j : J) ↦ G.map (Y.π j), ι := fun (j : J) ↦ G.map (Y.ι j), ι_π := ⋯ })
    (Bicone.ι { pt := G.obj X.pt, π := fun (j : J) ↦ G.map (X.π j), ι := fun (j : J) ↦ G.map (X.ι j), ι_π := ⋯ } j ≫
      G.map f.hom)
    (Bicone.ι { pt := G.obj Y.pt, π := fun (j : J) ↦ G.map (Y.π j), ι := fun (j : J) ↦ G.map (Y.ι j), ι_π := ⋯ } j)

Tactic:
simp [-BiconeMorphism.wι, ← f.wι j]

Premises used: CategoryTheory.Limits.BiconeMorphism.wι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
F : J → C
G : Functor.{uC', uD', uC, uD} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : G.Full
inst_6 : G.Faithful
X Y : Bicone.{w, uC', uC} F
t : Quiver.Hom (V := Bicone.{w, uD', uD} (G.obj ∘ F)) (obj (functoriality F G) X) (obj (functoriality F G) Y)
j : J
⊢ G.map (G.preimage t.hom ≫ Y.π j) = G.map (X.π j)

Tactic:
simpa using t.wπ j

Premises used: CategoryTheory.Limits.BiconeMorphism.wπ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
F : J → C
G : Functor.{uC', uD', uC, uD} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : G.Full
inst_6 : G.Faithful
X Y : Bicone.{w, uC', uC} F
t : Quiver.Hom (V := Bicone.{w, uD', uD} (G.obj ∘ F)) (obj (functoriality F G) X) (obj (functoriality F G) Y)
j : J
⊢ G.map (X.ι j ≫ G.preimage t.hom) = G.map (Y.ι j)

Tactic:
simpa using t.wι j

Premises used: CategoryTheory.Limits.BiconeMorphism.wι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
⊢ B.toCone.pt = B.pt

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
j : Discrete J
⊢ B.toCone.π.app j = B.π j.as

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
j : J
⊢ B.toCone.π.app { as := j } = B.π j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
j : J
⊢ Fan.proj B.toCone j = B.π j

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fan.proj, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
B : Bicone.{w, uC', uC} F
⊢ B.toCocone.pt = B.pt

Tactic:
rfl

Premises used: rfl