awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : (c.inl ≫ l) ≫ c.inl = 𝟙 X ≫ c.inl
mp : ∀ (e : c.inl ≫ l ≫ c.inl = 𝟙 X ≫ c.inl), c.inl ≫ l ≫ c.inl = c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl
have mp₁ : ∀ (e : c.inl ≫ l ≫ c.inl = c.inl), c.inl ≫ l ≫ c.inl = c.inl
Tactic: rwa [Category.assoc, Category.id_comp] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} X
c : BinaryCofan.{v, u} X Y
⊢ Nonempty (IsColimit c) ↔ IsIso c.inr
have refine : Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk c.inr c.inl))
Tactic: refine Iff.trans ?_ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
⊢ IsColimit (mk (f ≫ c.inl) c.inr)
have desc : (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair } ⟶
    s.pt
Tactic: fapply BinaryCofan.isColimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
desc :
  (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair } ⟶
      s.pt
⊢ IsColimit (mk (f ≫ c.inl) c.inr)
have fac_left : ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
  (f ≫ c.inl) ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inl
Tactic: fapply BinaryCofan.isColimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
desc :
  (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair } ⟶
      s.pt
fac_left :
  ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    (f ≫ c.inl) ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inl
⊢ IsColimit (mk (f ≫ c.inl) c.inr)
have fac_right : ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
  c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inr
Tactic: fapply BinaryCofan.isColimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
desc :
  (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair } ⟶
      s.pt
fac_left :
  ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    (f ≫ c.inl) ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inl
fac_right :
  ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inr
⊢ IsColimit (mk (f ≫ c.inl) c.inr)
have uniq : ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair }))
  (m :
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair } ⟶
      s.pt),
  (f ≫ c.inl) ≫ m = s.inl → c.inr ≫ m = s.inr → m = IsColimit.desc h (inv f ≫ s.inl) s.inr
Tactic: fapply BinaryCofan.isColimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair } ⟶
    s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ m = IsColimit.desc h (inv f ≫ s.inl) s.inr
have uniq : c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
Tactic: apply BinaryCofan.IsColimit.hom_ext h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair } ⟶
    s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
uniq : c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
⊢ m = IsColimit.desc h (inv f ≫ s.inl) s.inr
have uniq₁ : c.inr ≫ m = c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
Tactic: apply BinaryCofan.IsColimit.hom_ext h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair } ⟶
    s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
have uniq : f ≫ c.inl ≫ m = f ≫ c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
Tactic: rw [← cancel_epi f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
x : Discrete WalkingPair
u : WalkingPair
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
        { as := u : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := u : Discrete WalkingPair })
    (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := u })
    (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
      NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := u })
have left : Eq (α :=
  Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
      { as := left : Discrete WalkingPair } ⟶
    Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair })
  (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := left })
  (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
    NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := left })
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
x : Discrete WalkingPair
u : WalkingPair
left :
  Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := WalkingPair.left })
    (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
      NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := WalkingPair.left })
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
        { as := u : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := u : Discrete WalkingPair })
    (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := u })
    (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
      NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := u })
have right : Eq (α :=
  Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
      { as := right : Discrete WalkingPair } ⟶
    Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
  (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := right })
  (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
    NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := right })
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
u : WalkingPair
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := u : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := u } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := u })
have left : Eq (α :=
  Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } ⟶
    Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
  (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := left } ≫
    Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
  (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := left })
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
u : WalkingPair
left :
  Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := WalkingPair.left } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := WalkingPair.left })
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := u : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := u } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := u })
have right : Eq (α :=
  Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair } ⟶
    Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
  (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := right } ≫
    Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
  (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := right })
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := left } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := left })
have left : Eq (α := X ⟶ coprod.{v, u} X Y)
  (colimit.ι (pair X Y) { as := left } ≫ 𝟙 (colimit.{0, 0, v, u} (pair X Y)) : X ⟶ coprod.{v, u} X Y)
  (coprod.inl : X ⟶ coprod.{v, u} X Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := right } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := right })
have right : Eq (α := Y ⟶ coprod.{v, u} X Y)
  (colimit.ι (pair X Y) { as := right } ≫ 𝟙 (colimit.{0, 0, v, u} (pair X Y)) : Y ⟶ coprod.{v, u} X Y)
  (coprod.inr : Y ⟶ coprod.{v, u} X Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
V W X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ Eq (α := V ⟶ prod.{v, u} X Y) (f ≫ lift g h) (lift (f ≫ g) (f ≫ h))
have h₁ : CategoryStruct.comp (Y := prod.{v, u} X Y) (f ≫ lift g h) fst =
  CategoryStruct.comp (Y := prod.{v, u} X Y) (lift (f ≫ g) (f ≫ h)) fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
V W X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
h₁ :
  CategoryStruct.comp (Y := prod.{v, u} X Y) (f ≫ lift g h) fst =
    CategoryStruct.comp (Y := prod.{v, u} X Y) (lift (f ≫ g) (f ≫ h)) fst
⊢ Eq (α := V ⟶ prod.{v, u} X Y) (f ≫ lift g h) (lift (f ≫ g) (f ≫ h))
have h₂ : CategoryStruct.comp (Y := prod.{v, u} X Y) (f ≫ lift g h) snd =
  CategoryStruct.comp (Y := prod.{v, u} X Y) (lift (f ≫ g) (f ≫ h)) snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (prod.{v, u} X Y)
have h₁ : CategoryStruct.comp (Y := prod.{v, u} X Y) (map (𝟙 X) (𝟙 Y)) fst = 𝟙 (prod.{v, u} X Y) ≫ fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
h₁ : CategoryStruct.comp (Y := prod.{v, u} X Y) (map (𝟙 X) (𝟙 Y)) fst = 𝟙 (prod.{v, u} X Y) ≫ fst
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (prod.{v, u} X Y)
have h₂ : CategoryStruct.comp (Y := prod.{v, u} X Y) (map (𝟙 X) (𝟙 Y)) snd = 𝟙 (prod.{v, u} X Y) ≫ snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
⊢ lift fst snd = 𝟙 (prod.{v, u} X Y)
have h₁ : CategoryStruct.comp (Y := prod.{v, u} X Y) (lift fst snd) fst = 𝟙 (prod.{v, u} X Y) ≫ fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
h₁ : CategoryStruct.comp (Y := prod.{v, u} X Y) (lift fst snd) fst = 𝟙 (prod.{v, u} X Y) ≫ fst
⊢ lift fst snd = 𝟙 (prod.{v, u} X Y)
have h₂ : CategoryStruct.comp (Y := prod.{v, u} X Y) (lift fst snd) snd = 𝟙 (prod.{v, u} X Y) ≫ snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
V W X Y Z : C
inst_1 : HasBinaryProduct.{v, u} W X
inst_2 : HasBinaryProduct.{v, u} Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ Eq (α := V ⟶ prod.{v, u} Y Z) (CategoryStruct.comp (Y := prod.{v, u} W X) (lift f g) (map h k)) (lift (f ≫ h) (g ≫ k))
have h₁ : CategoryStruct.comp (Y := prod.{v, u} Y Z) (CategoryStruct.comp (Y := prod.{v, u} W X) (lift f g) (map h k)) fst =
  CategoryStruct.comp (Y := prod.{v, u} Y Z) (lift (f ≫ h) (g ≫ k)) fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
V W X Y Z : C
inst_1 : HasBinaryProduct.{v, u} W X
inst_2 : HasBinaryProduct.{v, u} Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
h₁ :
  CategoryStruct.comp (Y := prod.{v, u} Y Z) (CategoryStruct.comp (Y := prod.{v, u} W X) (lift f g) (map h k)) fst =
    CategoryStruct.comp (Y := prod.{v, u} Y Z) (lift (f ≫ h) (g ≫ k)) fst
⊢ Eq (α := V ⟶ prod.{v, u} Y Z) (CategoryStruct.comp (Y := prod.{v, u} W X) (lift f g) (map h k)) (lift (f ≫ h) (g ≫ k))
have h₂ : CategoryStruct.comp (Y := prod.{v, u} Y Z) (CategoryStruct.comp (Y := prod.{v, u} W X) (lift f g) (map h k)) snd =
  CategoryStruct.comp (Y := prod.{v, u} Y Z) (lift (f ≫ h) (g ≫ k)) snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
inst_1 : HasBinaryProduct.{v, u} W Y
inst_2 : HasBinaryProduct.{v, u} X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ Eq (α := prod.{v, u} W Y ⟶ prod.{v, u} X Z) (lift (fst ≫ g) (snd ≫ g')) (map g g')
have rw : Eq (α := prod.{v, u} W Y ⟶ prod.{v, u} X Z) (CategoryStruct.comp (Y := prod.{v, u} W Y) (lift fst snd) (map g g'))
  (map g g')
Tactic: rw [← prod.lift_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst_1 : HasBinaryProduct.{v, u} A₁ B₁
inst_2 : HasBinaryProduct.{v, u} A₂ B₂
inst_3 : HasBinaryProduct.{v, u} A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ Eq (α := prod.{v, u} A₁ B₁ ⟶ prod.{v, u} A₃ B₃) (CategoryStruct.comp (Y := prod.{v, u} A₂ B₂) (map f g) (map h k))
    (map (f ≫ h) (g ≫ k))
have h₁ : Eq (α := prod.{v, u} A₁ B₁ ⟶ A₃)
  (CategoryStruct.comp (Y := prod.{v, u} A₃ B₃) (CategoryStruct.comp (Y := prod.{v, u} A₂ B₂) (map f g) (map h k)) fst)
  (CategoryStruct.comp (Y := prod.{v, u} A₃ B₃) (map (f ≫ h) (g ≫ k)) fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst_1 : HasBinaryProduct.{v, u} A₁ B₁
inst_2 : HasBinaryProduct.{v, u} A₂ B₂
inst_3 : HasBinaryProduct.{v, u} A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
h₁ :
  Eq (α := prod.{v, u} A₁ B₁ ⟶ A₃)
    (CategoryStruct.comp (Y := prod.{v, u} A₃ B₃) (CategoryStruct.comp (Y := prod.{v, u} A₂ B₂) (map f g) (map h k))
      fst)
    (CategoryStruct.comp (Y := prod.{v, u} A₃ B₃) (map (f ≫ h) (g ≫ k)) fst)
⊢ Eq (α := prod.{v, u} A₁ B₁ ⟶ prod.{v, u} A₃ B₃) (CategoryStruct.comp (Y := prod.{v, u} A₂ B₂) (map f g) (map h k))
    (map (f ≫ h) (g ≫ k))
have h₂ : Eq (α := prod.{v, u} A₁ B₁ ⟶ B₃)
  (CategoryStruct.comp (Y := prod.{v, u} A₃ B₃) (CategoryStruct.comp (Y := prod.{v, u} A₂ B₂) (map f g) (map h k)) snd)
  (CategoryStruct.comp (Y := prod.{v, u} A₃ B₃) (map (f ≫ h) (g ≫ k)) snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Mono f
inst_3 : Mono g
inst_4 : HasBinaryProduct.{v_1, u_1} W X
inst_5 : HasBinaryProduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : Z_1 ⟶ prod.{v_1, u_1} W X
h : Eq (α := Z_1 ⟶ prod.{v_1, u_1} Y Z) (i₁ ≫ map f g) (i₂ ≫ map f g)
⊢ i₁ = i₂
have h₁ : i₁ ≫ fst = i₂ ≫ fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Mono f
inst_3 : Mono g
inst_4 : HasBinaryProduct.{v_1, u_1} W X
inst_5 : HasBinaryProduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : Z_1 ⟶ prod.{v_1, u_1} W X
h : Eq (α := Z_1 ⟶ prod.{v_1, u_1} Y Z) (i₁ ≫ map f g) (i₂ ≫ map f g)
h₁ : i₁ ≫ fst = i₂ ≫ fst
⊢ i₁ = i₂
have h₂ : i₁ ≫ snd = i₂ ≫ snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Mono f
inst_3 : Mono g
inst_4 : HasBinaryProduct.{v_1, u_1} W X
inst_5 : HasBinaryProduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : Z_1 ⟶ prod.{v_1, u_1} W X
h : Eq (α := Z_1 ⟶ prod.{v_1, u_1} Y Z) (i₁ ≫ map f g) (i₂ ≫ map f g)
⊢ i₁ ≫ fst = i₂ ≫ fst
have h₁ : (i₁ ≫ fst) ≫ f = (i₂ ≫ fst) ≫ f
Tactic: rw [← cancel_mono f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Mono f
inst_3 : Mono g
inst_4 : HasBinaryProduct.{v_1, u_1} W X
inst_5 : HasBinaryProduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : Z_1 ⟶ prod.{v_1, u_1} W X
h : Eq (α := Z_1 ⟶ prod.{v_1, u_1} Y Z) (i₁ ≫ map f g) (i₂ ≫ map f g)
⊢ i₁ ≫ snd = i₂ ≫ snd
have h₂ : (i₁ ≫ snd) ≫ g = (i₂ ≫ snd) ≫ g
Tactic: rw [← cancel_mono g]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
V W X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ Eq (α := coprod.{v, u} X Y ⟶ W) (desc g h ≫ f) (desc (g ≫ f) (h ≫ f))
have h₁ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc g h ≫ f) =
  CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc (g ≫ f) (h ≫ f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
V W X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
h₁ :
  CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc g h ≫ f) =
    CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc (g ≫ f) (h ≫ f))
⊢ Eq (α := coprod.{v, u} X Y ⟶ W) (desc g h ≫ f) (desc (g ≫ f) (h ≫ f))
have h₂ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (desc g h ≫ f) =
  CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (desc (g ≫ f) (h ≫ f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (coprod.{v, u} X Y)
have h₁ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (map (𝟙 X) (𝟙 Y)) = inl ≫ 𝟙 (coprod.{v, u} X Y)
Tactic: ext