awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
F : X.Hom Y
G : Y.Hom Z
refine_1 :
  LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
      (Functor.obj (Subobject.pullback π(π₁, F.F)) X.rel))
refine_2 :
  LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
      (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
      (Functor.obj (Subobject.pullback (prod.map F.f (𝟙 Y.tgt))) Y.rel))
    (Functor.obj (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))) (Functor.obj (Subobject.pullback π(π₁, G.F)) Y.rel))
refine_3 :
  LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} Y.src Z.tgt)) (Subobject.pullback (prod.map F.f (𝟙 Z.tgt)))
      (Functor.obj (Subobject.pullback (prod.map G.f (𝟙 Z.tgt))) Z.rel))
    (Functor.obj (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))) Z.rel)
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))) Z.rel)

Tactic:
refine
    le_trans ?_ <| ((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
    le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_

Premises used: CategoryTheory.Dial.Hom.F, CategoryTheory.Limits.prod.fst, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.monotone, CategoryTheory.Dial.Hom.le, CategoryTheory.Subobject.pullback, CategoryTheory.CategoryStruct.comp, LE.le.trans, CategoryTheory.Dial.tgt, CategoryTheory.Limits.prod.lift, CategoryTheory.Dial.Hom.f, CategoryTheory.Limits.prod.map, le_trans
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
F : X.Hom Y
G : Y.Hom Z
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
      (Functor.obj (Subobject.pullback π(π₁, F.F)) X.rel))

Tactic:
simp [← Subobject.pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
F : X.Hom Y
G : Y.Hom Z
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
      (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F))
      (Functor.obj (Subobject.pullback (prod.map F.f (𝟙 Y.tgt))) Y.rel))
    (Functor.obj (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))) (Functor.obj (Subobject.pullback π(π₁, G.F)) Y.rel))

Tactic:
simp [← Subobject.pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
F : X.Hom Y
G : Y.Hom Z
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (C := Subobject.{v, u} (Limits.prod.{v, u} Y.src Z.tgt)) (Subobject.pullback (prod.map F.f (𝟙 Z.tgt)))
      (Functor.obj (Subobject.pullback (prod.map G.f (𝟙 Z.tgt))) Z.rel))
    (Functor.obj (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))) Z.rel)

Tactic:
simp [← Subobject.pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src X.tgt)) (Functor.obj (Subobject.pullback π(π₁, π₂)) X.rel)
    (Functor.obj (Subobject.pullback (prod.map (𝟙 X.src) (𝟙 X.tgt))) X.rel)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
simp :
  Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ W.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
      (π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F) ≫ f.F))
    (π(π₁,
        CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
          (π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫ g.F)) ≫
      f.F)
⊢ { f := { f := f.f ≫ g.f, F := π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F) ≫ f.F, le := ⋯ : W.Hom Y }.f ≫ h.f,
      F :=
        π(π₁,
            prod.map { f := f.f ≫ g.f, F := π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F) ≫ f.F, le := ⋯ : W.Hom Y }.f (𝟙 Z.tgt) ≫
              h.F) ≫
          { f := f.f ≫ g.f, F := π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F) ≫ f.F, le := ⋯ : W.Hom Y }.F,
      le := ⋯ : W.Hom Z } =
    { f := f.f ≫ { f := g.f ≫ h.f, F := π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫ g.F, le := ⋯ : X.Hom Z }.f,
      F :=
        π(π₁,
            prod.map f.f (𝟙 Z.tgt) ≫
              { f := g.f ≫ h.f, F := π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫ g.F, le := ⋯ : X.Hom Z }.F) ≫
          f.F,
      le := ⋯ }

Tactic:
simp only [Category.assoc, Hom.mk.injEq, true_and]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Dial.Hom.mk.injEq, true_and
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
rw :
  Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ W.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
        π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F) ≫
      f.F)
    (π(π₁,
        CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
            π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫
          g.F) ≫
      f.F)
⊢ Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ W.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
      (π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F) ≫ f.F))
    (π(π₁,
        CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
          (π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫ g.F)) ≫
      f.F)

Tactic:
rw [← Category.assoc, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
e_a :
  Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ Limits.prod.{v, u} W.src X.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
      π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F))
    π(π₁,
      CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
          π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫
        g.F)
⊢ Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ W.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
        π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F) ≫
      f.F)
    (π(π₁,
        CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
            π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫
          g.F) ≫
      f.F)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
e_a :
  Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ W.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src X.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
        π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F))
      π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src X.tgt)
      π(π₁,
        CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
            π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫
          g.F)
      π₁)
e_a₁ :
  Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ X.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src X.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
        π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F))
      π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src X.tgt)
      π(π₁,
        CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
            π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫
          g.F)
      π₂)
⊢ Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ Limits.prod.{v, u} W.src X.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
      π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F))
    π(π₁,
      CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
          π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫
        g.F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ W.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src X.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
        π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F))
      π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src X.tgt)
      π(π₁,
        CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
            π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫
          g.F)
      π₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ Eq (α := Limits.prod.{v, u} W.src Z.tgt ⟶ X.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src X.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src Y.tgt) π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z.tgt) ≫ h.F)
        π(π₁, prod.map f.f (𝟙 Y.tgt) ≫ g.F))
      π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} W.src X.tgt)
      π(π₁,
        CategoryStruct.comp (Y := Limits.prod.{v, u} X.src Z.tgt) (prod.map f.f (𝟙 Z.tgt))
            π(π₁, prod.map g.f (𝟙 Z.tgt) ≫ h.F) ≫
          g.F)
      π₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
x y : X ⟶ Y
hf : x.f = y.f
hF : x.F = y.F
⊢ x = y

Tactic:
Hom.ext hf hF

Premises used: CategoryTheory.Dial.Hom.ext
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
rw :
  LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom)))
      Y.rel)
    (Functor.obj (Subobject.pullback (prod.map e₁.hom (𝟙 Y.tgt))) Y.rel)
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π₂ ≫ e₂.inv)) X.rel)
    (Functor.obj (Subobject.pullback (prod.map e₁.hom (𝟙 Y.tgt))) Y.rel)

Tactic:
rw [eq, ← Subobject.pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
hab :
  Eq (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom)))
      Y.rel)
    (Functor.obj (Subobject.pullback (prod.map e₁.hom (𝟙 Y.tgt))) Y.rel)
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom)))
      Y.rel)
    (Functor.obj (Subobject.pullback (prod.map e₁.hom (𝟙 Y.tgt))) Y.rel)

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
hab :
  Eq (α := Limits.prod.{v, u} X.src Y.tgt ⟶ Limits.prod.{v, u} Y.src Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom))
    (prod.map e₁.hom (𝟙 Y.tgt))
⊢ Eq (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Y.tgt))
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom)))
      Y.rel)
    (Functor.obj (Subobject.pullback (prod.map e₁.hom (𝟙 Y.tgt))) Y.rel)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
hab :
  Eq (α := Limits.prod.{v, u} X.src Y.tgt ⟶ Y.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom)) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt) (prod.map e₁.hom (𝟙 Y.tgt)) π₁)
hab₁ :
  Eq (α := Limits.prod.{v, u} X.src Y.tgt ⟶ Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom)) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt) (prod.map e₁.hom (𝟙 Y.tgt)) π₂)
⊢ Eq (α := Limits.prod.{v, u} X.src Y.tgt ⟶ Limits.prod.{v, u} Y.src Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom))
    (prod.map e₁.hom (𝟙 Y.tgt))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
⊢ Eq (α := Limits.prod.{v, u} X.src Y.tgt ⟶ Y.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom)) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt) (prod.map e₁.hom (𝟙 Y.tgt)) π₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
⊢ Eq (α := Limits.prod.{v, u} X.src Y.tgt ⟶ Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) π(π₁, π₂ ≫ e₂.inv) (prod.map e₁.hom e₂.hom)) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt) (prod.map e₁.hom (𝟙 Y.tgt)) π₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
rw :
  LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} Y.src X.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π₂ ≫ e₂.hom)) Y.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt))
          (prod.map e₁.hom e₂.hom)))
      Y.rel)
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} Y.src X.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π₂ ≫ e₂.hom)) Y.rel)
    (Functor.obj (Subobject.pullback (prod.map e₁.inv (𝟙 X.tgt))) X.rel)

Tactic:
rw [eq, ← Subobject.pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
hab :
  Eq (α := Subobject.{v, u} (Limits.prod.{v, u} Y.src X.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π₂ ≫ e₂.hom)) Y.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt))
          (prod.map e₁.hom e₂.hom)))
      Y.rel)
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} Y.src X.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π₂ ≫ e₂.hom)) Y.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt))
          (prod.map e₁.hom e₂.hom)))
      Y.rel)

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
hab :
  Eq (α := Limits.prod.{v, u} Y.src X.tgt ⟶ Limits.prod.{v, u} Y.src Y.tgt) π(π₁, π₂ ≫ e₂.hom)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt)) (prod.map e₁.hom e₂.hom))
⊢ Eq (α := Subobject.{v, u} (Limits.prod.{v, u} Y.src X.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π₂ ≫ e₂.hom)) Y.rel)
    (Functor.obj
      (Subobject.pullback
        (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt))
          (prod.map e₁.hom e₂.hom)))
      Y.rel)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
hab :
  Eq (α := Limits.prod.{v, u} Y.src X.tgt ⟶ Y.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt) π(π₁, π₂ ≫ e₂.hom) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt)) (prod.map e₁.hom e₂.hom))
      π₁)
hab₁ :
  Eq (α := Limits.prod.{v, u} Y.src X.tgt ⟶ Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt) π(π₁, π₂ ≫ e₂.hom) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt)) (prod.map e₁.hom e₂.hom))
      π₂)
⊢ Eq (α := Limits.prod.{v, u} Y.src X.tgt ⟶ Limits.prod.{v, u} Y.src Y.tgt) π(π₁, π₂ ≫ e₂.hom)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt)) (prod.map e₁.hom e₂.hom))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
⊢ Eq (α := Limits.prod.{v, u} Y.src X.tgt ⟶ Y.src)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt) π(π₁, π₂ ≫ e₂.hom) π₁)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt)) (prod.map e₁.hom e₂.hom))
      π₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
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
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = Functor.obj (Subobject.pullback (prod.map e₁.hom e₂.hom)) Y.rel
⊢ Eq (α := Limits.prod.{v, u} Y.src X.tgt ⟶ Y.tgt)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt) π(π₁, π₂ ≫ e₂.hom) π₂)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y.src Y.tgt)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} X.src X.tgt) (prod.map e₁.inv (𝟙 X.tgt)) (prod.map e₁.hom e₂.hom))
      π₂)

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

Tactic:
simp only [tensorObjImpl, Subobject.inf_pullback]

Premises used: CategoryTheory.Dial.tensorObjImpl, CategoryTheory.Subobject.inf_pullback