awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (v ≫ ChosenPullbacksAlong.snd (Functor.map (ihom I) X.hom) (curryRightUnitorHom I)) ≫ curryRightUnitorHom I =
    v₂ ≫ Functor.map (ihom I) X.hom

Tactic:
simp [v₂, condition]

Premises used: CategoryTheory.ChosenPullbacksAlong.condition
-- 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)
⊢ toUnit A ≫ curryRightUnitorHom I = v₂ ≫ Functor.map (ihom I) X.hom

Tactic:
have comm : toUnit A ≫ (curryRightUnitorHom I) = v₂ ≫ (ihom I).map X.hom := by
      rw [IsTerminal.hom_ext isTerminalTensorUnit (toUnit A) (v ≫ snd ..)]
      simp [v₂, condition]
-- 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)
comm : toUnit A ≫ curry (Iso.hom (ρ_ I)) = v₂ ≫ Functor.map (ihom I) X.hom
⊢ Eq.{v₁ + 1} (α := Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft I) A ⟶ I)
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft I) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Functor.map (tensorLeft I) (toUnit A))
      ((Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) I) :
          (a : 𝟙_ C ⟶ (ihom I).obj I) → (tensorLeft I).obj (𝟙_ C) ⟶ I)
        (curry (Iso.hom (ρ_ I)))))
    ((Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) A X.left) :
          (a : A ⟶ (ihom I).obj X.left) → (tensorLeft I).obj A ⟶ X.left)
        v₂ ≫
      X.hom)

Tactic:
have w' := (ihom.adjunction I).homEquiv_naturality_right_square _ _ _ _ comm
-- 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)
comm : toUnit A ≫ curry (Iso.hom (ρ_ I)) = v₂ ≫ Functor.map (ihom I) X.hom
w' :
  Eq.{v₁ + 1} (α := Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft I) A ⟶ I)
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft I) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Functor.map (tensorLeft I) (toUnit A))
      ((Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) I) :
          (a : 𝟙_ C ⟶ (ihom I).obj I) → (tensorLeft I).obj (𝟙_ C) ⟶ I)
        (curry (Iso.hom (ρ_ I)))))
    ((Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) A X.left) :
          (a : A ⟶ (ihom I).obj X.left) → (tensorLeft I).obj A ⟶ X.left)
        v₂ ≫
      X.hom)
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) I A ⟶ I) (I ◁ toUnit A ≫ Iso.hom (ρ_ I))
    ((Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) A X.left) : (a : A ⟶ (ihom I).obj X.left) → I ⊗ A ⟶ X.left)
        v₂ ≫
      X.hom)

Tactic:
simp only [curriedTensor_obj_obj, curriedTensor_obj_map, curry,
      Equiv.symm_apply_apply] at w'

Premises used: Equiv.symm_apply_apply, CategoryTheory.MonoidalCategory.curriedTensor_obj_map, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, CategoryTheory.MonoidalClosed.curry
-- 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)
comm : toUnit A ≫ curry (Iso.hom (ρ_ I)) = v₂ ≫ Functor.map (ihom I) X.hom
w' :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) I A ⟶ I) (I ◁ toUnit A ≫ Iso.hom (ρ_ I))
    ((Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) A X.left) : (a : A ⟶ (ihom I).obj X.left) → I ⊗ A ⟶ X.left)
        v₂ ≫
      X.hom)
dsimp :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A I ⟶ I)
    ((Iso.hom (β_ A I) ≫
        (Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) A X.left) : (a : A ⟶ (ihom I).obj X.left) → I ⊗ A ⟶ X.left)
          v₂) ≫
      X.hom)
    (SemiCartesianMonoidalCategory.snd A I)
⊢ (Iso.hom (β_ A I) ≫ uncurry v₂) ≫ X.hom = hom (Functor.obj (toOver I) A)

Tactic:
dsimp [uncurry] at *

Premises used: CategoryTheory.MonoidalClosed.uncurry
-- 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)
comm : toUnit A ≫ curry (Iso.hom (ρ_ I)) = v₂ ≫ Functor.map (ihom I) X.hom
w' :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) I A ⟶ I) (I ◁ toUnit A ≫ Iso.hom (ρ_ I))
    ((Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) A X.left) : (a : A ⟶ (ihom I).obj X.left) → I ⊗ A ⟶ X.left)
        v₂ ≫
      X.hom)
rw :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A I ⟶ I)
    (Iso.hom (β_ A I) ≫
      (Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) A X.left) : (a : A ⟶ (ihom I).obj X.left) → I ⊗ A ⟶ X.left)
          v₂ ≫
        X.hom)
    (SemiCartesianMonoidalCategory.snd A I)
rw₁ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A I ⟶ I) (Iso.hom (β_ A I) ≫ I ◁ toUnit A ≫ Iso.hom (ρ_ I))
    (SemiCartesianMonoidalCategory.snd A I)
rw₂ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A I ⟶ I) (Iso.hom (β_ A I) ≫ SemiCartesianMonoidalCategory.fst I A)
    (SemiCartesianMonoidalCategory.snd A I)
rw₃ rw₄ :
  Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A I ⟶ I) (SemiCartesianMonoidalCategory.snd A I)
    (SemiCartesianMonoidalCategory.snd A I)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A I ⟶ I)
    ((Iso.hom (β_ A I) ≫
        (Equiv.symm (Adjunction.homEquiv (ihom.adjunction I) A X.left) : (a : A ⟶ (ihom I).obj X.left) → I ⊗ A ⟶ X.left)
          v₂) ≫
      X.hom)
    (SemiCartesianMonoidalCategory.snd A I)

Tactic:
rw [Category.assoc, ← w', whiskerLeft_toUnit_comp_rightUnitor_hom, braiding_hom_fst]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom, CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst
-- 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
dsimp :
  ChosenPullbacksAlong.lift
      (curry
        (Iso.hom (β_ I A) ≫
          Iso.hom (β_ A I) ≫
            uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curryRightUnitorHom I))))
      (toUnit A) ⋯ =
    v
⊢ sectionsCurry (sectionsUncurry v) = v

Tactic:
dsimp [sectionsCurry, sectionsUncurry]

Premises used: CategoryTheory.Over.sectionsCurry, CategoryTheory.Over.sectionsUncurry
-- 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
dsimp :
  homMk
      (Iso.hom (β_ A I) ≫
        uncurry
          (CategoryStruct.comp (Y :=
            pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
              (curryRightUnitorHom I))
            (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
            (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curryRightUnitorHom I))))
      ⋯ =
    u
⊢ sectionsUncurry (sectionsCurry u) = u

Tactic:
dsimp [sectionsCurry, sectionsUncurry]

Premises used: CategoryTheory.Over.sectionsCurry, CategoryTheory.Over.sectionsUncurry
-- 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
h :
  Hom.left
      (homMk
        (Iso.hom (β_ A I) ≫
          uncurry
            (CategoryStruct.comp (Y :=
              pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
                (curryRightUnitorHom I))
              (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
              (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curryRightUnitorHom I))))
        ⋯) =
    Hom.left u
⊢ homMk
      (Iso.hom (β_ A I) ≫
        uncurry
          (CategoryStruct.comp (Y :=
            pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
              (curryRightUnitorHom I))
            (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
            (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curryRightUnitorHom I))))
      ⋯ =
    u

Tactic:
ext
-- 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
⊢ Hom.left
      (homMk
        (Iso.hom (β_ A I) ≫
          uncurry
            (CategoryStruct.comp (Y :=
              pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
                (curryRightUnitorHom I))
              (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
              (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curryRightUnitorHom I))))
        ⋯) =
    Hom.left u

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
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
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
dsimp :
  homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    Functor.map (toOver I) g ≫
      homMk
        (Iso.hom (β_ A I) ≫
          uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
        ⋯
⊢ Eq (α := Functor.obj (toOver I) A' ⟶ X)
    ((Equiv.symm { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } :
          (a : A' ⟶ (sections I).obj X) → (toOver I).obj A' ⟶ X)
        (g ≫ v) :
      Functor.obj (toOver I) A' ⟶ X)
    (Functor.map (toOver I) g ≫
        (Equiv.symm { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } :
            (a : A ⟶ (sections I).obj X) → (toOver I).obj A ⟶ X)
          v :
      Functor.obj (toOver I) A' ⟶ X)

Tactic:
dsimp [sectionsCurry, sectionsUncurry, curryRightUnitorHom]

Premises used: CategoryTheory.curryRightUnitorHom, CategoryTheory.Over.sectionsCurry, CategoryTheory.Over.sectionsUncurry
-- 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
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
simp :
  homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    homMk (g ▷ I) ⋯ ≫
      homMk
        (Iso.hom (β_ A I) ≫
          uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
        ⋯
⊢ homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    Functor.map (toOver I) g ≫
      homMk
        (Iso.hom (β_ A I) ≫
          uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
        ⋯

Tactic:
simp only [toOver_map]

Premises used: CategoryTheory.toOver_map
-- 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
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
rw :
  homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    homMk
      (g ▷ I ≫
        Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯
⊢ homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    homMk (g ▷ I) ⋯ ≫
      homMk
        (Iso.hom (β_ A I) ≫
          uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
        ⋯

Tactic:
rw [← Over.homMk_comp]

Premises used: CategoryTheory.Over.homMk_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
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
e_f :
  Iso.hom (β_ A' I) ≫
      uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))) =
    g ▷ I ≫
      Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))))
⊢ homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    homMk
      (g ▷ I ≫
        Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯

Tactic:
congr 1
-- 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
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
⊢ Iso.hom (β_ A' I) ≫
      uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))) =
    g ▷ I ≫
      Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))))

Tactic:
simp [uncurry_natural_left]

Premises used: CategoryTheory.MonoidalClosed.uncurry_natural_left
-- 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
A : C
X' X : Over.{v₁, u₁} I
u : Functor.obj (toOver I) A ⟶ X'
g : X' ⟶ X
dsimp :
  Eq (α :=
    A ⟶
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
    (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯)
    (CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))))
      (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
      (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) ⋯ ⋯))
⊢ Eq (α := A ⟶ Functor.obj (sections I) X)
    (({ toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } :
          (a : (toOver I).obj A ⟶ X) → A ⟶ (sections I).obj X)
        (u ≫ g) :
      A ⟶ Functor.obj (sections I) X)
    (({ toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } :
            (a : (toOver I).obj A ⟶ X') → A ⟶ (sections I).obj X')
          u ≫
        Functor.map (sections I) g :
      A ⟶ Functor.obj (sections I) X)

Tactic:
dsimp [sectionsCurry, sectionsUncurry, curryRightUnitorHom]

Premises used: CategoryTheory.curryRightUnitorHom, CategoryTheory.Over.sectionsCurry, CategoryTheory.Over.sectionsUncurry
-- 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
A : C
X' X : Over.{v₁, u₁} I
u : Functor.obj (toOver I) A ⟶ X'
g : X' ⟶ X
⊢ CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
      (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯)
      (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))) =
    CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
      (CategoryStruct.comp (Y :=
        pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
          (curry (Iso.hom (ρ_ I))))
        (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
        (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
          (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) ⋯ ⋯))
      (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))))

Tactic:
simp [← curry_natural_right]

Premises used: CategoryTheory.MonoidalClosed.curry_natural_right
-- 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
A : C
X' X : Over.{v₁, u₁} I
u : Functor.obj (toOver I) A ⟶ X'
g : X' ⟶ X
⊢ CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
      (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯)
      (ChosenPullbacksAlong.snd (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))) =
    CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
      (CategoryStruct.comp (Y :=
        pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
          (curry (Iso.hom (ρ_ I))))
        (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
        (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
          (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) ⋯ ⋯))
      (ChosenPullbacksAlong.snd (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))))

Tactic:
simp