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 : C
R S T : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) (tensorObj (𝒞 := instCategoryOver) R S) T).left ⟶ R.left)
    (Hom.left (Iso.hom (α_ R S T)) ≫ pullback.fst R.hom (pullback.fst S.hom T.hom ≫ S.hom))
    (pullback.fst (tensorObj (𝒞 := instCategoryOver) R S).hom T.hom ≫ pullback.fst R.hom S.hom)

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
R S T : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) (tensorObj (𝒞 := instCategoryOver) R S) T).left ⟶ S.left)
    (Hom.left (Iso.hom (α_ R S T)) ≫ pullback.snd R.hom (pullback.fst S.hom T.hom ≫ S.hom) ≫ pullback.fst S.hom T.hom)
    (pullback.fst (tensorObj (𝒞 := instCategoryOver) R S).hom T.hom ≫ pullback.snd R.hom S.hom)

Tactic:
(limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π, Eq.trans
-- 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 : C
R S T : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) (tensorObj (𝒞 := instCategoryOver) R S) T).left ⟶ T.left)
    (Hom.left (Iso.hom (α_ R S T)) ≫ pullback.snd R.hom (pullback.fst S.hom T.hom ≫ S.hom) ≫ pullback.snd S.hom T.hom)
    (pullback.snd (tensorObj (𝒞 := instCategoryOver) R S).hom T.hom)

Tactic:
(limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π, Eq.trans
-- 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 : C
R S T : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R (tensorObj (𝒞 := instCategoryOver) S T)).left ⟶ R.left)
    (Hom.left (Iso.inv (α_ R S T)) ≫ pullback.fst (pullback.fst R.hom S.hom ≫ R.hom) T.hom ≫ pullback.fst R.hom S.hom)
    (pullback.fst R.hom (tensorObj (𝒞 := instCategoryOver) S T).hom)

Tactic:
(limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π, Eq.trans
-- 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 : C
R S T : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R (tensorObj (𝒞 := instCategoryOver) S T)).left ⟶ S.left)
    (Hom.left (Iso.inv (α_ R S T)) ≫ pullback.fst (pullback.fst R.hom S.hom ≫ R.hom) T.hom ≫ pullback.snd R.hom S.hom)
    (pullback.snd R.hom (tensorObj (𝒞 := instCategoryOver) S T).hom ≫ pullback.fst S.hom T.hom)

Tactic:
(limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π, Eq.trans
-- 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 : C
R S T : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R (tensorObj (𝒞 := instCategoryOver) S T)).left ⟶ T.left)
    (Hom.left (Iso.inv (α_ R S T)) ≫ pullback.snd (pullback.fst R.hom S.hom ≫ R.hom) T.hom)
    (pullback.snd R.hom (tensorObj (𝒞 := instCategoryOver) S T).hom ≫ pullback.snd S.hom T.hom)

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
Y : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver)) Y).left ⟶ Y.left)
    (Hom.left (Iso.hom (λ_ Y))) (pullback.snd (hom ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))) Y.hom)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- 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 : C
Y : Over.{v_1, u_1} X
⊢ CategoryStruct.comp (Y :=
      (tensorObj (𝒞 := instCategoryOver) ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver)) Y).left)
      (Hom.left (Iso.inv (λ_ Y))) (pullback.fst (𝟙 X) Y.hom) =
    Y.hom

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
Y : Over.{v_1, u_1} X
⊢ CategoryStruct.comp (Y :=
      (tensorObj (𝒞 := instCategoryOver) ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver)) Y).left)
      (Hom.left (Iso.inv (λ_ Y))) (pullback.snd (𝟙 X) Y.hom) =
    𝟙 Y.left

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
Y : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) Y ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left ⟶ Y.left)
    (Hom.left (Iso.hom (ρ_ Y))) (pullback.fst Y.hom (𝟙 X))

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- 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 : C
Y : Over.{v_1, u_1} X
⊢ CategoryStruct.comp (Y :=
      (tensorObj (𝒞 := instCategoryOver) Y ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left)
      (Hom.left (Iso.inv (ρ_ Y))) (pullback.fst Y.hom (𝟙 X)) =
    𝟙 Y.left

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
Y : Over.{v_1, u_1} X
⊢ CategoryStruct.comp (Y :=
      (tensorObj (𝒞 := instCategoryOver) Y ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left)
      (Hom.left (Iso.inv (ρ_ Y))) (pullback.snd Y.hom (𝟙 X)) =
    Y.hom

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
R S T : Over.{v_1, u_1} X
f : S ⟶ T
⊢ R.hom ≫ 𝟙 X = 𝟙 R.left ≫ R.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 : C
R S T : Over.{v_1, u_1} X
f : S ⟶ T
⊢ S.hom ≫ 𝟙 X = Hom.left f ≫ T.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 : C
R S T : Over.{v_1, u_1} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ (tensorObj (𝒞 := instCategoryOver) R T).left)
    (Hom.left (R ◁ f)) (pullback.map R.hom S.hom R.hom T.hom (𝟙 R.left) (Hom.left f) (𝟙 X) ⋯ ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.limit.lift, rfl
-- 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 : C
R S T : Over.{v_1, u_1} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ R.left) (Hom.left (R ◁ f) ≫ pullback.fst R.hom T.hom)
    (pullback.fst R.hom S.hom)

Tactic:
(limit.lift_π _ _).trans (Category.comp_id _)

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π, Eq.trans
-- 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 : C
R S T : Over.{v_1, u_1} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ T.left) (Hom.left (R ◁ f) ≫ pullback.snd R.hom T.hom)
    (pullback.snd R.hom S.hom ≫ Hom.left f)

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
R S T : Over.{v_1, u_1} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) S R).left ⟶ (tensorObj (𝒞 := instCategoryOver) T R).left)
    (Hom.left (f ▷ R)) (pullback.map S.hom R.hom T.hom R.hom (Hom.left f) (𝟙 R.left) (𝟙 X) ⋯ ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.limit.lift, rfl
-- 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 : C
R S T : Over.{v_1, u_1} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) S R).left ⟶ T.left) (Hom.left (f ▷ R) ≫ pullback.fst T.hom R.hom)
    (pullback.fst S.hom R.hom ≫ Hom.left f)

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
R S T : Over.{v_1, u_1} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) S R).left ⟶ R.left) (Hom.left (f ▷ R) ≫ pullback.snd T.hom R.hom)
    (pullback.snd S.hom R.hom)

Tactic:
(limit.lift_π _ _).trans (Category.comp_id _)

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π, Eq.trans
-- 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 : C
R S T U : Over.{v_1, u_1} X
f : R ⟶ S
g : T ⟶ U
⊢ R.hom ≫ 𝟙 X = Hom.left f ≫ S.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 : C
R S T U : Over.{v_1, u_1} X
f : R ⟶ S
g : T ⟶ U
⊢ T.hom ≫ 𝟙 X = Hom.left g ≫ U.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 : C
R S T U : Over.{v_1, u_1} X
f : R ⟶ S
g : T ⟶ U
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R T).left ⟶ (tensorObj (𝒞 := instCategoryOver) S U).left)
    (Hom.left (f ⊗ₘ g)) (pullback.map R.hom T.hom S.hom U.hom (Hom.left f) (Hom.left g) (𝟙 X) ⋯ ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.limit.lift, rfl
-- 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 S U : C
R T : Over.{v_1, u_1} X
fS : S ⟶ X
fU : U ⟶ X
f : R ⟶ mk fS
g : T ⟶ mk fU
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R T).left ⟶ S) (Hom.left (f ⊗ₘ g) ≫ pullback.fst fS fU)
    (pullback.fst R.hom T.hom ≫ Hom.left f)

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 S U : C
R T : Over.{v_1, u_1} X
fS : S ⟶ X
fU : U ⟶ X
f : R ⟶ mk fS
g : T ⟶ mk fU
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R T).left ⟶ U) (Hom.left (f ⊗ₘ g) ≫ pullback.snd fS fU)
    (pullback.snd R.hom T.hom ≫ Hom.left g)

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, 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 : C
R S : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ (tensorObj (𝒞 := instCategoryOver) S R).left)
    (Hom.left (Iso.hom (β_ R S))) (Iso.hom (pullbackSymmetry R.hom S.hom))

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.PullbackCone.flip, CategoryTheory.Limits.limit, CategoryTheory.Limits.PullbackCone.mk, rfl
-- 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 : C
R S : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) S R).left ⟶ (tensorObj (𝒞 := instCategoryOver) R S).left)
    (Hom.left (Iso.inv (β_ R S))) (Iso.hom (pullbackSymmetry S.hom R.hom))

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.PullbackCone.flip, CategoryTheory.Limits.limit, CategoryTheory.Limits.PullbackCone.mk, rfl
-- 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 : C
f : R ⟶ X
⊢ Eq (α :=
    ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left ⟶
      left.{v_1, u_1} (X := R) ((𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver)))
    (Hom.left (OplaxMonoidal.η (pullback f))) (pullback.snd (𝟙 X) f)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- 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 : C
f : R ⟶ X
hom_inv_id :
  pullback.snd (𝟙 X) f ≫ Hom.left (LaxMonoidal.ε (pullback f)) =
    𝟙 ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left
⊢ Eq (α :=
    left.{v_1, u_1} (X := R) ((𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver)) ⟶
      ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left)
    (Hom.left (LaxMonoidal.ε (pullback f))) (inv (pullback.snd (𝟙 X) f))

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id
-- 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 : C
f : R ⟶ X
hom_inv_id :
  CategoryStruct.comp (Y := left.{v_1, u_1} (X := R) ((𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver)))
      (Hom.left (OplaxMonoidal.η (pullback f))) (Hom.left (LaxMonoidal.ε (pullback f))) =
    𝟙 ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left
hom_inv_id₁ :
  Hom.left
      (CategoryStruct.comp (Y := (𝟙_ (Over.{v_1, u_1} R)) (𝒞 := instCategoryOver)) (OplaxMonoidal.η (pullback f))
        (LaxMonoidal.ε (pullback f))) =
    𝟙 ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left
hom_inv_id₂ :
  Hom.left (𝟙 ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver)))) =
    𝟙 ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left
hom_inv_id₃ hom_inv_id₄ :
  Eq.{v_1 + 1} (α :=
    ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left ⟶
      ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left)
    (𝟙 ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left)
    (𝟙 ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left)
⊢ pullback.snd (𝟙 X) f ≫ Hom.left (LaxMonoidal.ε (pullback f)) =
    𝟙 ((pullback f).obj ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))).left

Tactic:
rw [← η_pullback_left, ← Over.comp_left, Monoidal.η_ε, Over.id_left]

Premises used: CategoryTheory.Over.comp_left, CategoryTheory.Over.η_pullback_left, CategoryTheory.Over.id_left, CategoryTheory.Functor.Monoidal.η_ε
-- 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_1 : C
f : R_1 ⟶ X
R S : Over.{v_1, u_1} X
rw :
  Hom.left (𝟙 ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) R S))) ≫
      pullback.fst (tensorObj (𝒞 := instCategoryOver) R S).hom f ≫ pullback.fst R.hom S.hom =
    CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) R S)))
      (pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f)
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left ⟶ R.left)
    (Hom.left (LaxMonoidal.μ (pullback f) R S) ≫
      pullback.fst (tensorObj (𝒞 := instCategoryOver) R S).hom f ≫ pullback.fst R.hom S.hom)
    (pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f)

Tactic:
rw [Monoidal.μ_of_cartesianMonoidalCategory,
    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left, ← Over.comp_left_assoc,
    Iso.hom_inv_id]

Premises used: CategoryTheory.Over.comp_left_assoc, CategoryTheory.Over.pullback, CategoryTheory.Over.Hom.left, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso, 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 R_1 : C
f : R_1 ⟶ X
R S : Over.{v_1, u_1} X
⊢ Hom.left (𝟙 ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) R S))) ≫
      pullback.fst (tensorObj (𝒞 := instCategoryOver) R S).hom f ≫ pullback.fst R.hom S.hom =
    CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) R S)))
      (pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.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 R_1 : C
f : R_1 ⟶ X
R S : Over.{v_1, u_1} X
rw :
  Hom.left (𝟙 ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) R S))) ≫
      pullback.fst (tensorObj (𝒞 := instCategoryOver) R S).hom f ≫ pullback.snd R.hom S.hom =
    CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) R S)))
      (pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst S.hom f)
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left ⟶ S.left)
    (Hom.left (LaxMonoidal.μ (pullback f) R S) ≫
      pullback.fst (tensorObj (𝒞 := instCategoryOver) R S).hom f ≫ pullback.snd R.hom S.hom)
    (pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst S.hom f)

Tactic:
rw [Monoidal.μ_of_cartesianMonoidalCategory,
    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left,
    ← Over.comp_left_assoc, Iso.hom_inv_id]

Premises used: CategoryTheory.Over.comp_left_assoc, CategoryTheory.Over.pullback, CategoryTheory.Over.Hom.left, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso, 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 R_1 : C
f : R_1 ⟶ X
R S : Over.{v_1, u_1} X
⊢ Hom.left (𝟙 ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) R S))) ≫
      pullback.fst (tensorObj (𝒞 := instCategoryOver) R S).hom f ≫ pullback.snd R.hom S.hom =
    CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) R S)))
      (pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst S.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 R_1 : C
f : R_1 ⟶ X
R S : Over.{v_1, u_1} X
rw :
  Hom.left (𝟙 ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) R S))) ≫
      pullback.snd (tensorObj (𝒞 := instCategoryOver) R S).hom f =
    CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) R S)))
      (pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f)
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left ⟶ R_1)
    (Hom.left (LaxMonoidal.μ (pullback f) R S) ≫ pullback.snd (tensorObj (𝒞 := instCategoryOver) R S).hom f)
    (pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f)

Tactic:
rw [Monoidal.μ_of_cartesianMonoidalCategory,
    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left,
    ← Over.comp_left_assoc, Iso.hom_inv_id]

Premises used: CategoryTheory.Over.comp_left_assoc, CategoryTheory.Over.pullback, CategoryTheory.Over.Hom.left, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso, 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 R_1 : C
f : R_1 ⟶ X
R S : Over.{v_1, u_1} X
⊢ Hom.left (𝟙 ((pullback f).obj (tensorObj (𝒞 := instCategoryOver) R S))) ≫
      pullback.snd (tensorObj (𝒞 := instCategoryOver) R S).hom f =
    CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((pullback f).obj R) ((pullback f).obj S)).left)
      (Hom.left (Iso.hom (prodComparisonIso (pullback f) R S)))
      (pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.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 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 ⟶ Y)
    (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.fst g₁ g₂))
    (pullback.fst ((pullback f).obj (mk g₁)).hom ((pullback f).obj (mk g₂)).hom ≫ pullback.fst (mk g₁).hom f)

Tactic:
μ_pullback_left_fst_fst ..

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Over.μ_pullback_left_fst_fst