awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
inst_4 : IsIso (X := F.obj (prod.{v, u} A B)) (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B)
⊢ Eq (α := prod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj A)
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A B)) (inv (prodComparison F A B)) (F.map prod.fst)) prod.fst

Tactic:
simp [IsIso.inv_comp_eq]

Premises used: CategoryTheory.IsIso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
inst_4 : IsIso (X := F.obj (prod.{v, u} A B)) (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B)
⊢ Eq (α := prod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj B)
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A B)) (inv (prodComparison F A B)) (F.map prod.snd)) prod.snd

Tactic:
simp [IsIso.inv_comp_eq]

Premises used: CategoryTheory.IsIso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A A' B B' : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{v, u} A' B'
inst_4 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
inst_5 : HasBinaryProduct.{w, u₂} (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst_6 : IsIso (X := F.obj (prod.{v, u} A B)) (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B)
inst_7 : IsIso (X := F.obj (prod.{v, u} A' B')) (Y := prod.{w, u₂} (F.obj A') (F.obj B')) (prodComparison F A' B')
rw :
  Eq (α := prod.{w, u₂} (F.obj A) (F.obj B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B'))
      (CategoryStruct.comp (Y := F.obj (prod.{v, u} A B)) (inv (prodComparison F A B)) (F.map (prod.map f g)))
      (prodComparison F A' B'))
    (prod.map (F.map f) (F.map g))
rw₁ :
  Eq (α := prod.{w, u₂} (F.obj A) (F.obj B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A B)) (inv (prodComparison F A B))
      (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (prodComparison F A' B')))
    (prod.map (F.map f) (F.map g))
rw₂ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (prodComparison F A' B'))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (F.map f) (F.map g)))
rw₃ rw₄ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (F.map f) (F.map g)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (F.map f) (F.map g)))
⊢ Eq (α := prod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (prod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A B)) (inv (prodComparison F A B)) (F.map (prod.map f g)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A') (F.obj B')) (prod.map (F.map f) (F.map g))
      (inv (prodComparison F A' B')))

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.Limits.prodComparison_natural
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{w, u₂} D
E : Type u₃
inst_2 : Category.{w', u₃} E
F : Functor.{v, w, u, u₂} C D
G : Functor.{w, w', u₂, u₃} D E
A_1 A' B B' : C
inst_3 : HasBinaryProduct.{v, u} A_1 B
inst_4 : HasBinaryProduct.{v, u} A' B'
inst_5 : HasBinaryProduct.{w, u₂} (F.obj A_1) (F.obj B)
inst_6 : HasBinaryProduct.{w, u₂} (F.obj A') (F.obj B')
inst_7 : HasBinaryProduct.{w', u₃} (G.obj (F.obj A_1)) (G.obj (F.obj B))
inst_8 : HasBinaryProduct.{w', u₃} ((F ⋙ G).obj A_1) ((F ⋙ G).obj B)
inst_9 : HasBinaryProducts.{v, u} C
inst_10 : HasBinaryProducts.{w, u₂} D
A : C
inst_11 : ∀ (B : C), IsIso (X := F.obj (prod.{v, u} A B)) (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B)
refine :
  IsIso (C := Functor.{v, w, u, u₂} C D) (X := Functor.obj prod.functor A ⋙ F) (Y :=
    F ⋙ Functor.obj prod.functor (F.obj A)) { app := fun (B : C) ↦ prodComparison F A B, naturality := ⋯ }
⊢ Functor.obj prod.functor A ⋙ F ≅ F ⋙ Functor.obj prod.functor (F.obj A)

Tactic:
refine { @asIso _ _ _ _ _ (?_) with hom := prodComparisonNatTrans F A }

Premises used: CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{w, u₂} D
E : Type u₃
inst_2 : Category.{w', u₃} E
F : Functor.{v, w, u, u₂} C D
G : Functor.{w, w', u₂, u₃} D E
A_1 A' B B' : C
inst_3 : HasBinaryProduct.{v, u} A_1 B
inst_4 : HasBinaryProduct.{v, u} A' B'
inst_5 : HasBinaryProduct.{w, u₂} (F.obj A_1) (F.obj B)
inst_6 : HasBinaryProduct.{w, u₂} (F.obj A') (F.obj B')
inst_7 : HasBinaryProduct.{w', u₃} (G.obj (F.obj A_1)) (G.obj (F.obj B))
inst_8 : HasBinaryProduct.{w', u₃} ((F ⋙ G).obj A_1) ((F ⋙ G).obj B)
inst_9 : HasBinaryProducts.{v, u} C
inst_10 : HasBinaryProducts.{w, u₂} D
A : C
inst_11 : ∀ (B : C), IsIso (X := F.obj (prod.{v, u} A B)) (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B)
⊢ IsIso (C := Functor.{v, w, u, u₂} C D) (X := Functor.obj prod.functor A ⋙ F) (Y :=
    F ⋙ Functor.obj prod.functor (F.obj A)) { app := fun (B : C) ↦ prodComparison F A B, naturality := ⋯ }

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
E : Type u₃
inst_2 : Category.{w', u₃} E
F : Functor.{v, w, u, u₂} C D
G : Functor.{w, w', u₂, u₃} D E
A B : C
inst_3 : HasBinaryProduct.{v, u} A B
inst_4 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
inst_5 : HasBinaryProduct.{w', u₃} (G.obj (F.obj A)) (G.obj (F.obj B))
inst_6 : HasBinaryProduct.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B)
unfold :
  Eq (α := (F ⋙ G).obj (prod.{v, u} A B) ⟶ prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
    (prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd))
    (CategoryStruct.comp (Y := G.obj (prod.{w, u₂} (F.obj A) (F.obj B)))
      (G.map (prod.lift (F.map prod.fst) (F.map prod.snd))) (prod.lift (G.map prod.fst) (G.map prod.snd)))
⊢ Eq (α := (F ⋙ G).obj (prod.{v, u} A B) ⟶ prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B)) (prodComparison (F ⋙ G) A B)
    (CategoryStruct.comp (Y := G.obj (prod.{w, u₂} (F.obj A) (F.obj B))) (G.map (prodComparison F A B))
      (prodComparison G (F.obj A) (F.obj B)))

Tactic:
unfold prodComparison

Premises used: CategoryTheory.Limits.prodComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
E : Type u₃
inst_2 : Category.{w', u₃} E
F : Functor.{v, w, u, u₂} C D
G : Functor.{w, w', u₂, u₃} D E
A B : C
inst_3 : HasBinaryProduct.{v, u} A B
inst_4 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
inst_5 : HasBinaryProduct.{w', u₃} (G.obj (F.obj A)) (G.obj (F.obj B))
inst_6 : HasBinaryProduct.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B)
h₁ :
  Eq (α := (F ⋙ G).obj (prod.{v, u} A B) ⟶ (F ⋙ G).obj A)
    (CategoryStruct.comp (Y := prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd)) prod.fst)
    (CategoryStruct.comp (Y := prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (CategoryStruct.comp (Y := G.obj (prod.{w, u₂} (F.obj A) (F.obj B)))
        (G.map (prod.lift (F.map prod.fst) (F.map prod.snd))) (prod.lift (G.map prod.fst) (G.map prod.snd)))
      prod.fst)
h₂ :
  Eq (α := (F ⋙ G).obj (prod.{v, u} A B) ⟶ (F ⋙ G).obj B)
    (CategoryStruct.comp (Y := prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd)) prod.snd)
    (CategoryStruct.comp (Y := prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (CategoryStruct.comp (Y := G.obj (prod.{w, u₂} (F.obj A) (F.obj B)))
        (G.map (prod.lift (F.map prod.fst) (F.map prod.snd))) (prod.lift (G.map prod.fst) (G.map prod.snd)))
      prod.snd)
⊢ Eq (α := (F ⋙ G).obj (prod.{v, u} A B) ⟶ prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
    (prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd))
    (CategoryStruct.comp (Y := G.obj (prod.{w, u₂} (F.obj A) (F.obj B)))
      (G.map (prod.lift (F.map prod.fst) (F.map prod.snd))) (prod.lift (G.map prod.fst) (G.map prod.snd)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
E : Type u₃
inst_2 : Category.{w', u₃} E
F : Functor.{v, w, u, u₂} C D
G : Functor.{w, w', u₂, u₃} D E
A B : C
inst_3 : HasBinaryProduct.{v, u} A B
inst_4 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
inst_5 : HasBinaryProduct.{w', u₃} (G.obj (F.obj A)) (G.obj (F.obj B))
inst_6 : HasBinaryProduct.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ Eq (α := (F ⋙ G).obj (prod.{v, u} A B) ⟶ (F ⋙ G).obj A)
    (CategoryStruct.comp (Y := prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd)) prod.fst)
    (CategoryStruct.comp (Y := prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (CategoryStruct.comp (Y := G.obj (prod.{w, u₂} (F.obj A) (F.obj B)))
        (G.map (prod.lift (F.map prod.fst) (F.map prod.snd))) (prod.lift (G.map prod.fst) (G.map prod.snd)))
      prod.fst)

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
E : Type u₃
inst_2 : Category.{w', u₃} E
F : Functor.{v, w, u, u₂} C D
G : Functor.{w, w', u₂, u₃} D E
A B : C
inst_3 : HasBinaryProduct.{v, u} A B
inst_4 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
inst_5 : HasBinaryProduct.{w', u₃} (G.obj (F.obj A)) (G.obj (F.obj B))
inst_6 : HasBinaryProduct.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ Eq (α := (F ⋙ G).obj (prod.{v, u} A B) ⟶ (F ⋙ G).obj B)
    (CategoryStruct.comp (Y := prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd)) prod.snd)
    (CategoryStruct.comp (Y := prod.{w', u₃} ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (CategoryStruct.comp (Y := G.obj (prod.{w, u₂} (F.obj A) (F.obj B)))
        (G.map (prod.lift (F.map prod.fst) (F.map prod.snd))) (prod.lift (G.map prod.fst) (G.map prod.snd)))
      prod.snd)

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryCoproduct.{v, u} A B
inst_3 : HasBinaryCoproduct.{w, u₂} (F.obj A) (F.obj B)
⊢ Eq (α := F.obj A ⟶ F.obj (coprod.{v, u} A B))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A) (F.obj B)) coprod.inl (coprodComparison F A B))
    (F.map coprod.inl)

Tactic:
coprod.inl_desc _ _

Premises used: CategoryTheory.Limits.coprod.inl_desc, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.coprodComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryCoproduct.{v, u} A B
inst_3 : HasBinaryCoproduct.{w, u₂} (F.obj A) (F.obj B)
⊢ Eq (α := F.obj B ⟶ F.obj (coprod.{v, u} A B))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A) (F.obj B)) coprod.inr (coprodComparison F A B))
    (F.map coprod.inr)

Tactic:
coprod.inr_desc _ _

Premises used: CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.coprod.inr_desc, CategoryTheory.Limits.coprodComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{w, u₂} D
F_1 : Functor.{v, w, u, u₂} C D
A_1 A' B B' : C
inst_2 : HasBinaryCoproduct.{v, u} A_1 B
inst_3 : HasBinaryCoproduct.{v, u} A' B'
inst_4 : HasBinaryCoproduct.{w, u₂} (F_1.obj A_1) (F_1.obj B)
inst_5 : HasBinaryCoproduct.{w, u₂} (F_1.obj A') (F_1.obj B')
inst_6 : HasBinaryCoproducts.{v, u} C
inst_7 : HasBinaryCoproducts.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A f : C
⊢ ∀ ⦃Y : C⦄ (f_1 : f ⟶ Y),
    (F ⋙ Functor.obj coprod.functor (F.obj A)).map f_1 ≫ coprodComparison F A Y =
      coprodComparison F A f ≫ (Functor.obj coprod.functor A ⋙ F).map f_1

Tactic:
simp [coprodComparison_natural]

Premises used: CategoryTheory.Limits.coprodComparison_natural
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryCoproduct.{v, u} A B
inst_3 : HasBinaryCoproduct.{w, u₂} (F.obj A) (F.obj B)
inst_4 : IsIso (X := coprod.{w, u₂} (F.obj A) (F.obj B)) (Y := F.obj (coprod.{v, u} A B)) (coprodComparison F A B)
⊢ Eq (α := F.obj A ⟶ coprod.{w, u₂} (F.obj A) (F.obj B))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (F.map coprod.inl) (inv (coprodComparison F A B))) coprod.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryCoproduct.{v, u} A B
inst_3 : HasBinaryCoproduct.{w, u₂} (F.obj A) (F.obj B)
inst_4 : IsIso (X := coprod.{w, u₂} (F.obj A) (F.obj B)) (Y := F.obj (coprod.{v, u} A B)) (coprodComparison F A B)
⊢ Eq (α := F.obj B ⟶ coprod.{w, u₂} (F.obj A) (F.obj B))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (F.map coprod.inr) (inv (coprodComparison F A B))) coprod.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A A' B B' : C
inst_2 : HasBinaryCoproduct.{v, u} A B
inst_3 : HasBinaryCoproduct.{v, u} A' B'
inst_4 : HasBinaryCoproduct.{w, u₂} (F.obj A) (F.obj B)
inst_5 : HasBinaryCoproduct.{w, u₂} (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst_6 : IsIso (X := coprod.{w, u₂} (F.obj A) (F.obj B)) (Y := F.obj (coprod.{v, u} A B)) (coprodComparison F A B)
inst_7 : IsIso (X := coprod.{w, u₂} (F.obj A') (F.obj B')) (Y := F.obj (coprod.{v, u} A' B')) (coprodComparison F A' B')
rw :
  Eq (α := F.obj (coprod.{v, u} A B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B'))
      (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A) (F.obj B)) (inv (coprodComparison F A B))
        (coprod.map (F.map f) (F.map g)))
      (coprodComparison F A' B'))
    (F.map (coprod.map f g))
rw₁ :
  Eq (α := F.obj (coprod.{v, u} A B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A) (F.obj B)) (inv (coprodComparison F A B))
      (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
        (coprodComparison F A' B')))
    (F.map (coprod.map f g))
rw₂ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprodComparison F A B) (F.map (coprod.map f g)))
rw₃ rw₄ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
⊢ Eq (α := F.obj (coprod.{v, u} A B) ⟶ coprod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A) (F.obj B)) (inv (coprodComparison F A B))
      (coprod.map (F.map f) (F.map g)))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A' B')) (F.map (coprod.map f g)) (inv (coprodComparison F A' B')))

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.Limits.coprodComparison_natural
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X Y : Over.{v, u} A
k : X ⟶ Y
g : Over.{v, u} A
dsimp :
  Eq (α := Limits.coprod.{v, u} X.left g.left ⟶ A)
    (CategoryStruct.comp (Y := Limits.coprod.{v, u} Y.left g.left) (coprod.map (Hom.left k) (𝟙 g.left))
      (coprod.desc Y.hom g.hom))
    (coprod.desc X.hom g.hom)
⊢ coprod.map (Hom.left k) (𝟙 g.left) ≫ (Y.coprodObj.obj g).hom = (X.coprodObj.obj g).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X Y : Over.{v, u} A
k : X ⟶ Y
g : Over.{v, u} A
rw :
  Eq (α := Limits.coprod.{v, u} X.left g.left ⟶ A) (coprod.desc (Hom.left k ≫ Y.hom) (𝟙 g.left ≫ g.hom))
    (coprod.desc X.hom g.hom)
rw₁ :
  Eq (α := Limits.coprod.{v, u} X.left g.left ⟶ A) (coprod.desc (Hom.left k ≫ Y.hom) g.hom) (coprod.desc X.hom g.hom)
rw₂ rw₃ : Eq (α := Limits.coprod.{v, u} X.left g.left ⟶ A) (coprod.desc X.hom g.hom) (coprod.desc X.hom g.hom)
⊢ Eq (α := Limits.coprod.{v, u} X.left g.left ⟶ A)
    (CategoryStruct.comp (Y := Limits.coprod.{v, u} Y.left g.left) (coprod.map (Hom.left k) (𝟙 g.left))
      (coprod.desc Y.hom g.hom))
    (coprod.desc X.hom g.hom)

Tactic:
rw [coprod.map_desc, Category.id_comp, Over.w k]

Premises used: CategoryTheory.Over.w, CategoryTheory.Limits.coprod.map_desc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X Y : Over.{v, u} A
k_1 : X ⟶ Y
f g : Over.{v, u} A
k : f ⟶ g
h :
  Hom.left (X.coprodObj.map k ≫ homMk (coprod.map (Hom.left k_1) (𝟙 g.left)) ⋯) =
    Hom.left (homMk (coprod.map (Hom.left k_1) (𝟙 f.left)) ⋯ ≫ Y.coprodObj.map k)
⊢ X.coprodObj.map k ≫ homMk (coprod.map (Hom.left k_1) (𝟙 g.left)) ⋯ =
    homMk (coprod.map (Hom.left k_1) (𝟙 f.left)) ⋯ ≫ Y.coprodObj.map k

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X Y : Over.{v, u} A
k_1 : X ⟶ Y
f g : Over.{v, u} A
k : f ⟶ g
⊢ Hom.left (X.coprodObj.map k ≫ homMk (coprod.map (Hom.left k_1) (𝟙 g.left)) ⋯) =
    Hom.left (homMk (coprod.map (Hom.left k_1) (𝟙 f.left)) ⋯ ≫ Y.coprodObj.map k)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X : Over.{v, u} A
w :
  ∀ (x : Over.{v, u} A),
    Hom.left
        (NatTrans.app
          { app := fun (g : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left (𝟙 X)) (𝟙 g.left)) ⋯, naturality := ⋯ } x) =
      Hom.left (NatTrans.app (𝟙 X.coprodObj) x)
⊢ { app := fun (g : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left (𝟙 X)) (𝟙 g.left)) ⋯, naturality := ⋯ } = 𝟙 X.coprodObj

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X x : Over.{v, u} A
⊢ Hom.left
      (NatTrans.app
        { app := fun (g : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left (𝟙 X)) (𝟙 g.left)) ⋯, naturality := ⋯ } x) =
    Hom.left (NatTrans.app (𝟙 X.coprodObj) x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X Y Z : Over.{v, u} A
f : X ⟶ Y
g : Y ⟶ Z
w :
  ∀ (x : Over.{v, u} A),
    Eq.{v + 1} (α := (X.coprodObj.obj x).left ⟶ (Z.coprodObj.obj x).left)
      (Hom.left
        (NatTrans.app
          { app := fun (g_1 : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left (f ≫ g)) (𝟙 g_1.left)) ⋯, naturality := ⋯ }
          x))
      (Hom.left
        (NatTrans.app
          (CategoryStruct.comp (Y := Y.coprodObj)
            { app := fun (g : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left f) (𝟙 g.left)) ⋯, naturality := ⋯ }
            { app := fun (g_1 : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left g) (𝟙 g_1.left)) ⋯, naturality := ⋯ })
          x))
⊢ Eq (α := X.coprodObj ⟶ Z.coprodObj)
    { app := fun (g_1 : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left (f ≫ g)) (𝟙 g_1.left)) ⋯, naturality := ⋯ }
    (CategoryStruct.comp (Y := Y.coprodObj)
      { app := fun (g : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left f) (𝟙 g.left)) ⋯, naturality := ⋯ }
      { app := fun (g_1 : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left g) (𝟙 g_1.left)) ⋯, naturality := ⋯ })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X Y Z : Over.{v, u} A
f : X ⟶ Y
g : Y ⟶ Z
x : Over.{v, u} A
⊢ Eq.{v + 1} (α := (X.coprodObj.obj x).left ⟶ (Z.coprodObj.obj x).left)
    (Hom.left
      (NatTrans.app
        { app := fun (g_1 : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left (f ≫ g)) (𝟙 g_1.left)) ⋯, naturality := ⋯ } x))
    (Hom.left
      (NatTrans.app
        (CategoryStruct.comp (Y := Y.coprodObj)
          { app := fun (g : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left f) (𝟙 g.left)) ⋯, naturality := ⋯ }
          { app := fun (g_1 : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left g) (𝟙 g_1.left)) ⋯, naturality := ⋯ })
        x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
π₁ : P ⟶ X
π₂ : P ⟶ Y
⊢ (mk π₁ π₂).op = BinaryCofan.mk π₁.op π₂.op

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
π₁ : op P ⟶ op X
π₂ : op P ⟶ op Y
⊢ BinaryFan.unop (mk π₁ π₂) = BinaryCofan.mk π₁.unop π₂.unop

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
ι₁ : X ⟶ P
ι₂ : Y ⟶ P
⊢ (mk ι₁ ι₂).op = BinaryFan.mk ι₁.op ι₂.op

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
ι₁ : op X ⟶ op P
ι₂ : op Y ⟶ op P
⊢ BinaryCofan.unop (mk ι₁ ι₂) = BinaryFan.mk ι₁.unop ι₂.unop

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryFan.{v, u} X Y
hc : IsLimit c
x : BinaryCofan.{v, u} (op X) (op Y)
⊢ Quiver.Hom.unop
      (c.fst.op ≫
        (fun (s : BinaryCofan.{v, u} (op X) (op Y)) ↦ (Quiver.Hom.op (hc.lift s.unop) : op c.pt ⟶ op s.unop.pt)) x) =
    x.inl.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryFan.{v, u} X Y
hc : IsLimit c
x : BinaryCofan.{v, u} (op X) (op Y)
⊢ Quiver.Hom.unop
      (c.snd.op ≫
        (fun (s : BinaryCofan.{v, u} (op X) (op Y)) ↦ (Quiver.Hom.op (hc.lift s.unop) : op c.pt ⟶ op s.unop.pt)) x) =
    x.inr.unop

Tactic:
simp