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
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'
rw :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
rw₁ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprod.desc (F.map coprod.inl) (F.map coprod.inr)))
rw₂ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map f ≫ F.map coprod.inl) (F.map g ≫ F.map coprod.inr))
⊢ Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprodComparison F A B) (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
have rw₃ : Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
  (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
    (F.map (coprod.map f g)))
  (coprod.desc (F.map (f ≫ coprod.inl)) (F.map g ≫ F.map coprod.inr))
Tactic: rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp,
    coprod.desc_comp, ← F.map_comp, coprod.inl_map, ← F.map_comp, coprod.inr_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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'
rw :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
rw₁ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprod.desc (F.map coprod.inl) (F.map coprod.inr)))
rw₂ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map f ≫ F.map coprod.inl) (F.map g ≫ F.map coprod.inr))
rw₃ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map (f ≫ coprod.inl)) (F.map g ≫ F.map coprod.inr))
⊢ Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprodComparison F A B) (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
have rw₄ : Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
  (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
    (F.map (coprod.map f g)))
  (coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr)))
Tactic: rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp,
    coprod.desc_comp, ← F.map_comp, coprod.inl_map, ← F.map_comp, coprod.inr_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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'
rw :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
rw₁ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprod.desc (F.map coprod.inl) (F.map coprod.inr)))
rw₂ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map f ≫ F.map coprod.inl) (F.map g ≫ F.map coprod.inr))
rw₃ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map (f ≫ coprod.inl)) (F.map g ≫ F.map coprod.inr))
rw₄ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr)))
⊢ Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprodComparison F A B) (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
have rw₅ : Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
  (coprod.desc (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (F.map coprod.inl) (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (F.map coprod.inr) (F.map (coprod.map f g))))
  (coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr)))
Tactic: rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp,
    coprod.desc_comp, ← F.map_comp, coprod.inl_map, ← F.map_comp, coprod.inr_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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')
⊢ 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')))
have 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))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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))
⊢ 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')))
have 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))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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))
⊢ 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')))
have 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)))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)))
⊢ 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')))
have 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'))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ coprod.map (Hom.left k) (𝟙 g.left) ≫ (Y.coprodObj.obj g).hom = (X.coprodObj.obj g).hom
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ 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)
have 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)
Tactic: rw [coprod.map_desc, Category.id_comp, Over.w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)
⊢ 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)
have 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)
Tactic: rw [coprod.map_desc, Category.id_comp, Over.w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)
⊢ 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)
have rw₂ : Eq (α := Limits.coprod.{v, u} X.left g.left ⟶ A) (coprod.desc X.hom g.hom) (coprod.desc X.hom g.hom)
Tactic: rw [coprod.map_desc, Category.id_comp, Over.w k]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ 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
have h : Hom.left (X.coprodObj.map k ≫ homMk (coprod.map (Hom.left k_1) (𝟙 g.left)) sorry) =
  Hom.left (homMk (coprod.map (Hom.left k_1) (𝟙 f.left)) sorry ≫ Y.coprodObj.map k)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
A : C
X : Over.{v, u} A
⊢ { app := fun (g : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left (𝟙 X)) (𝟙 g.left)) ⋯, naturality := ⋯ } = 𝟙 X.coprodObj
have 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)) sorry, naturality := sorry } x) =
    Hom.left (NatTrans.app (𝟙 X.coprodObj) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ 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 := ⋯ })
have 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)) sorry, naturality := sorry } 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)) sorry, naturality := sorry }
          { app := fun (g_1 : Over.{v, u} A) ↦ homMk (coprod.map (Hom.left g) (𝟙 g_1.left)) sorry, naturality := sorry })
        x))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
⊢ m = I.lift (BinaryFan.swap t)
have h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
Tactic: have h := I.uniq (BinaryFan.swap t) m
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
⊢ m = I.lift (BinaryFan.swap t)
have rw : ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
⊢ Eq (α := (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := j : Discrete WalkingPair })
    (m ≫ s.π.app { as := j }) ((BinaryFan.swap t).π.app { as := j })
have w₁ : Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
  (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
  (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
Tactic: specialize w ⟨WalkingPair.swap j⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
w :
  Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
    (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
    (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
⊢ Eq (α := (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := j : Discrete WalkingPair })
    (m ≫ s.π.app { as := j }) ((BinaryFan.swap t).π.app { as := j })
have left : ∀
  (w :
    Eq (α :=
      t.pt ⟶
        Functor.obj.{0, v, 0, u} (pair Y X)
          { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
      (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
      (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })),
  Eq (α :=
    (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.left }) ((BinaryFan.swap t).π.app { as := WalkingPair.left })
Tactic: cases j
Cleared hypotheses: j, w