awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
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₁ m₂ m₃ : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X) ⟶
      (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X))
    (NatTrans.app (μ F m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
        NatTrans.app (F.map (Iso.inv (α_ m₁ m₂ m₃))) X ≫
          NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
have rw : Eq (α :=
  (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X) ⟶
    (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X))
  ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X))
  ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X) ≫
    NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
      NatTrans.app (F.map (Iso.hom (α_ m₁ m₂ m₃))) X ≫
        NatTrans.app (F.map (Iso.inv (α_ m₁ m₂ m₃))) X ≫
          NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
Tactic: rw [← associativity_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
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₁ m₂ m₃ : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
      (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
    (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
      NatTrans.app (F.map (Iso.hom (α_ m₁ m₂ m₃))) X ≫
        NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
          NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))
have rw : Eq (α :=
  (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
    (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X))
  ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
  (CategoryStruct.comp (Y :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃)).obj X)
    (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
      (NatTrans.app
        (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃ ≫
          δ F m₁ m₂ ▷ F.obj m₃ ≫
            Iso.hom (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)) ≫
              F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))
        X)
      (NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
        NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))))
Tactic: rw [map_associator]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
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₁ m₂ m₃ : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
      (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃)).obj X)
      (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
      (CategoryStruct.comp (Y :=
        (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
        (NatTrans.app
          (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃ ≫
            δ F m₁ m₂ ▷ F.obj m₃ ≫
              Iso.hom (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)) ≫
                F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))
          X)
        (NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
          NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))))
have dsimp : Eq (α :=
  (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
    (F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X)))
  ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
  (CategoryStruct.comp (Y :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃)).obj X)
    (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
      (NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
        (F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X) ≫
          𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
            NatTrans.app (μ F m₂ m₃) ((F.obj m₁).obj X) ≫
              NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X)
      (NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
        NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
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 : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst_3 : F.Monoidal
⊢ (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).map f ≫
      NatTrans.app (μ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y =
    NatTrans.app (η F) X ≫ f ≫ NatTrans.app (F.map (Iso.inv (ρ_ m))) Y
have rw : CategoryStruct.comp (Y := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj Y)
    (NatTrans.app (ε F) X ≫
      (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).map f ≫
        NatTrans.app (μ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y)
    (NatTrans.app (δ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y) =
  CategoryStruct.comp (Y := (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X) (NatTrans.app (ε F) X)
      (NatTrans.app (η F) X ≫ f ≫ NatTrans.app (F.map (Iso.inv (ρ_ m))) Y) ≫
    NatTrans.app (δ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y
Tactic: rw [← cancel_epi ((ε F).app _), ← cancel_mono ((δ F _ _).app _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
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₁ m₂ : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category) (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) (F.obj m₂)).obj
        ((F.obj m₁).obj X) ⟶
      (tensorObj (𝒞 := Functor.category)
            (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))) (F.obj m₂)).obj
        X)
    (NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂)) X ≫
        NatTrans.app (F.map (Iso.inv (α_ m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂))) X ≫
          NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) m₂) X)
    (NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (F.map (Iso.hom (λ_ m₂))) ((F.obj m₁).obj X) ≫
        (F.obj m₂).map (NatTrans.app (F.map (Iso.inv (ρ_ m₁))) X))
have rw : Eq (α :=
  (tensorObj (𝒞 := Functor.category) (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) (F.obj m₂)).obj
      ((F.obj m₁).obj X) ⟶
    (tensorObj (𝒞 := Functor.category)
          (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))) (F.obj m₂)).obj
      X)
  (NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂) ((F.obj m₁).obj X) ≫
    NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂)) X ≫
      NatTrans.app (F.map (Iso.inv (α_ m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂))) X ≫
        NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) m₂) X)
  ((F.obj m₂).map (NatTrans.app (η F) ((F.obj m₁).obj X) ≫ NatTrans.app (F.map (Iso.inv (ρ_ m₁))) X))
Tactic: rw [← obj_η_app_assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
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
⊢ (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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
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
⊢ (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)
have 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)
Tactic: simp only [μ_naturalityᵣ_assoc, μ_naturalityₗ_assoc, η_app_obj, Category.assoc,
      obj_μ_inv_app, Functor.map_comp, δ_μ_app_assoc, obj_ε_app,
      unitOfTensorIsoUnit_inv_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (goal)
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)
⊢ (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).IsPointwiseLeftKanExtensionAt (d, e)
have apply : Limits.IsColimit
  (Limits.Cocone.whisker equiv.functor ((Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)))
Tactic: apply Limits.IsColimit.ofWhiskerEquivalence equiv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (goal)
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))) :=
  ⋯
⊢ I.Final
have 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))))
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))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (goal)
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 := ⋯
⊢ Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)))
have apply : Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
Tactic: apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone) |>.toFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (goal)
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 (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
have 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))
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (goal)
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)
⊢ (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).IsPointwiseLeftKanExtensionAt (e, d)
have apply : Limits.IsColimit
  (Limits.Cocone.whisker equiv.functor
    ((Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)))
Tactic: apply Limits.IsColimit.ofWhiskerEquivalence equiv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (goal)
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)
I : CostructuredArrow L d ⥤ CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d :=
  Equivalence.inverse (prod.leftUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
      (𝟭 (CostructuredArrow L d))
this : Functor.Final (D := CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e)
  (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))) :=
  ⋯
⊢ I.Final
have apply : Functor.Final (C := Discrete PUnit.{1} × CostructuredArrow L d) (D :=
  CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d)
  (Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))) (𝟭 (CostructuredArrow L d)))
Tactic: apply Iff.mp <| Functor.final_iff_final_comp
      (F := (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse)
      (G := Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.prod <| 𝟭 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (goal)
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)
I : CostructuredArrow L d ⥤ CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d :=
  Equivalence.inverse (prod.leftUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
      (𝟭 (CostructuredArrow L d))
this : I.Final := ⋯
⊢ Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)))
have apply : Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
Tactic: apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone) |>.toFun