awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X R Y Z : C
f : R ⟶ X
g₁ : Y ⟶ X
g₂ : Z ⟶ X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk g₁)) ((pullback f).obj (mk g₂))).left ⟶ Z)
    (CategoryStruct.comp (Y := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk g₁) (mk g₂))).left)
      (Hom.left (LaxMonoidal.μ (pullback f) (mk g₁) (mk g₂)))
      (pullback.fst (pullback.fst g₁ g₂ ≫ g₁) f ≫ pullback.snd g₁ g₂))
    (pullback.snd ((pullback f).obj (mk g₁)).hom ((pullback f).obj (mk g₂)).hom ≫ pullback.fst (mk g₂).hom f)

Tactic:
μ_pullback_left_fst_snd ..

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X R Y Z : C
f : R ⟶ X
g₁ : Y ⟶ X
g₂ : Z ⟶ X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk g₁)) ((pullback f).obj (mk g₂))).left ⟶ R)
    (CategoryStruct.comp (Y := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk g₁) (mk g₂))).left)
      (Hom.left (LaxMonoidal.μ (pullback f) (mk g₁) (mk g₂))) (pullback.snd (pullback.fst g₁ g₂ ≫ g₁) f))
    (pullback.snd ((pullback f).obj (mk g₁)).hom ((pullback f).obj (mk g₂)).hom ≫ pullback.snd (mk g₂).hom f)

Tactic:
μ_pullback_left_snd ..

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Over.μ_pullback_left_snd
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f_1 : R ⟶ X
g : S ⟶ X
f : R ⟶ S
⊢ Iso.hom (asIso (pullback.snd (𝟙 S) f)) ≫ hom ((𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver)) =
    ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} S)) (𝒞 := instCategoryOver))).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
R S : C
f : R ⟶ S
w :
  Eq (α :=
    (pullback f).obj ((𝟙_ (Over.{v_1, u_1} S)) (𝒞 := instCategoryOver)) ⟶
      (𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver))
    (Iso.hom (preservesTerminalIso (pullback f))) (Iso.hom (isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯))
⊢ Eq (α :=
    (pullback f).obj ((𝟙_ (Over.{v_1, u_1} S)) (𝒞 := instCategoryOver)) ≅
      (𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver))
    (preservesTerminalIso (pullback f)) (isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
R S : C
f : R ⟶ S
⊢ Eq (α :=
    (pullback f).obj ((𝟙_ (Over.{v_1, u_1} S)) (𝒞 := instCategoryOver)) ⟶
      (𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver))
    (Iso.hom (preservesTerminalIso (pullback f))) (Iso.hom (isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯))

Tactic:
toUnit_unique _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
R S : C
f : R ⟶ S
⊢ Eq (α :=
    (pullback f).obj ((𝟙_ (Over.{v_1, u_1} S)) (𝒞 := instCategoryOver)) ⟶
      (𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver))
    (Iso.hom (preservesTerminalIso (pullback f))) (Iso.hom (isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯))

Tactic:
exact toUnit_unique _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Over.{v_1, u_1} Y
rw :
  Eq (α := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) A B)).left ⟶ A.left)
    (pullback.fst (pullback.fst A.hom B.hom ≫ A.hom) f ≫ pullback.fst A.hom B.hom)
    (CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj A) ((pullback f).obj B)).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) A B)))
      (pullback.fst (pullback.snd A.hom f) (pullback.snd B.hom f) ≫ pullback.fst A.hom f))
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj A) ((pullback f).obj B)).left ⟶ A.left)
    (CategoryStruct.comp (Y := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) A B)).left)
      (Hom.left (Iso.inv (prodComparisonIso (pullback f) A B)))
      (pullback.fst (pullback.fst A.hom B.hom ≫ A.hom) f ≫ pullback.fst A.hom B.hom))
    (pullback.fst (pullback.snd A.hom f) (pullback.snd B.hom f) ≫ pullback.fst A.hom f)

Tactic:
rw [← cancel_epi (prodComparisonIso (Over.pullback f) A B).hom.left,
    Over.hom_left_inv_left_assoc]

Premises used: CategoryTheory.Over.pullback, CategoryTheory.Over.Hom.left, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso, CategoryTheory.Over.hom_left_inv_left_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Over.{v_1, u_1} Y
⊢ Eq (α := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) A B)).left ⟶ A.left)
    (pullback.fst (pullback.fst A.hom B.hom ≫ A.hom) f ≫ pullback.fst A.hom B.hom)
    (CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj A) ((pullback f).obj B)).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) A B)))
      (pullback.fst (pullback.snd A.hom f) (pullback.snd B.hom f) ≫ pullback.fst A.hom f))

Tactic:
simp [CartesianMonoidalCategory.prodComparison, fst]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison, CategoryTheory.SemiCartesianMonoidalCategory.fst
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk gA)) ((pullback f).obj (mk gB))).left ⟶ A)
    (CategoryStruct.comp (Y := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk gA) (mk gB))).left)
      (Hom.left (Iso.inv (prodComparisonIso (pullback f) (mk gA) (mk gB))))
      (pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.fst gA gB))
    (pullback.fst (pullback.snd gA f) (pullback.snd gB f) ≫ pullback.fst gA f)

Tactic:
prodComparisonIso_pullback_inv_left_fst_fst ..

Premises used: CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
rw :
  Eq (α := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk gA) (mk gB))).left ⟶ B)
    (pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.snd gA gB)
    (CategoryStruct.comp (Y :=
      (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk gA)) ((pullback f).obj (mk gB))).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) (mk gA) (mk gB))))
      (pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.fst (mk gB).hom f))
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk gA)) ((pullback f).obj (mk gB))).left ⟶ B)
    (CategoryStruct.comp (Y := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk gA) (mk gB))).left)
      (Hom.left (Iso.inv (prodComparisonIso (pullback f) (mk gA) (mk gB))))
      (pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.snd gA gB))
    (pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.fst (mk gB).hom f)

Tactic:
rw [← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,
    Over.hom_left_inv_left_assoc]

Premises used: CategoryTheory.Over.pullback, CategoryTheory.Over.Hom.left, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso, CategoryTheory.Over.hom_left_inv_left_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Eq (α := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk gA) (mk gB))).left ⟶ B)
    (pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.snd gA gB)
    (CategoryStruct.comp (Y :=
      (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk gA)) ((pullback f).obj (mk gB))).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) (mk gA) (mk gB))))
      (pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.fst (mk gB).hom f))

Tactic:
simp [CartesianMonoidalCategory.prodComparison, snd]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.CartesianMonoidalCategory.prodComparison
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
rw :
  Eq (α := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk gA) (mk gB))).left ⟶ X)
    (pullback.snd (pullback.fst gA gB ≫ gA) f)
    (CategoryStruct.comp (Y :=
      (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk gA)) ((pullback f).obj (mk gB))).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) (mk gA) (mk gB))))
      (pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f))
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk gA)) ((pullback f).obj (mk gB))).left ⟶ X)
    (CategoryStruct.comp (Y := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk gA) (mk gB))).left)
      (Hom.left (Iso.inv (prodComparisonIso (pullback f) (mk gA) (mk gB)))) (pullback.snd (pullback.fst gA gB ≫ gA) f))
    (pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f)

Tactic:
rw [← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,
    Over.hom_left_inv_left_assoc]

Premises used: CategoryTheory.Over.pullback, CategoryTheory.Over.Hom.left, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso, CategoryTheory.Over.hom_left_inv_left_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Eq (α := ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) (mk gA) (mk gB))).left ⟶ X)
    (pullback.snd (pullback.fst gA gB ≫ gA) f)
    (CategoryStruct.comp (Y :=
      (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj (mk gA)) ((pullback f).obj (mk gB))).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) (mk gA) (mk gB))))
      (pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f))

Tactic:
simp [CartesianMonoidalCategory.prodComparison]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
inst_3 : IsCommMonObj (mk f)
⊢ IsCommMonObj (mk (Y := Limits.pullback f g) (pullback.snd f g))

Tactic:
((Over.pullback g).mapCommMon.obj <| .mk <| .mk f).comm

Premises used: CategoryTheory.Over, CategoryTheory.Over.pullback, CategoryTheory.Over.mk, CategoryTheory.CostructuredArrow, CategoryTheory.CommMon.mk, CategoryTheory.CostructuredArrow.mk, CategoryTheory.CommMon.comm, CategoryTheory.Functor.obj, CategoryTheory.Functor.mapCommMon
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
⊢ pullback.snd f (𝟙 X) ≫ 𝟙 X = (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
h :
  Eq.{v_1 + 1} (α :=
    (tensorObj (𝒞 := instCategoryOver) (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))
          (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))).left ⟶
      (mk f).left)
    (Hom.left (MonObj.mul ≫ homMk (pullback.fst f (𝟙 X)) ⋯))
    (Hom.left ((homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ MonObj.mul))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj (𝒞 := instCategoryOver) (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))
        (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))) ⟶
      mk f)
    (MonObj.mul ≫ homMk (pullback.fst f (𝟙 X)) ⋯)
    ((homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ MonObj.mul)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
h :
  Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback f (𝟙 X))
        (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
          (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)))
          (pullback.lift (pullback.fst (pullback.fst f f ≫ f) (𝟙 X) ≫ Hom.left MonObj.mul)
            (pullback.snd (pullback.fst f f ≫ f) (𝟙 X)) ⋯))
        (pullback.fst f (𝟙 X)) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
⊢ Eq.{v_1 + 1} (α :=
    (tensorObj (𝒞 := instCategoryOver) (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))
          (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))).left ⟶
      (mk f).left)
    (Hom.left (MonObj.mul ≫ homMk (pullback.fst f (𝟙 X)) ⋯))
    (Hom.left ((homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ MonObj.mul))

Tactic:
dsimp [monObjMkPullbackSnd_mul]

Premises used: CategoryTheory.Over.monObjMkPullbackSnd_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
h :
  Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
        (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)))
        (pullback.fst (pullback.fst f f ≫ f) (𝟙 X) ≫ Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
⊢ Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback f (𝟙 X))
        (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
          (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)))
          (pullback.lift (pullback.fst (pullback.fst f f ≫ f) (𝟙 X) ≫ Hom.left MonObj.mul)
            (pullback.snd (pullback.fst f f ≫ f) (𝟙 X)) ⋯))
        (pullback.fst f (𝟙 X)) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)

Tactic:
simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
h :
  Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
          (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f))) (pullback.fst (pullback.fst f f ≫ f) (𝟙 X)))
        (Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
⊢ Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
        (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)))
        (pullback.fst (pullback.fst f f ≫ f) (𝟙 X) ≫ Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
h :
  Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      Limits.pullback f f)
    (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
        (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f))) (pullback.fst (pullback.fst f f ≫ f) (𝟙 X)) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        Limits.pullback f f)
    (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) :
      (tensorObj (𝒞 := instCategoryOver) (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))
            (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))).left ⟶
        (tensorObj (𝒞 := instCategoryOver) (mk f) (mk f)).left)
⊢ Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
          (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f))) (pullback.fst (pullback.fst f f ≫ f) (𝟙 X)))
        (Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (Hom.left MonObj.mul) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
h :
  Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
          (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f))) (pullback.fst (pullback.fst f f ≫ f) (𝟙 X)))
        (pullback.fst f f) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (pullback.fst f f) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
h₁ :
  Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
          (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f))) (pullback.fst (pullback.fst f f ≫ f) (𝟙 X)))
        (pullback.snd f f) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (pullback.snd f f) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
⊢ Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      Limits.pullback f f)
    (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
        (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f))) (pullback.fst (pullback.fst f f ≫ f) (𝟙 X)) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        Limits.pullback f f)
    (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) :
      (tensorObj (𝒞 := instCategoryOver) (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))
            (mk (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X)))).left ⟶
        (tensorObj (𝒞 := instCategoryOver) (mk f) (mk f)).left)

Tactic:
ext