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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h₁ :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (C :=
      Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt)))
      (Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)))
      (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) X₁.rel))
    (Functor.obj (C :=
      Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
      (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))))
      (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) X₂.rel))
h₂ :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (C :=
      Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt)))
      (Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)))
      (Functor.obj (Subobject.pullback (prod.map π₂ π₂)) Y₁.rel))
    (Functor.obj (C :=
      Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
      (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))))
      (Functor.obj (Subobject.pullback (prod.map π₂ π₂)) Y₂.rel))
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (C :=
        Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt)))
        (Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)))
        (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) X₁.rel) ⊓
      Functor.obj (C :=
        Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt)))
        (Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)))
        (Functor.obj (Subobject.pullback (prod.map π₂ π₂)) Y₁.rel))
    (Functor.obj (C :=
        Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
        (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))))
        (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) X₂.rel) ⊓
      Functor.obj (C :=
        Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
        (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))))
        (Functor.obj (Subobject.pullback (prod.map π₂ π₂)) Y₂.rel))

Tactic:
apply inf_le_inf

Premises used: inf_le_inf
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h₁ :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y :=
          Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt))
          π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) (prod.map π₁ π₁)))
      X₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y :=
          Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt))
          (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))) (prod.map π₁ π₁)))
      X₂.rel)
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (C :=
      Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt)))
      (Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)))
      (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) X₁.rel))
    (Functor.obj (C :=
      Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
      (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))))
      (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) X₂.rel))

Tactic:
rw [← Subobject.pullback_comp, ← Subobject.pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h₂ :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y :=
          Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt))
          π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) (prod.map π₂ π₂)))
      Y₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y :=
          Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt))
          (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))) (prod.map π₂ π₂)))
      Y₂.rel)
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (C :=
      Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt)))
      (Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)))
      (Functor.obj (Subobject.pullback (prod.map π₂ π₂)) Y₁.rel))
    (Functor.obj (C :=
      Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
      (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))))
      (Functor.obj (Subobject.pullback (prod.map π₂ π₂)) Y₂.rel))

Tactic:
rw [← Subobject.pullback_comp, ← Subobject.pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) (Functor.obj (Subobject.pullback π(π₁, f.F)) X₁.rel))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} X₁.src X₂.tgt)) (Subobject.pullback (prod.map π₁ π₁))
      (Functor.obj (Subobject.pullback (prod.map f.f (𝟙 X₂.tgt))) X₂.rel))

Tactic:
have := (Subobject.pullback (prod.map π₁ π₁ :
        (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le f)
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) (Functor.obj (Subobject.pullback π(π₁, f.F)) X₁.rel))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} X₁.src X₂.tgt)) (Subobject.pullback (prod.map π₁ π₁))
      (Functor.obj (Subobject.pullback (prod.map f.f (𝟙 X₂.tgt))) X₂.rel))
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₁ π₁ ≫ π(π₁, f.F))) X₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src X₂.tgt) (prod.map π₁ π₁) (prod.map f.f (𝟙 X₂.tgt))))
      X₂.rel)

Tactic:
rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this

Premises used: CategoryTheory.Subobject.pullback_comp
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₁ π₁ ≫ π(π₁, f.F))) X₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src X₂.tgt) (prod.map π₁ π₁) (prod.map f.f (𝟙 X₂.tgt))))
      X₂.rel)
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₁ π₁ ≫ π(π₁, f.F))) X₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src X₂.tgt) (prod.map π₁ π₁) (prod.map f.f (𝟙 X₂.tgt))))
      X₂.rel)

Tactic:
this
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₁ π₁ ≫ π(π₁, f.F))) X₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src X₂.tgt) (prod.map π₁ π₁) (prod.map f.f (𝟙 X₂.tgt))))
      X₂.rel)
h :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt) ⟶
      Limits.prod.{v, u} X₁.src X₁.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt))
      π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) (prod.map π₁ π₁))
    (prod.map π₁ π₁ ≫ π(π₁, f.F))
h₁ :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt) ⟶
      Limits.prod.{v, u} X₂.src X₂.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt))
      (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))) (prod.map π₁ π₁))
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src X₂.tgt) (prod.map π₁ π₁) (prod.map f.f (𝟙 X₂.tgt)))
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y :=
          Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt))
          π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) (prod.map π₁ π₁)))
      X₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y :=
          Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt))
          (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))) (prod.map π₁ π₁)))
      X₂.rel)

Tactic:
convert! this using 3
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₁ π₁ ≫ π(π₁, f.F))) X₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src X₂.tgt) (prod.map π₁ π₁) (prod.map f.f (𝟙 X₂.tgt))))
      X₂.rel)
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt) ⟶
      Limits.prod.{v, u} X₁.src X₁.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt))
      π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) (prod.map π₁ π₁))
    (prod.map π₁ π₁ ≫ π(π₁, 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₁ π₁ ≫ π(π₁, f.F))) X₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src X₂.tgt) (prod.map π₁ π₁) (prod.map f.f (𝟙 X₂.tgt))))
      X₂.rel)
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt) ⟶
      Limits.prod.{v, u} X₂.src X₂.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt))
      (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))) (prod.map π₁ π₁))
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X₁.src X₂.tgt) (prod.map π₁ π₁) (prod.map f.f (𝟙 X₂.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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₂ π₂)) (Functor.obj (Subobject.pullback π(π₁, g.F)) Y₁.rel))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} Y₁.src Y₂.tgt)) (Subobject.pullback (prod.map π₂ π₂))
      (Functor.obj (Subobject.pullback (prod.map g.f (𝟙 Y₂.tgt))) Y₂.rel))

Tactic:
have := (Subobject.pullback (prod.map π₂ π₂ :
        (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le g)
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₂ π₂)) (Functor.obj (Subobject.pullback π(π₁, g.F)) Y₁.rel))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} Y₁.src Y₂.tgt)) (Subobject.pullback (prod.map π₂ π₂))
      (Functor.obj (Subobject.pullback (prod.map g.f (𝟙 Y₂.tgt))) Y₂.rel))
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₂ π₂ ≫ π(π₁, g.F))) Y₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y₁.src Y₂.tgt) (prod.map π₂ π₂) (prod.map g.f (𝟙 Y₂.tgt))))
      Y₂.rel)

Tactic:
rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this

Premises used: CategoryTheory.Subobject.pullback_comp
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₂ π₂ ≫ π(π₁, g.F))) Y₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y₁.src Y₂.tgt) (prod.map π₂ π₂) (prod.map g.f (𝟙 Y₂.tgt))))
      Y₂.rel)
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₂ π₂ ≫ π(π₁, g.F))) Y₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y₁.src Y₂.tgt) (prod.map π₂ π₂) (prod.map g.f (𝟙 Y₂.tgt))))
      Y₂.rel)

Tactic:
this
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₂ π₂ ≫ π(π₁, g.F))) Y₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y₁.src Y₂.tgt) (prod.map π₂ π₂) (prod.map g.f (𝟙 Y₂.tgt))))
      Y₂.rel)
h :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt) ⟶
      Limits.prod.{v, u} Y₁.src Y₁.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt))
      π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) (prod.map π₂ π₂))
    (prod.map π₂ π₂ ≫ π(π₁, g.F))
h₁ :
  Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt) ⟶
      Limits.prod.{v, u} Y₂.src Y₂.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt))
      (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))) (prod.map π₂ π₂))
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y₁.src Y₂.tgt) (prod.map π₂ π₂) (prod.map g.f (𝟙 Y₂.tgt)))
⊢ LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y :=
          Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt))
          π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) (prod.map π₂ π₂)))
      Y₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y :=
          Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt))
          (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))) (prod.map π₂ π₂)))
      Y₂.rel)

Tactic:
convert! this using 3
-- 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₂ π₂ ≫ π(π₁, g.F))) Y₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y₁.src Y₂.tgt) (prod.map π₂ π₂) (prod.map g.f (𝟙 Y₂.tgt))))
      Y₂.rel)
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt) ⟶
      Limits.prod.{v, u} Y₁.src Y₁.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₁.tgt Y₁.tgt))
      π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) (prod.map π₂ π₂))
    (prod.map π₂ π₂ ≫ π(π₁, 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₁ X₂ Y₁ Y₂ : Dial.{v, u} C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this :
  LE.le (α :=
    Subobject.{v, u} (Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt)))
    (Functor.obj (Subobject.pullback (prod.map π₂ π₂ ≫ π(π₁, g.F))) Y₁.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y₁.src Y₂.tgt) (prod.map π₂ π₂) (prod.map g.f (𝟙 Y₂.tgt))))
      Y₂.rel)
⊢ Eq (α :=
    Limits.prod.{v, u} (Limits.prod.{v, u} X₁.src Y₁.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt) ⟶
      Limits.prod.{v, u} Y₂.src Y₂.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} X₂.src Y₂.src) (Limits.prod.{v, u} X₂.tgt Y₂.tgt))
      (prod.map (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))) (prod.map π₂ π₂))
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y₁.src Y₂.tgt) (prod.map π₂ π₂) (prod.map g.f (𝟙 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 : Dial.{v, u} C
⊢ (tensorObjImpl tensorUnitImpl X).rel =
    Functor.obj
      (Subobject.pullback (prod.map (Iso.hom (Limits.prod.leftUnitor X.src)) (Iso.hom (Limits.prod.leftUnitor X.tgt))) :
        Subobject.{v, u} (Limits.prod.{v, u} X.src X.tgt) ⥤
          Subobject.{v, u}
            (Limits.prod.{v, u} (tensorObjImpl tensorUnitImpl X).src (tensorObjImpl tensorUnitImpl X).tgt))
      X.rel

Tactic:
simp [Subobject.pullback_top]

Premises used: CategoryTheory.Subobject.pullback_top
-- 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 : Dial.{v, u} C
⊢ (X.tensorObjImpl tensorUnitImpl).rel =
    Functor.obj
      (Subobject.pullback
          (prod.map (Iso.hom (Limits.prod.rightUnitor X.src)) (Iso.hom (Limits.prod.rightUnitor X.tgt))) :
        Subobject.{v, u} (Limits.prod.{v, u} X.src X.tgt) ⥤
          Subobject.{v, u}
            (Limits.prod.{v, u} (X.tensorObjImpl tensorUnitImpl).src (X.tensorObjImpl tensorUnitImpl).tgt))
      X.rel

Tactic:
simp [Subobject.pullback_top]

Premises used: CategoryTheory.Subobject.pullback_top
-- 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 : Dial.{v, u} C
⊢ ((X.tensorObjImpl Y).tensorObjImpl Z).rel =
    Functor.obj
      (Subobject.pullback
          (prod.map (Iso.hom (prod.associator X.src Y.src Z.src)) (Iso.hom (prod.associator X.tgt Y.tgt Z.tgt))) :
        Subobject.{v, u}
            (Limits.prod.{v, u} (X.tensorObjImpl (Y.tensorObjImpl Z)).src (X.tensorObjImpl (Y.tensorObjImpl Z)).tgt) ⥤
          Subobject.{v, u}
            (Limits.prod.{v, u} ((X.tensorObjImpl Y).tensorObjImpl Z).src ((X.tensorObjImpl Y).tensorObjImpl Z).tgt))
      (X.tensorObjImpl (Y.tensorObjImpl Z)).rel

Tactic:
simp [Subobject.inf_pullback, ← Subobject.pullback_comp, inf_assoc]

Premises used: CategoryTheory.Subobject.pullback_comp, CategoryTheory.Subobject.inf_pullback, inf_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 (α := (tensorObj (𝒞 := instCategory) X₁ X₂).src ⟶ (tensorObj (𝒞 := instCategory) Z₁ Z₂).src)
    (Hom.f ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Hom.f (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
hF :
  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₂))
⊢ Eq (α := tensorObj (𝒞 := instCategory) X₁ X₂ ⟶ tensorObj (𝒞 := instCategory) Z₁ Z₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))
    (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

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₂
⊢ Eq (α := (tensorObj (𝒞 := instCategory) X₁ X₂).src ⟶ (tensorObj (𝒞 := instCategory) Z₁ Z₂).src)
    (Hom.f ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Hom.f (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))

Tactic:
simp