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
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
        (Iso.hom (associator X (initial.{v, u} C) Y) :
          coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
        (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
          coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
      coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)
    (map (Iso.hom (rightUnitor X)) (𝟙 Y) : coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)
have h₁ : Eq.{v + 1} (α := X ⟶ coprod.{v, u} X Y)
  (CategoryStruct.comp (Y := coprod.{v, u} X (initial.{v, u} C)) (inl : X ⟶ coprod.{v, u} X (initial.{v, u} C))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
        (inl : coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
        (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
            (Iso.hom (associator X (initial.{v, u} C) Y) :
              coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶
                coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
            (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
              coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
          coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y) :
      coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} X Y))
  (CategoryStruct.comp (Y := coprod.{v, u} X (initial.{v, u} C)) (inl : X ⟶ coprod.{v, u} X (initial.{v, u} C))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y) inl
        (map (Iso.hom (rightUnitor X)) (𝟙 Y)) :
      coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} X Y))
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
inst_2 : HasInitial.{v, u} C
X Y : C
h₁ :
  Eq.{v + 1} (α := X ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} X (initial.{v, u} C)) (inl : X ⟶ coprod.{v, u} X (initial.{v, u} C))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
          (inl : coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
          (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
              (Iso.hom (associator X (initial.{v, u} C) Y) :
                coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶
                  coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
              (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
                coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
            coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y) :
        coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} X Y))
    (CategoryStruct.comp (Y := coprod.{v, u} X (initial.{v, u} C)) (inl : X ⟶ coprod.{v, u} X (initial.{v, u} C))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y) inl
          (map (Iso.hom (rightUnitor X)) (𝟙 Y)) :
        coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} X Y))
⊢ Eq.{v + 1} (α := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
        (Iso.hom (associator X (initial.{v, u} C) Y) :
          coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
        (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
          coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
      coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)
    (map (Iso.hom (rightUnitor X)) (𝟙 Y) : coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)
have h₂ : Eq.{v + 1} (α := Y ⟶ coprod.{v, u} X Y)
  (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
    (inr : Y ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
    (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
        (Iso.hom (associator X (initial.{v, u} C) Y) :
          coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
        (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
          coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
      coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y))
  (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
    (inr : Y ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
    (map (Iso.hom (rightUnitor X)) (𝟙 Y) : coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y))
Tactic: ext
-- 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 : 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'
⊢ 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)))
have 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))
    (prod.lift (F.map prod.fst) (F.map prod.snd)))
  (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (F.map f) (F.map g)))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]
-- 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 : 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'
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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (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 (α := 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)))
have 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))
    (prod.lift (F.map prod.fst) (F.map prod.snd)))
  (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
    (prod.map (F.map f) (F.map g)))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]
-- 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 : 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'
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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (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₁ :
  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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
      (prod.map (F.map f) (F.map g)))
⊢ 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)))
have 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))
    (prod.lift (F.map prod.fst) (F.map prod.snd)))
  (prod.lift (F.map prod.fst ≫ F.map f) (F.map prod.snd ≫ F.map g))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]
-- 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 : 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'
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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (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₁ :
  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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
      (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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map prod.fst ≫ F.map f) (F.map prod.snd ≫ F.map g))
⊢ 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)))
have 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))
    (prod.lift (F.map prod.fst) (F.map prod.snd)))
  (prod.lift (F.map (prod.fst ≫ f)) (F.map prod.snd ≫ F.map g))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]
-- 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 : 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'
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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (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₁ :
  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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
      (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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map prod.fst ≫ F.map f) (F.map prod.snd ≫ 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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map prod.snd ≫ F.map g))
⊢ 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)))
have 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))
    (prod.lift (F.map prod.fst) (F.map prod.snd)))
  (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]
-- 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 : 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'
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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (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₁ :
  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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
      (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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map prod.fst ≫ F.map f) (F.map prod.snd ≫ 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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map prod.snd ≫ 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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
⊢ 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)))
have rw₅ : Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
  (prod.lift (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.fst))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.snd)))
  (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]
-- 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 : 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'
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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (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₁ :
  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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
      (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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map prod.fst ≫ F.map f) (F.map prod.snd ≫ 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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map prod.snd ≫ 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))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
rw₅ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (prod.lift (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.fst))
      (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
⊢ 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)))
have rw₆ : Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
  (prod.lift (F.map (CategoryStruct.comp (Y := prod.{v, u} A' B') (prod.map f g) prod.fst))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.snd)))
  (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]
-- 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 B : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
H : Functor.{v, w, u, u₂} C D
inst_4 : HasBinaryProduct.{w, u₂} (H.obj A) (H.obj B)
α : F ⟶ H
⊢ Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B)) (α.app (prod.{v, u} A B) ≫ prodComparison H A B)
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (α.app A) (α.app B)))
have rw : Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
  (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
  (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (α.app A) (α.app B)))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, prod.comp_lift, α.naturality, α.naturality]
-- 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 B : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
H : Functor.{v, w, u, u₂} C D
inst_4 : HasBinaryProduct.{w, u₂} (H.obj A) (H.obj B)
α : F ⟶ H
rw :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (α.app A) (α.app B)))
⊢ Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B)) (α.app (prod.{v, u} A B) ≫ prodComparison H A B)
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (α.app A) (α.app B)))
have rw₁ : Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
  (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
  (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
    (prod.map (α.app A) (α.app B)))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, prod.comp_lift, α.naturality, α.naturality]
-- 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 B : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
H : Functor.{v, w, u, u₂} C D
inst_4 : HasBinaryProduct.{w, u₂} (H.obj A) (H.obj B)
α : F ⟶ H
rw :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (α.app A) (α.app B)))
rw₁ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
      (prod.map (α.app A) (α.app B)))
⊢ Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B)) (α.app (prod.{v, u} A B) ≫ prodComparison H A B)
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (α.app A) (α.app B)))
have rw₂ : Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
  (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
  (prod.lift (F.map prod.fst ≫ α.app A) (F.map prod.snd ≫ α.app B))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, prod.comp_lift, α.naturality, α.naturality]