awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
f g : W ⟶ prod.{v, u} X Y
h₁ : f ≫ fst = g ≫ fst
h₂ : f ≫ snd = g ≫ snd
⊢ f = g

Tactic:
BinaryFan.IsLimit.hom_ext (limit.isLimit _) h₁ h₂

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
f g : coprod.{v, u} X Y ⟶ W
h₁ : inl ≫ f = inl ≫ g
h₂ : inr ≫ f = inr ≫ g
⊢ f = g

Tactic:
BinaryCofan.IsColimit.hom_ext (colimit.isColimit _) h₁ h₂

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
f : W ⟶ X
g : W ⟶ Y
⊢ CategoryStruct.comp (Y := prod.{v, u} X Y) (lift f g) fst = f

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
f : W ⟶ X
g : W ⟶ Y
⊢ CategoryStruct.comp (Y := prod.{v, u} X Y) (lift f g) snd = g

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
f : X ⟶ W
g : Y ⟶ W
⊢ CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc f g) = f

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
f : X ⟶ W
g : Y ⟶ W
⊢ CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (desc f g) = g

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 W X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
f : W ⟶ X
g : W ⟶ Y
inst_2 : Mono f
⊢ Mono (Y := prod.{v, u} X Y) (lift f g)

Tactic:
mono_of_mono_fac <| prod.lift_fst _ _

Premises used: CategoryTheory.Limits.prod.lift_fst, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 W X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
f : W ⟶ X
g : W ⟶ Y
inst_2 : Mono g
⊢ Mono (Y := prod.{v, u} X Y) (lift f g)

Tactic:
mono_of_mono_fac <| prod.lift_snd _ _

Premises used: CategoryTheory.Limits.prod.lift_snd, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 W X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
f : X ⟶ W
g : Y ⟶ W
inst_2 : Epi f
⊢ Epi (X := coprod.{v, u} X Y) (desc f g)

Tactic:
epi_of_epi_fac <| coprod.inl_desc _ _

Premises used: CategoryTheory.epi_of_epi_fac, CategoryTheory.Limits.coprod.inl_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 W X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
f : X ⟶ W
g : Y ⟶ W
inst_2 : Epi g
⊢ Epi (X := coprod.{v, u} X Y) (desc f g)

Tactic:
epi_of_epi_fac <| coprod.inr_desc _ _

Premises used: CategoryTheory.epi_of_epi_fac, CategoryTheory.Limits.coprod.inr_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
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
⊢ Eq (α := V ⟶ prod.{v, u} X Y) (f ≫ lift g h) (lift (f ≫ g) (f ≫ h))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} Y Y
f : X ⟶ Y
⊢ Eq (α := X ⟶ prod.{v, u} Y Y) (f ≫ diag Y) (lift f f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
inst_1 : HasBinaryProduct.{v, u} W X
inst_2 : HasBinaryProduct.{v, u} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := prod.{v, u} W X ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} Y Z) (map f g) fst) (fst ≫ f)

Tactic:
limMap_π _ _

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Limits.prod.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
inst_1 : HasBinaryProduct.{v, u} W X
inst_2 : HasBinaryProduct.{v, u} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := prod.{v, u} W X ⟶ Z) (CategoryStruct.comp (Y := prod.{v, u} Y Z) (map f g) snd) (snd ≫ g)

Tactic:
limMap_π _ _

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Limits.prod.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
h₂ : CategoryStruct.comp (Y := prod.{v, u} X Y) (map (𝟙 X) (𝟙 Y)) snd = 𝟙 (prod.{v, u} X Y) ≫ snd
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (prod.{v, u} X Y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
⊢ CategoryStruct.comp (Y := prod.{v, u} X Y) (map (𝟙 X) (𝟙 Y)) fst = 𝟙 (prod.{v, u} X Y) ≫ fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
⊢ CategoryStruct.comp (Y := prod.{v, u} X Y) (map (𝟙 X) (𝟙 Y)) snd = 𝟙 (prod.{v, u} X Y) ≫ snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
h₂ : CategoryStruct.comp (Y := prod.{v, u} X Y) (lift fst snd) snd = 𝟙 (prod.{v, u} X Y) ≫ snd
⊢ lift fst snd = 𝟙 (prod.{v, u} X Y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
⊢ CategoryStruct.comp (Y := prod.{v, u} X Y) (lift fst snd) fst = 𝟙 (prod.{v, u} X Y) ≫ fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
⊢ CategoryStruct.comp (Y := prod.{v, u} X Y) (lift fst snd) snd = 𝟙 (prod.{v, u} X Y) ≫ snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
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
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
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')
⊢ Eq (α := prod.{v, u} W Y ⟶ prod.{v, u} X Z) (lift (fst ≫ g) (snd ≫ g')) (map g g')

Tactic:
rw [← prod.lift_map]

Premises used: CategoryTheory.Limits.prod.lift_map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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) (CategoryStruct.comp (Y := prod.{v, u} W Y) (lift fst snd) (map g g'))
    (map g g')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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)
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)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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₁ ⟶ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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₁ ⟶ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst_1 : HasLimitsOfShape.{0, 0, v, u} (Discrete WalkingPair) C
⊢ Eq (α := prod.{v, u} X A ⟶ prod.{v, u} Y B) (CategoryStruct.comp (Y := prod.{v, u} X B) (map (𝟙 X) f) (map g (𝟙 B)))
    (CategoryStruct.comp (Y := prod.{v, u} Y A) (map g (𝟙 A)) (map (𝟙 Y) f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : HasBinaryProduct.{v, u} X W
inst_2 : HasBinaryProduct.{v, u} Z W
inst_3 : HasBinaryProduct.{v, u} Y W
⊢ Eq (α := prod.{v, u} X W ⟶ prod.{v, u} Z W) (map (f ≫ g) (𝟙 W))
    (CategoryStruct.comp (Y := prod.{v, u} Y W) (map f (𝟙 W)) (map g (𝟙 W)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : HasBinaryProduct.{v, u} W X
inst_2 : HasBinaryProduct.{v, u} W Y
inst_3 : HasBinaryProduct.{v, u} W Z
⊢ Eq (α := prod.{v, u} W X ⟶ prod.{v, u} W Z) (map (𝟙 W) (f ≫ g))
    (CategoryStruct.comp (Y := prod.{v, u} W Y) (map (𝟙 W) f) (map (𝟙 W) g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 W X Y Z : C
inst_1 : HasBinaryProduct.{v, u} W X
inst_2 : HasBinaryProduct.{v, u} Y Z
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso f
inst_4 : IsIso g
⊢ IsIso (X := prod.{v, u} W X) (Y := prod.{v, u} Y Z) (prod.map f g)

Tactic:
(prod.mapIso (asIso f) (asIso g)).isIso_hom

Premises used: CategoryTheory.Limits.prod.mapIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap, CategoryTheory.asIso, CategoryTheory.Limits.prod.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
h₂ : i₁ ≫ snd = i₂ ≫ snd
⊢ i₁ = i₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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) ≫ f = (i₂ ≫ fst) ≫ f
⊢ i₁ ≫ fst = i₂ ≫ fst

Tactic:
rw [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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) ≫ f = (i₂ ≫ fst) ≫ f

Tactic:
simpa using congr_arg (fun f => f ≫ prod.fst) h

Premises used: CategoryTheory.Limits.prod.fst, congr_arg, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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₁ ≫ snd) ≫ g = (i₂ ≫ snd) ≫ g
⊢ i₁ ≫ snd = i₂ ≫ snd

Tactic:
rw [← cancel_mono g]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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) ≫ g = (i₂ ≫ snd) ≫ g

Tactic:
simpa using congr_arg (fun f => f ≫ prod.snd) h

Premises used: congr_arg, CategoryTheory.Limits.prod.snd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasBinaryProduct.{v, u} X X
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ Eq (α := X ⟶ prod.{v, u} Y Y) (CategoryStruct.comp (Y := prod.{v, u} X X) (diag X) (map f f)) (f ≫ diag Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
inst_2 : HasBinaryProduct.{v, u} (prod.{v, u} X Y) (prod.{v, u} X Y)
⊢ CategoryStruct.comp (Y := prod.{v, u} (prod.{v, u} X Y) (prod.{v, u} X Y)) (diag (prod.{v, u} X Y)) (map fst snd) =
    𝟙 (prod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfShape.{0, 0, v, u} (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ Eq (α := prod.{v, u} X X' ⟶ prod.{v, u} Y Y')
    (CategoryStruct.comp (Y := prod.{v, u} (prod.{v, u} X X') (prod.{v, u} X X')) (diag (prod.{v, u} X X'))
      (map (fst ≫ g) (snd ≫ g')))
    (map g g')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y X : C
inst_1 : HasBinaryProduct.{v, u} X X
⊢ IsSplitMono.{v, u} (Y := prod.{v, u} X X) (diag X)

Tactic:
IsSplitMono.mk' { retraction := prod.fst }

Premises used: CategoryTheory.Limits.prod.fst, CategoryTheory.SplitMono.mk, CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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))
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))
⊢ Eq (α := coprod.{v, u} X Y ⟶ W) (desc g h ≫ f) (desc (g ≫ f) (h ≫ f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X X
f : X ⟶ Y
⊢ Eq (α := coprod.{v, u} X X ⟶ Y) (codiag X ≫ f) (desc f f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
inst_1 : HasBinaryCoproduct.{v, u} W X
inst_2 : HasBinaryCoproduct.{v, u} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := W ⟶ coprod.{v, u} Y Z) (CategoryStruct.comp (Y := coprod.{v, u} W X) inl (map f g)) (f ≫ inl)

Tactic:
ι_colimMap _ _

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.coprod.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
inst_1 : HasBinaryCoproduct.{v, u} W X
inst_2 : HasBinaryCoproduct.{v, u} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := X ⟶ coprod.{v, u} Y Z) (CategoryStruct.comp (Y := coprod.{v, u} W X) inr (map f g)) (g ≫ inr)

Tactic:
ι_colimMap _ _

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.coprod.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
h₁ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (map (𝟙 X) (𝟙 Y)) = inl ≫ 𝟙 (coprod.{v, u} X Y)
h₂ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (map (𝟙 X) (𝟙 Y)) = inr ≫ 𝟙 (coprod.{v, u} X Y)
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (coprod.{v, u} X Y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
⊢ CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (map (𝟙 X) (𝟙 Y)) = inl ≫ 𝟙 (coprod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
⊢ CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (map (𝟙 X) (𝟙 Y)) = inr ≫ 𝟙 (coprod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
h₁ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc inl inr) = inl ≫ 𝟙 (coprod.{v, u} X Y)
h₂ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (desc inl inr) = inr ≫ 𝟙 (coprod.{v, u} X Y)
⊢ desc inl inr = 𝟙 (coprod.{v, u} X Y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
⊢ CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc inl inr) = inl ≫ 𝟙 (coprod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
⊢ CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (desc inl inr) = inr ≫ 𝟙 (coprod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
S T U V W : C
inst_1 : HasBinaryCoproduct.{v, u} U W
inst_2 : HasBinaryCoproduct.{v, u} T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
h₁ :
  CategoryStruct.comp (Y := coprod.{v, u} T V) inl (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g)) =
    CategoryStruct.comp (Y := coprod.{v, u} T V) inl (desc (h ≫ f) (k ≫ g))
h₂ :
  CategoryStruct.comp (Y := coprod.{v, u} T V) inr (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g)) =
    CategoryStruct.comp (Y := coprod.{v, u} T V) inr (desc (h ≫ f) (k ≫ g))
⊢ Eq (α := coprod.{v, u} T V ⟶ S) (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g))
    (desc (h ≫ f) (k ≫ g))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
S T U V W : C
inst_1 : HasBinaryCoproduct.{v, u} U W
inst_2 : HasBinaryCoproduct.{v, u} T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ CategoryStruct.comp (Y := coprod.{v, u} T V) inl (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g)) =
    CategoryStruct.comp (Y := coprod.{v, u} T V) inl (desc (h ≫ f) (k ≫ g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
S T U V W : C
inst_1 : HasBinaryCoproduct.{v, u} U W
inst_2 : HasBinaryCoproduct.{v, u} T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ CategoryStruct.comp (Y := coprod.{v, u} T V) inr (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g)) =
    CategoryStruct.comp (Y := coprod.{v, u} T V) inr (desc (h ≫ f) (k ≫ g))

Tactic:
simp