awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m n : M
h₁ : tensorObj.{v_1, u_1} (𝒞 := inst_1) m n ≅ tensorUnit.{v_1, u_1} M (𝒞 := inst_1)
h₂ : tensorObj.{v_1, u_1} (𝒞 := inst_1) n m ≅ tensorUnit.{v_1, u_1} M (𝒞 := inst_1)
H : h₁.hom ▷ m ≫ Iso.hom (λ_ m) = Iso.hom (α_ m n m) ≫ m ◁ h₂.hom ≫ Iso.hom (ρ_ m)
inst_3 : F.Monoidal
X : C
dsimp :
  (F.obj m).map ((unitOfTensorIsoUnit F m n h₁).inv.app X) ≫
      NatTrans.app (μ F n m) ((F.obj m).obj X) ≫
        (F.map h₂.hom).app ((F.obj m).obj X) ≫ NatTrans.app (η F) ((F.obj m).obj X) =
    𝟙 ((F.obj m).obj X)
⊢ (F.obj m).map ((unitOfTensorIsoUnit F m n h₁).symm.hom.app X) ≫
      (unitOfTensorIsoUnit F n m h₂).hom.app ((F.obj m).obj X) =
    𝟙 ((F.obj m).obj X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m n : M
h₁ : tensorObj.{v_1, u_1} (𝒞 := inst_1) m n ≅ tensorUnit.{v_1, u_1} M (𝒞 := inst_1)
h₂ : tensorObj.{v_1, u_1} (𝒞 := inst_1) n m ≅ tensorUnit.{v_1, u_1} M (𝒞 := inst_1)
H : h₁.hom ▷ m ≫ Iso.hom (λ_ m) = Iso.hom (α_ m n m) ≫ m ◁ h₂.hom ≫ Iso.hom (ρ_ m)
inst_3 : F.Monoidal
X : C
simp :
  NatTrans.app (F.map (Iso.inv (λ_ m))) X ≫
      NatTrans.app (F.map (h₁.inv ▷ m)) X ≫
        NatTrans.app (F.map (Iso.hom (α_ m n m))) X ≫
          NatTrans.app (F.map (m ◁ h₂.hom)) X ≫ NatTrans.app (F.map (Iso.hom (ρ_ m))) X =
    𝟙 ((F.obj m).obj X)
⊢ (F.obj m).map ((unitOfTensorIsoUnit F m n h₁).inv.app X) ≫
      NatTrans.app (μ F n m) ((F.obj m).obj X) ≫
        (F.map h₂.hom).app ((F.obj m).obj X) ≫ NatTrans.app (η F) ((F.obj m).obj X) =
    𝟙 ((F.obj m).obj X)

Tactic:
simp only [μ_naturalityᵣ_assoc, μ_naturalityₗ_assoc, η_app_obj, Category.assoc,
      obj_μ_inv_app, Functor.map_comp, δ_μ_app_assoc, obj_ε_app,
      unitOfTensorIsoUnit_inv_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.μ_naturalityᵣ_assoc, CategoryTheory.η_app_obj, CategoryTheory.unitOfTensorIsoUnit_inv_app, CategoryTheory.obj_μ_inv_app, CategoryTheory.Functor.map_comp, CategoryTheory.obj_ε_app, CategoryTheory.δ_μ_app_assoc, CategoryTheory.μ_naturalityₗ_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m n : M
h₁ : tensorObj.{v_1, u_1} (𝒞 := inst_1) m n ≅ tensorUnit.{v_1, u_1} M (𝒞 := inst_1)
h₂ : tensorObj.{v_1, u_1} (𝒞 := inst_1) n m ≅ tensorUnit.{v_1, u_1} M (𝒞 := inst_1)
H : h₁.hom ▷ m ≫ Iso.hom (λ_ m) = Iso.hom (α_ m n m) ≫ m ◁ h₂.hom ≫ Iso.hom (ρ_ m)
inst_3 : F.Monoidal
X : C
⊢ NatTrans.app (F.map (Iso.inv (λ_ m))) X ≫
      NatTrans.app (F.map (h₁.inv ▷ m)) X ≫
        NatTrans.app (F.map (Iso.hom (α_ m n m))) X ≫
          NatTrans.app (F.map (m ◁ h₂.hom)) X ≫ NatTrans.app (F.map (Iso.hom (ρ_ m))) X =
    𝟙 ((F.obj m).obj X)

Tactic:
simp only [← NatTrans.comp_app, ← F.map_comp, ← H, inv_hom_whiskerRight_assoc,
      Iso.inv_hom_id, Functor.map_id, NatTrans.id_app]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.inv_hom_whiskerRight_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
Goal:
J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} J₁
inst_1 : Category.{v₂, u₂} J₂
inst_2 : Category.{v₃, u₃} C
inst_3 : MonoidalCategory.{v₃, u₃} C
x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₁, v₃, u₁, u₃} J₁ C
⊢ ∀ {X Y : J₁} (f : X ⟶ Y),
    (obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).map f ≫
        Iso.hom
          ((fun (x_1 : J₁) ↦
              (Iso.refl
                  ((obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj x_1) :
                (obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj x_1 ≅
                  (obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj x_1))
            Y) =
      Iso.hom
          ((fun (x_1 : J₁) ↦
              (Iso.refl
                  ((obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj x_1) :
                (obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj x_1 ≅
                  (obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj x_1))
            X) ≫
        (obj (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) x).map f

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
Goal:
J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} J₁
inst_1 : Category.{v₂, u₂} J₂
inst_2 : Category.{v₃, u₃} C
inst_3 : MonoidalCategory.{v₃, u₃} C
X Y : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₁, v₃, u₁, u₃} J₁ C
x : X ⟶ Y
x_1 : J₁
⊢ Eq (α :=
    (obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) X).obj x_1 ⟶
      (obj (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) Y).obj x_1)
    (NatTrans.app
      (map (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x ≫
        Iso.hom
          ((fun (x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₁, v₃, u₁, u₃} J₁ C) ↦
              (NatIso.ofComponents
                  (fun (x_2 : J₁) ↦
                    Iso.refl
                      ((obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj
                        x_2))
                  ⋯ :
                obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x ≅
                  obj (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) x))
            Y))
      x_1)
    (NatTrans.app
      (Iso.hom
          ((fun (x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₁, v₃, u₁, u₃} J₁ C) ↦
              (NatIso.ofComponents
                  (fun (x_2 : J₁) ↦
                    Iso.refl
                      ((obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj
                        x_2))
                  ⋯ :
                obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x ≅
                  obj (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) x))
            X) ≫
        map (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) x)
      x_1)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
Goal:
J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} J₁
inst_1 : Category.{v₂, u₂} J₂
inst_2 : Category.{v₃, u₃} C
inst_3 : MonoidalCategory.{v₃, u₃} C
inst_4 : BraidedCategory.{v₃, u₃} C
x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C
⊢ ∀ {X Y : J₂ × J₁} (f : X ⟶ Y),
    (obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) x).map f ≫
        Iso.hom
          ((fun (x_1 : J₂ × J₁) ↦
              (β_ (x.1.obj (obj (Prod.swap J₂ J₁) x_1).1) (x.2.obj (obj (Prod.swap J₂ J₁) x_1).2) :
                tensorObj.{v₃, u₃} (𝒞 := inst_2) (x.1.obj (obj (Prod.swap J₂ J₁) x_1).1)
                    (x.2.obj (obj (Prod.swap J₂ J₁) x_1).2) ≅
                  tensorObj.{v₃, u₃} (𝒞 := inst_2) (x.2.obj (obj (Prod.swap J₂ J₁) x_1).2)
                    (x.1.obj (obj (Prod.swap J₂ J₁) x_1).1)))
            Y) =
      Iso.hom
          ((fun (x_1 : J₂ × J₁) ↦
              (β_ (x.1.obj (obj (Prod.swap J₂ J₁) x_1).1) (x.2.obj (obj (Prod.swap J₂ J₁) x_1).2) :
                tensorObj.{v₃, u₃} (𝒞 := inst_2) (x.1.obj (obj (Prod.swap J₂ J₁) x_1).1)
                    (x.2.obj (obj (Prod.swap J₂ J₁) x_1).2) ≅
                  tensorObj.{v₃, u₃} (𝒞 := inst_2) (x.2.obj (obj (Prod.swap J₂ J₁) x_1).2)
                    (x.1.obj (obj (Prod.swap J₂ J₁) x_1).1)))
            X) ≫
        (obj
              (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
                externalProductBifunctor J₂ J₁ C)
              x).map
          f

Tactic:
simp [whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
Goal:
J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} J₁
inst_1 : Category.{v₂, u₂} J₂
inst_2 : Category.{v₃, u₃} C
inst_3 : MonoidalCategory.{v₃, u₃} C
inst_4 : BraidedCategory.{v₃, u₃} C
X Y : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C
x : X ⟶ Y
x_1 : J₂ × J₁
⊢ Eq (α :=
    (obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) X).obj x_1 ⟶
      (obj
            (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
              externalProductBifunctor J₂ J₁ C)
            Y).obj
        x_1)
    (NatTrans.app
      (map (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) x ≫
        Iso.hom
          ((fun (x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C) ↦
              (NatIso.ofComponents
                  (fun (x_2 : J₂ × J₁) ↦
                    β_ (x.1.obj (obj (Prod.swap J₂ J₁) x_2).1) (x.2.obj (obj (Prod.swap J₂ J₁) x_2).2))
                  ⋯ :
                obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁))
                    x ≅
                  obj
                    (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
                      externalProductBifunctor J₂ J₁ C)
                    x))
            Y))
      x_1)
    (NatTrans.app
      (Iso.hom
          ((fun (x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C) ↦
              (NatIso.ofComponents
                  (fun (x_2 : J₂ × J₁) ↦
                    β_ (x.1.obj (obj (Prod.swap J₂ J₁) x_2).1) (x.2.obj (obj (Prod.swap J₂ J₁) x_2).2))
                  ⋯ :
                obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁))
                    x ≅
                  obj
                    (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
                      externalProductBifunctor J₂ J₁ C)
                    x))
            X) ≫
        map
          (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙ externalProductBifunctor J₂ J₁ C)
          x)
      x_1)

Tactic:
simp [whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (L.prod (𝟭 E)) (d, e))
  (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence L (𝟭 E) d e)
apply :
  Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)))
⊢ (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).IsPointwiseLeftKanExtensionAt (d, e)

Tactic:
apply Limits.IsColimit.ofWhiskerEquivalence equiv

Premises used: CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (L.prod (𝟭 E)) (d, e))
  (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence L (𝟭 E) d e)
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e :=
  Equivalence.inverse (prod.rightUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (𝟭 (CostructuredArrow L d))
      (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
this : Functor.Final (D := CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e)
  (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))) :=
  ⋯
apply :
  Functor.Final (C := CostructuredArrow L d × Discrete PUnit.{1}) (D :=
    CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e)
    (Functor.prod (𝟭 (CostructuredArrow L d)) (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))))
⊢ I.Final

Tactic:
apply Iff.mp <| Functor.final_iff_final_comp
      (F := (prod.rightUnitorEquivalence <| CostructuredArrow L d).inverse)
      (G := (𝟭 _).prod <| Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e))

Premises used: CategoryTheory.Functor.id, CategoryTheory.CategoryStruct.id, CategoryTheory.CostructuredArrow, CategoryTheory.Functor.prod, CategoryTheory.Functor.final_iff_final_comp, Iff.mp, CategoryTheory.CostructuredArrow.mk, CategoryTheory.prod.rightUnitorEquivalence, CategoryTheory.Functor.fromPUnit, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (L.prod (𝟭 E)) (d, e))
  (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence L (𝟭 E) d e)
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e :=
  Equivalence.inverse (prod.rightUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (𝟭 (CostructuredArrow L d))
      (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
this : Functor.Final (D := CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e)
  (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))) :=
  ⋯
⊢ Functor.Final (C := CostructuredArrow L d × Discrete PUnit.{1}) (D :=
    CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e)
    (Functor.prod (𝟭 (CostructuredArrow L d)) (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (L.prod (𝟭 E)) (d, e))
  (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence L (𝟭 E) d e)
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e :=
  Equivalence.inverse (prod.rightUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (𝟭 (CostructuredArrow L d))
      (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
this : I.Final := ⋯
apply : Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
⊢ Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)))

Tactic:
apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone) |>.toFun

Premises used: CategoryTheory.Limits.Cocone.whisker, CategoryTheory.Equivalence.functor, Equiv.toFun, CategoryTheory.Functor.Final.isColimitWhiskerEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (L.prod (𝟭 E)) (d, e))
  (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence L (𝟭 E) d e)
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e :=
  Equivalence.inverse (prod.rightUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (𝟭 (CostructuredArrow L d))
      (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
this : I.Final := ⋯
diag_iso : (CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e) ≅
  I ⋙ equiv.functor ⋙ CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K :=
  NatIso.ofComponents
    (fun (x : CostructuredArrow L d) ↦ Iso.refl (((CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e)).obj x)) ⋯
apply :
  Limits.IsColimit (F := (CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e))
    (Functor.mapCocone (tensorRight (K.obj e)) ((Functor.LeftExtension.mk H' α).coconeAt d))
⊢ Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))

Tactic:
apply Limits.IsColimit.equivOfNatIsoOfIso diag_iso
    (d := Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
    (c := tensorRight (K.obj e) |>.mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d)
    (Limits.Cocone.ext <| .refl _) |>.toFun

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.LeftExtension.mk, CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, Equiv.toFun, CategoryTheory.Functor.LeftExtension.coconeAt, CategoryTheory.MonoidalCategory.tensorRight, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (L.prod (𝟭 E)) (d, e))
  (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence L (𝟭 E) d e)
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e :=
  Equivalence.inverse (prod.rightUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (𝟭 (CostructuredArrow L d))
      (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
this : I.Final := ⋯
diag_iso : (CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e) ≅
  I ⋙ equiv.functor ⋙ CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K :=
  NatIso.ofComponents
    (fun (x : CostructuredArrow L d) ↦ Iso.refl (((CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e)).obj x)) ⋯
⊢ Limits.IsColimit (F := (CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e))
    (Functor.mapCocone (tensorRight (K.obj e)) ((Functor.LeftExtension.mk H' α).coconeAt d))

Tactic:
exact Limits.PreservesColimit.preserves (F := tensorRight <| K.obj e) P |>.some

Premises used: Nonempty.some, CategoryTheory.Limits.PreservesColimit.preserves
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (Functor.prod (𝟭 E) L) (e, d))
  (CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d ≌
  CostructuredArrow (Functor.prod (𝟭 E) L) (e, d) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence (𝟭 E) L e d)
apply :
  Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)))
⊢ (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).IsPointwiseLeftKanExtensionAt (e, d)

Tactic:
apply Limits.IsColimit.ofWhiskerEquivalence equiv

Premises used: CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence