awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Y Z : Over.{v₁, u₁} X
inst_1 : ChosenPullbacksAlong Z.hom
T : Over.{v₁, u₁} X
a : T ⟶ Y
b : T ⟶ Z
m : T ⟶ (binaryFan Y Z).pt
h₁ : m ≫ (binaryFan Y Z).fst = a
h₂ : m ≫ (binaryFan Y Z).snd = b
h :
  Over.Hom.left m =
    Over.Hom.left
      ((fun {T : Over.{v₁, u₁} X} (u : T ⟶ Y) (v : T ⟶ Z) ↦
          (Over.homMk (lift (Over.Hom.left u) (Over.Hom.left v) ⋯) ⋯ : T ⟶ (binaryFan Y Z).pt))
        a b)
⊢ m =
    (fun {T : Over.{v₁, u₁} X} (u : T ⟶ Y) (v : T ⟶ Z) ↦
        (Over.homMk (lift (Over.Hom.left u) (Over.Hom.left v) ⋯) ⋯ : T ⟶ (binaryFan Y Z).pt))
      a b

Tactic:
ext
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Y Z : Over.{v₁, u₁} X
inst_1 : ChosenPullbacksAlong Z.hom
T : Over.{v₁, u₁} X
a : T ⟶ Y
b : T ⟶ Z
m : T ⟶ (binaryFan Y Z).pt
h₁ : m ≫ (binaryFan Y Z).fst = a
h₂ : m ≫ (binaryFan Y Z).snd = b
h : Over.Hom.left m = lift (Over.Hom.left a) (Over.Hom.left b) ⋯
⊢ Over.Hom.left m =
    Over.Hom.left
      ((fun {T : Over.{v₁, u₁} X} (u : T ⟶ Y) (v : T ⟶ Z) ↦
          (Over.homMk (lift (Over.Hom.left u) (Over.Hom.left v) ⋯) ⋯ : T ⟶ (binaryFan Y Z).pt))
        a b)

Tactic:
dsimp [Over.map, Comma.mapRight]

Premises used: CategoryTheory.Over.map, CategoryTheory.Comma.mapRight
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y : Over.{v₁, u₁} X
m : Y ⟶ Over.mk (𝟙 X)
⊢ Over.Hom.left m = Over.Hom.left ((fun (Y : Over.{v₁, u₁} X) ↦ (Over.homMk Y.hom ⋯ : Y ⟶ Over.mk (𝟙 X))) Y)

Tactic:
simpa using m.w

Premises used: CategoryTheory.Over.Hom.w
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X A : C
Y Z : Over.{v₁, u₁} X
f₁ f₂ : A ⟶ (tensorObj (𝒞 := instCategoryOver) Y Z).left
e₁ : f₁ ≫ fst Y.hom Z.hom = f₂ ≫ fst Y.hom Z.hom
e₂ : f₁ ≫ snd Y.hom Z.hom = f₂ ≫ snd Y.hom Z.hom
⊢ f₁ = f₂

Tactic:
hom_ext Y.hom Z.hom e₁ e₂

Premises used: CategoryTheory.Over, CategoryTheory.ChosenPullbacksAlong.hom_ext, CategoryTheory.CostructuredArrow, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y Z : Over.{v₁, u₁} X
⊢ (tensorObj (𝒞 := instCategoryOver) Y Z).left = pullbackObj Y.hom Z.hom

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y Z : Over.{v₁, u₁} X
⊢ (tensorObj (𝒞 := instCategoryOver) Y Z).hom = snd Y.hom Z.hom ≫ Z.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
⊢ Over.left.{v₁, u₁} (X := X) ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver)) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := Over.left.{v₁, u₁} (X := X) ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver)) ⟶ X)
    (Over.hom ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver))) (𝟙 X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y Z : Over.{v₁, u₁} X
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := instCategoryOver) Y Z ⟶ Y) (SemiCartesianMonoidalCategory.fst Y Z)
    (fst' Y.hom Z.hom)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y Z : Over.{v₁, u₁} X
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := instCategoryOver) Y Z ⟶ Z) (SemiCartesianMonoidalCategory.snd Y Z)
    (snd' Y.hom Z.hom)

Tactic:
rfl

Premises used: CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Over.homMk, rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
W Y Z : Over.{v₁, u₁} X
f : W ⟶ Y
g : W ⟶ Z
⊢ Eq (α := W.left ⟶ (tensorObj (𝒞 := instCategoryOver) Y Z).left) (Over.Hom.left (CartesianMonoidalCategory.lift f g))
    (lift (Over.Hom.left f) (Over.Hom.left g) ⋯)

Tactic:
rfl

Premises used: CategoryTheory.ChosenPullbacksAlong.lift, rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Z : Over.{v₁, u₁} X
⊢ Over.Hom.left (toUnit Z) = Z.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) (tensorObj (𝒞 := instCategoryOver) R S) T).left ⟶ R.left)
    (Over.Hom.left (Iso.hom (α_ R S T)) ≫ fst R.hom (snd S.hom T.hom ≫ T.hom))
    (fst (tensorObj (𝒞 := instCategoryOver) R S).hom T.hom ≫ fst R.hom S.hom)

Tactic:
congr_arg CommaMorphism.left (associator_hom_fst R S T)

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.CartesianMonoidalCategory.associator_hom_fst, congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) (tensorObj (𝒞 := instCategoryOver) R S) T).left ⟶ S.left)
    (Over.Hom.left (Iso.hom (α_ R S T)) ≫ snd R.hom (snd S.hom T.hom ≫ T.hom) ≫ fst S.hom T.hom)
    (fst (tensorObj (𝒞 := instCategoryOver) R S).hom T.hom ≫ snd R.hom S.hom)

Tactic:
congr_arg CommaMorphism.left (associator_hom_snd_fst R S T)

Premises used: CategoryTheory.Over, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) (tensorObj (𝒞 := instCategoryOver) R S) T).left ⟶ T.left)
    (Over.Hom.left (Iso.hom (α_ R S T)) ≫ snd R.hom (snd S.hom T.hom ≫ T.hom) ≫ snd S.hom T.hom)
    (snd (tensorObj (𝒞 := instCategoryOver) R S).hom T.hom)

Tactic:
congr_arg CommaMorphism.left (associator_hom_snd_snd R S T)

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R (tensorObj (𝒞 := instCategoryOver) S T)).left ⟶ R.left)
    (Over.Hom.left (Iso.inv (α_ R S T)) ≫ fst (snd R.hom S.hom ≫ S.hom) T.hom ≫ fst R.hom S.hom)
    (fst R.hom (tensorObj (𝒞 := instCategoryOver) S T).hom)

Tactic:
congr_arg CommaMorphism.left (associator_inv_fst_fst R S T)

Premises used: CategoryTheory.Over, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R (tensorObj (𝒞 := instCategoryOver) S T)).left ⟶ S.left)
    (Over.Hom.left (Iso.inv (α_ R S T)) ≫ fst (snd R.hom S.hom ≫ S.hom) T.hom ≫ snd R.hom S.hom)
    (snd R.hom (tensorObj (𝒞 := instCategoryOver) S T).hom ≫ fst S.hom T.hom)

Tactic:
congr_arg CommaMorphism.left (associator_inv_fst_snd R S T)

Premises used: CategoryTheory.Over, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R (tensorObj (𝒞 := instCategoryOver) S T)).left ⟶ T.left)
    (Over.Hom.left (Iso.inv (α_ R S T)) ≫ snd (snd R.hom S.hom ≫ S.hom) T.hom)
    (snd R.hom (tensorObj (𝒞 := instCategoryOver) S T).hom ≫ snd S.hom T.hom)

Tactic:
congr_arg CommaMorphism.left (associator_inv_snd R S T)

Premises used: CategoryTheory.Over, CategoryTheory.CartesianMonoidalCategory.associator_inv_snd, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Z : Over.{v₁, u₁} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver)) Z).left ⟶ Z.left)
    (Over.Hom.left (Iso.hom (λ_ Z))) (snd (Over.hom ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver))) Z.hom)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Z : Over.{v₁, u₁} X
⊢ CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver)) Z).left)
      (Over.Hom.left (Iso.inv (λ_ Z))) (fst (𝟙 X) Z.hom) =
    Z.hom

Tactic:
congr_arg CommaMorphism.left (leftUnitor_inv_fst Z)

Premises used: congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y : Over.{v₁, u₁} X
⊢ CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver)) Y).left)
      (Over.Hom.left (Iso.inv (λ_ Y))) (snd (𝟙 X) Y.hom) =
    𝟙 Y.left

Tactic:
congr_arg CommaMorphism.left (leftUnitor_inv_snd Y)

Premises used: CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd, congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y : Over.{v₁, u₁} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) Y ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver))).left ⟶ Y.left)
    (Over.Hom.left (Iso.hom (ρ_ Y))) (fst Y.hom (𝟙 X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y : Over.{v₁, u₁} X
⊢ CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) Y ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver))).left)
      (Over.Hom.left (Iso.inv (ρ_ Y))) (fst Y.hom (𝟙 X)) =
    𝟙 Y.left

Tactic:
congr_arg CommaMorphism.left (rightUnitor_inv_fst Y)

Premises used: CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst, congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
Y : Over.{v₁, u₁} X
⊢ CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategoryOver) Y ((𝟙_ (Over.{v₁, u₁} X)) (𝒞 := instCategoryOver))).left)
      (Over.Hom.left (Iso.inv (ρ_ Y))) (snd Y.hom (𝟙 X)) =
    Y.hom

Tactic:
congr_arg CommaMorphism.left (rightUnitor_inv_snd Y)

Premises used: congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ (tensorObj (𝒞 := instCategoryOver) R T).left)
    (Over.Hom.left (R ◁ f)) (pullbackMap R.hom T.hom R.hom S.hom (𝟙 R.left) (Over.Hom.left f) (𝟙 X) ⋯ ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.ChosenPullbacksAlong.lift, rfl, CategoryTheory.ChosenPullbacksAlong.pullbackMap
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ R.left) (Over.Hom.left (R ◁ f) ≫ fst R.hom T.hom)
    (fst R.hom S.hom)

Tactic:
congr_arg CommaMorphism.left (whiskerLeft_fst R f)

Premises used: congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ T.left) (Over.Hom.left (R ◁ f) ≫ snd R.hom T.hom)
    (snd R.hom S.hom ≫ Over.Hom.left f)

Tactic:
congr_arg CommaMorphism.left (whiskerLeft_snd R f)

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) S R).left ⟶ (tensorObj (𝒞 := instCategoryOver) T R).left)
    (Over.Hom.left (f ▷ R)) (pullbackMap T.hom R.hom S.hom R.hom (Over.Hom.left f) (𝟙 R.left) (𝟙 X) ⋯ ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.ChosenPullbacksAlong.lift, rfl, CategoryTheory.ChosenPullbacksAlong.pullbackMap
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) S R).left ⟶ T.left) (Over.Hom.left (f ▷ R) ≫ fst T.hom R.hom)
    (fst S.hom R.hom ≫ Over.Hom.left f)

Tactic:
congr_arg CommaMorphism.left (whiskerRight_fst f R)

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T : Over.{v₁, u₁} X
f : S ⟶ T
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) S R).left ⟶ R.left) (Over.Hom.left (f ▷ R) ≫ snd T.hom R.hom)
    (snd S.hom R.hom)

Tactic:
congr_arg CommaMorphism.left (whiskerRight_snd f R)

Premises used: congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T U : Over.{v₁, u₁} X
f : R ⟶ S
g : T ⟶ U
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R T).left ⟶ (tensorObj (𝒞 := instCategoryOver) S U).left)
    (Over.Hom.left (f ⊗ₘ g)) (pullbackMap S.hom U.hom R.hom T.hom (Over.Hom.left f) (Over.Hom.left g) (𝟙 X) ⋯ ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.ChosenPullbacksAlong.lift, rfl, CategoryTheory.ChosenPullbacksAlong.pullbackMap
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T U : Over.{v₁, u₁} X
f : R ⟶ S
g : T ⟶ U
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R T).left ⟶ S.left) (Over.Hom.left (f ⊗ₘ g) ≫ fst S.hom U.hom)
    (fst R.hom T.hom ≫ Over.Hom.left f)

Tactic:
congr_arg CommaMorphism.left (tensorHom_fst f g)

Premises used: CategoryTheory.Over, CategoryTheory.CartesianMonoidalCategory.tensorHom_fst, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : ChosenPullbacks.{v₁, u₁} C
X : C
R S T U : Over.{v₁, u₁} X
f : R ⟶ S
g : T ⟶ U
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R T).left ⟶ U.left) (Over.Hom.left (f ⊗ₘ g) ≫ snd S.hom U.hom)
    (snd R.hom T.hom ≫ Over.Hom.left g)

Tactic:
congr_arg CommaMorphism.left (tensorHom_snd f g)

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X A A' : C
f : A ⟶ A'
⊢ Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X) (Functor.obj (toOver X) A) (Functor.obj (toOver X) A'))
    (Functor.map (toOver X) f) (Over.homMk (f ▷ X) ⋯)

Tactic:
simp [toOver]

Premises used: CategoryTheory.toOver
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
Z : Over.{v₁, u₁} X
A : C
f : Z ⟶ Functor.obj (toOver X) A
rw :
  Functor.map (Over.forget X) f ≫ SemiCartesianMonoidalCategory.fst A X =
    Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X
⊢ (Equiv.symm (Adjunction.homEquiv (forgetAdjToOver X) Z A) : (a : Z ⟶ (toOver X).obj A) → (Over.forget X).obj Z ⟶ A)
      f =
    Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X

Tactic:
rw [Adjunction.homEquiv_counit, forgetAdjToOver_counit_app]

Premises used: CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.forgetAdjToOver_counit_app
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
Z : Over.{v₁, u₁} X
A : C
f : Z ⟶ Functor.obj (toOver X) A
⊢ Functor.map (Over.forget X) f ≫ SemiCartesianMonoidalCategory.fst A X =
    Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
A : C
a :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) I A ⟶ I) (uncurry (toUnit A ≫ curryRightUnitorHom I))
    (uncurry (curry (fst I A)))
⊢ Eq.{v₁ + 1} (α := A ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I) (toUnit A ≫ curryRightUnitorHom I) (curry (fst I A))

Tactic:
apply uncurry_injective

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
A : C
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) I A ⟶ I) (uncurry (toUnit A ≫ curryRightUnitorHom I))
    (uncurry (curry (fst I A)))

Tactic:
simp [uncurry_natural_left, curryRightUnitorHom, fst_def, toUnit]

Premises used: CategoryTheory.curryRightUnitorHom, CategoryTheory.MonoidalClosed.uncurry_natural_left, CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
X Y : Over.{v₁, u₁} I
u : X ⟶ Y
⊢ Functor.map (ihom I) X.hom ≫ 𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I) =
    Functor.map (ihom I) (Hom.left u) ≫ Functor.map (ihom I) Y.hom

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
X : Over.{v₁, u₁} I
A : C
u : Functor.obj (toOver I) A ⟶ X
rw :
  Eq.{v₁ + 1} (α := A ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curry (Iso.hom (β_ I A) ≫ hom (Functor.obj (toOver I) A))) (curry (SemiCartesianMonoidalCategory.fst I A))
⊢ Eq (α := A ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curry (Iso.hom (β_ I A) ≫ Hom.left u) ≫ Functor.map (ihom I) X.hom) (toUnit A ≫ curryRightUnitorHom I)

Tactic:
rw [curry_natural_right, Category.assoc, ← Functor.map_comp, w,
      ← curry_natural_right, toUnit_comp_curryRightUnitorHom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Over.w, CategoryTheory.Functor.map_comp, CategoryTheory.MonoidalClosed.curry_natural_right, CategoryTheory.toUnit_comp_curryRightUnitorHom
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
X : Over.{v₁, u₁} I
A : C
u : Functor.obj (toOver I) A ⟶ X
e_a :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) I A ⟶ I) (Iso.hom (β_ I A) ≫ hom (Functor.obj (toOver I) A))
    (SemiCartesianMonoidalCategory.fst I A)
⊢ Eq.{v₁ + 1} (α := A ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curry (Iso.hom (β_ I A) ≫ hom (Functor.obj (toOver I) A))) (curry (SemiCartesianMonoidalCategory.fst I A))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
X : Over.{v₁, u₁} I
A : C
u : Functor.obj (toOver I) A ⟶ X
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) I A ⟶ I) (Iso.hom (β_ I A) ≫ hom (Functor.obj (toOver I) A))
    (SemiCartesianMonoidalCategory.fst I A)

Tactic:
simp [braiding_hom_snd]

Premises used: CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
X : Over.{v₁, u₁} I
A : C
v : A ⟶ Functor.obj (sections I) X
v₂ : A ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left :=
  v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curryRightUnitorHom I)
rw :
  (v ≫ ChosenPullbacksAlong.snd (Functor.map (ihom I) X.hom) (curryRightUnitorHom I)) ≫ curryRightUnitorHom I =
    v₂ ≫ Functor.map (ihom I) X.hom
⊢ toUnit A ≫ curryRightUnitorHom I = v₂ ≫ Functor.map (ihom I) X.hom

Tactic:
rw [IsTerminal.hom_ext isTerminalTensorUnit (toUnit A) (v ≫ snd ..)]

Premises used: CategoryTheory.ChosenPullbacksAlong.snd, CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.SemiCartesianMonoidalCategory.toUnit