awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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
⊢ { 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 := ⋯ }
have 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)
Tactic: simp only [Category.assoc, Hom.mk.injEq, true_and]
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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.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)
have 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)
Tactic: rw [← Category.assoc, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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.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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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 ⟶ 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)
have 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)
    π₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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)
      π₁)
⊢ 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)
have 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)
    π₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [eq, ← Subobject.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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
⊢ 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)
have 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)
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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 (α := 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)
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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 ⟶ 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))
have 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)) π₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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)) π₁)
⊢ 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))
have 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)) π₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [eq, ← Subobject.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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
⊢ 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)
have 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)
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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 (α := 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)
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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 ⟶ 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))
have 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)) π₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Basic (goal)
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))
      π₁)
⊢ 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))
have 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)) π₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Monoidal (goal)
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} (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)
have 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))
Tactic: simp only [tensorObjImpl, Subobject.inf_pullback]
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Monoidal (goal)
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 (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))
have 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))
Tactic: apply inf_le_inf
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Monoidal (goal)
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))
⊢ 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))
have 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))
Tactic: apply inf_le_inf