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 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)))
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))
⊢ 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))
  (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ 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]
-- 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)))
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))
rw₃ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
    (prod.lift (F.map prod.fst ≫ α.app A) (F.map prod.snd ≫ α.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))
  (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
  (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (F.map prod.snd ≫ α.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)))
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))
rw₃ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
    (prod.lift (F.map prod.fst ≫ α.app A) (F.map prod.snd ≫ α.app B))
rw₄ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (F.map prod.snd ≫ α.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))
  (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
  (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
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 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')
⊢ 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')))
have 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))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_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 : 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))
⊢ 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')))
have 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))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_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 : 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))
⊢ 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')))
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)) (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)))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_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 : 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)))
⊢ 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')))
have 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)))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)
⊢ Functor.obj prod.functor A ⋙ F ≅ F ⋙ Functor.obj prod.functor (F.obj A)
have 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 := sorry }
Tactic: refine { @asIso _ _ _ _ _ (?_) with hom := prodComparisonNatTrans F A }
-- 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
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) ⟶ 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)))
have 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)))
Tactic: unfold prodComparison
-- 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
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) ⟶ 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)))
have 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)
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
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)
⊢ 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)))
have 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)
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 : 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'
⊢ 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)))
  (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 [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'))
⊢ 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)))
  (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)))
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)))
⊢ 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 ≫ F.map 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]