awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (prod.map f.f g.f) (𝟙 (Limits.prod.{v, u} X₂.tgt Y₂.tgt))))
      (Functor.obj (Subobject.pullback (prod.map π₁ π₁)) X₂.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
    (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: rw [← Subobject.pullback_comp, ← Subobject.pullback_comp]
-- 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 π₂ π₂)) 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))
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
    (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: rw [← Subobject.pullback_comp, ← Subobject.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Monoidal (hypothesis)
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
        (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)
have 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))
Tactic: have := (Subobject.pullback (prod.map π₁ π₁ :
        (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Monoidal (hypothesis)
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
        (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)
have 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)
Tactic: rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this
Cleared hypotheses: this
-- 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₂
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
        (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)
have 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))
Tactic: convert! this using 3
-- 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₂
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))
⊢ 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)
have 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)))
Tactic: convert! this using 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Monoidal (hypothesis)
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
        (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)
have 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))
Tactic: have := (Subobject.pullback (prod.map π₂ π₂ :
        (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Dialectica.Monoidal (hypothesis)
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
        (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)
have 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)
Tactic: rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this
Cleared hypotheses: this
-- 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₂
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
        (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)
have 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))
Tactic: convert! this using 3
-- 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₂
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))
⊢ 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)
have 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)))
Tactic: convert! this using 3
-- 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₁ 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₂ ⟶ tensorObj (𝒞 := instCategory) Z₁ Z₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))
    (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
have hf : Eq (α := (tensorObj (𝒞 := instCategory) X₁ X₂).src ⟶ (tensorObj (𝒞 := instCategory) Z₁ Z₂).src)
  (Hom.f ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Hom.f (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
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₁ 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₂))
⊢ Eq (α := tensorObj (𝒞 := instCategory) X₁ X₂ ⟶ tensorObj (𝒞 := instCategory) Z₁ Z₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))
    (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
have 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₂))
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₁ 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} (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₂))
have 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))
Tactic: simp
-- 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₁ 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₁.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))
have 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))
    π₁)
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₁ 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))
      π₁)
⊢ 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))
have 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))
    π₂)
Tactic: ext