awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
hF :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶
      Limits.prod.{v, u} X₁.tgt X₂.tgt)
    π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)
    π(CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
        (π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F),
      CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
        (π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F))
⊢ Eq (α :=
    Limits.prod.{v, u} (tensorObj (𝒞 := instCategory) X₁ X₂).src (tensorObj (𝒞 := instCategory) Z₁ Z₂).tgt ⟶
      (tensorObj (𝒞 := instCategory) X₁ X₂).tgt)
    (Hom.F ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Hom.F (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
hF :
  Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₁.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.tgt X₂.tgt)
      π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.tgt X₂.tgt)
      π(CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
          (π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F),
        CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
          (π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F))
      π₁)
hF₁ :
  Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₂.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.tgt X₂.tgt)
      π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.tgt X₂.tgt)
      π(CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
          (π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F),
        CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
          (π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F))
      π₂)
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶
      Limits.prod.{v, u} X₁.tgt X₂.tgt)
    π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)
    π(CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
        (π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F),
      CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
        (π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
hF :
  Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₁.tgt)
    (π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
      (π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F))
⊢ Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₁.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.tgt X₂.tgt)
      π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.tgt X₂.tgt)
      π(CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
          (π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F),
        CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
          (π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F))
      π₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
hF :
  Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₂.tgt)
    (π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
      (π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F))
⊢ Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₂.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.tgt X₂.tgt)
      π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.tgt X₂.tgt)
      π(CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
          (π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F),
        CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
          (π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F))
      π₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
hF :
  Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₁.tgt)
    (π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
        π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫
      f₁.F)
⊢ Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₁.tgt)
    (π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
      (π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F))

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
hF :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶
      Limits.prod.{v, u} X₁.src Y₁.tgt)
    π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
      π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F))
⊢ Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₁.tgt)
    (π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
        π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫
      f₁.F)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶
      Limits.prod.{v, u} X₁.src Y₁.tgt)
    π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src Z₁.tgt) (prod.map π₁ π₁)
      π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
hF :
  Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₂.tgt)
    (π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
        π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫
      f₂.F)
⊢ Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₂.tgt)
    (π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
      (π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F))

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
hF :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶
      Limits.prod.{v, u} X₂.src Y₂.tgt)
    π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
      π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F))
⊢ Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶ X₂.tgt)
    (π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
        π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫
      f₂.F)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src X₂.src) (Limits.prod.{v, u} Z₁.tgt Z₂.tgt) ⟶
      Limits.prod.{v, u} X₂.src Y₂.tgt)
    π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₂.src Z₂.tgt) (prod.map π₂ π₂)
      π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hf :
  Eq (α := (tensorObj (𝒞 := instCategory) ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) X).src ⟶ Y.src)
    (Hom.f ((𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) ⊗ₘ f) ≫ Iso.hom (λ_ Y))) (Hom.f (Iso.hom (λ_ X) ≫ f))
hF :
  Eq (α :=
    Limits.prod.{v, u} (tensorObj (𝒞 := instCategory) ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) X).src Y.tgt ⟶
      (tensorObj (𝒞 := instCategory) ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) X).tgt)
    (Hom.F ((𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) ⊗ₘ f) ≫ Iso.hom (λ_ Y))) (Hom.F (Iso.hom (λ_ X) ≫ f))
⊢ Eq (α := tensorObj (𝒞 := instCategory) ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) X ⟶ Y)
    ((𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) ⊗ₘ f) ≫ Iso.hom (λ_ Y)) (Iso.hom (λ_ X) ≫ f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
⊢ Eq (α := (tensorObj (𝒞 := instCategory) ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) X).src ⟶ Y.src)
    (Hom.f ((𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) ⊗ₘ f) ≫ Iso.hom (λ_ Y))) (Hom.f (Iso.hom (λ_ X) ≫ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶
      Limits.prod.{v, u} (terminal.{v, u} C) X.tgt)
    π(terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F)
    π(terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt),
      prod.map π₂ (𝟙 Y.tgt) ≫ f.F)
⊢ Eq (α :=
    Limits.prod.{v, u} (tensorObj (𝒞 := instCategory) ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) X).src Y.tgt ⟶
      (tensorObj (𝒞 := instCategory) ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) X).tgt)
    (Hom.F ((𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) ⊗ₘ f) ≫ Iso.hom (λ_ Y))) (Hom.F (Iso.hom (λ_ X) ≫ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  CategoryStruct.comp (Y := Limits.prod.{v, u} (terminal.{v, u} C) X.tgt)
      π(terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F)
      π₂ =
    CategoryStruct.comp (Y := Limits.prod.{v, u} (terminal.{v, u} C) X.tgt)
      π(terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt),
        prod.map π₂ (𝟙 Y.tgt) ≫ f.F)
      π₂
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶
      Limits.prod.{v, u} (terminal.{v, u} C) X.tgt)
    π(terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F)
    π(terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt),
      prod.map π₂ (𝟙 Y.tgt) ≫ f.F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶ X.tgt) (π(π₁ ≫ π₂, π₂) ≫ f.F)
    (prod.map π₂ (𝟙 Y.tgt) ≫ f.F)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} (terminal.{v, u} C) X.tgt)
      π(terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F)
      π₂ =
    CategoryStruct.comp (Y := Limits.prod.{v, u} (terminal.{v, u} C) X.tgt)
      π(terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt),
        prod.map π₂ (𝟙 Y.tgt) ≫ f.F)
      π₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  Eq.{v + 1} (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶ Limits.prod.{v, u} X.src Y.tgt)
    π(π₁ ≫ π₂, π₂) (prod.map π₂ (𝟙 Y.tgt))
⊢ Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶ X.tgt) (π(π₁ ≫ π₂, π₂) ≫ f.F)
    (prod.map π₂ (𝟙 Y.tgt) ≫ f.F)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  Eq.{v + 1} (α := Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶ X.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) π(π₁ ≫ π₂, π₂) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) (prod.map π₂ (𝟙 Y.tgt)) π₁)
hF₁ :
  Eq.{v + 1} (α := Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶ Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) π(π₁ ≫ π₂, π₂) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) (prod.map π₂ (𝟙 Y.tgt)) π₂)
⊢ Eq.{v + 1} (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶ Limits.prod.{v, u} X.src Y.tgt)
    π(π₁ ≫ π₂, π₂) (prod.map π₂ (𝟙 Y.tgt))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
⊢ Eq.{v + 1} (α := Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶ X.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) π(π₁ ≫ π₂, π₂) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) (prod.map π₂ (𝟙 Y.tgt)) π₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
⊢ Eq.{v + 1} (α := Limits.prod.{v, u} (Limits.prod.{v, u} (terminal.{v, u} C) X.src) Y.tgt ⟶ Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) π(π₁ ≫ π₂, π₂) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) (prod.map π₂ (𝟙 Y.tgt)) π₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hf :
  Eq (α := (tensorObj (𝒞 := instCategory) X ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))).src ⟶ Y.src)
    (Hom.f ((f ⊗ₘ 𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))) ≫ Iso.hom (ρ_ Y))) (Hom.f (Iso.hom (ρ_ X) ≫ f))
hF :
  Eq (α :=
    Limits.prod.{v, u} (tensorObj (𝒞 := instCategory) X ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))).src Y.tgt ⟶
      (tensorObj (𝒞 := instCategory) X ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))).tgt)
    (Hom.F ((f ⊗ₘ 𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))) ≫ Iso.hom (ρ_ Y))) (Hom.F (Iso.hom (ρ_ X) ≫ f))
⊢ Eq (α := tensorObj (𝒞 := instCategory) X ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory)) ⟶ Y)
    ((f ⊗ₘ 𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))) ≫ Iso.hom (ρ_ Y)) (Iso.hom (ρ_ X) ≫ f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
⊢ Eq (α := (tensorObj (𝒞 := instCategory) X ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))).src ⟶ Y.src)
    (Hom.f ((f ⊗ₘ 𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))) ≫ Iso.hom (ρ_ Y))) (Hom.f (Iso.hom (ρ_ X) ≫ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶
      Limits.prod.{v, u} X.tgt (terminal.{v, u} C))
    π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt))
    π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F,
      terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt))
⊢ Eq (α :=
    Limits.prod.{v, u} (tensorObj (𝒞 := instCategory) X ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))).src Y.tgt ⟶
      (tensorObj (𝒞 := instCategory) X ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))).tgt)
    (Hom.F ((f ⊗ₘ 𝟙 ((𝟙_ (Dial.{v, u} C)) (𝒞 := instCategory))) ≫ Iso.hom (ρ_ Y))) (Hom.F (Iso.hom (ρ_ X) ≫ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X.tgt (terminal.{v, u} C))
      π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt))
      π₁ =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X.tgt (terminal.{v, u} C))
      π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F,
        terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt))
      π₁
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶
      Limits.prod.{v, u} X.tgt (terminal.{v, u} C))
    π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt))
    π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F,
      terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶ X.tgt) (π(π₁ ≫ π₁, π₂) ≫ f.F)
    (prod.map π₁ (𝟙 Y.tgt) ≫ f.F)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} X.tgt (terminal.{v, u} C))
      π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt))
      π₁ =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X.tgt (terminal.{v, u} C))
      π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F,
        terminal.from (Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt))
      π₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  Eq.{v + 1} (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶ Limits.prod.{v, u} X.src Y.tgt)
    π(π₁ ≫ π₁, π₂) (prod.map π₁ (𝟙 Y.tgt))
⊢ Eq (α := Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶ X.tgt) (π(π₁ ≫ π₁, π₂) ≫ f.F)
    (prod.map π₁ (𝟙 Y.tgt) ≫ f.F)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
hF :
  Eq.{v + 1} (α := Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶ X.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) π(π₁ ≫ π₁, π₂) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) (prod.map π₁ (𝟙 Y.tgt)) π₁)
hF₁ :
  Eq.{v + 1} (α := Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶ Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) π(π₁ ≫ π₁, π₂) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) (prod.map π₁ (𝟙 Y.tgt)) π₂)
⊢ Eq.{v + 1} (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶ Limits.prod.{v, u} X.src Y.tgt)
    π(π₁ ≫ π₁, π₂) (prod.map π₁ (𝟙 Y.tgt))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
⊢ Eq.{v + 1} (α := Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶ X.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) π(π₁ ≫ π₁, π₂) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) (prod.map π₁ (𝟙 Y.tgt)) π₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
f : X ⟶ Y
⊢ Eq.{v + 1} (α := Limits.prod.{v, u} (Limits.prod.{v, u} X.src (terminal.{v, u} C)) Y.tgt ⟶ Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) π(π₁ ≫ π₁, π₂) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Y.tgt) (prod.map π₁ (𝟙 Y.tgt)) π₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : Dial.{v, u} C
hf :
  Hom.f
      ((Iso.hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫
        Iso.hom (α_ W (tensorObj (𝒞 := instCategory) X Y) Z) ≫ (𝟙 W ⊗ₘ Iso.hom (α_ X Y Z))) =
    (Iso.hom (α_ (tensorObj (𝒞 := instCategory) W X) Y Z) ≫ Iso.hom (α_ W X (tensorObj (𝒞 := instCategory) Y Z))).f
hF :
  Hom.F
      ((Iso.hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫
        Iso.hom (α_ W (tensorObj (𝒞 := instCategory) X Y) Z) ≫ (𝟙 W ⊗ₘ Iso.hom (α_ X Y Z))) =
    (Iso.hom (α_ (tensorObj (𝒞 := instCategory) W X) Y Z) ≫ Iso.hom (α_ W X (tensorObj (𝒞 := instCategory) Y Z))).F
⊢ (Iso.hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫ Iso.hom (α_ W (tensorObj (𝒞 := instCategory) X Y) Z) ≫ (𝟙 W ⊗ₘ Iso.hom (α_ X Y Z)) =
    Iso.hom (α_ (tensorObj (𝒞 := instCategory) W X) Y Z) ≫ Iso.hom (α_ W X (tensorObj (𝒞 := instCategory) Y Z))

Tactic:
ext