awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : SymmetricCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : SymmetricCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
⊢ CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
      (Iso.hom (braiding G F)) =
    𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _)
have hγ : CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _) (unit F G)
    (Functor.whiskerLeft (tensor C)
      (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
        (Iso.hom (braiding G F)))) =
  unit F G ≫ Functor.whiskerLeft (tensor C) (𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _))
Tactic: apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G) (unit F G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : SymmetricCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : SymmetricCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
⊢ CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _) (unit F G)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
          (Iso.hom (braiding G F)))) =
    unit F G ≫ Functor.whiskerLeft (tensor C) (𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _))
have hγ : ∀ (x y : C),
  Eq (α := (F ⊠ G).obj (x, y) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).obj (x, y))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _) (unit F G)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
            (Iso.hom (braiding G F)))))
      (x, y))
    ((unit F G ≫ Functor.whiskerLeft (tensor C) (𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _))).app (x, y))
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
⊢ Eq (α := H.obj c ⟶ ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).obj j')
    ((fun (j : C) ↦ ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)) j)
        j ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).map φ)
    ((fun (j : C) ↦ ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)) j)
        j' ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op).app j')
have this : Eq.{v₂ + 1} (α :=
  ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j')).obj j' ⟶
    ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).obj j')
  ((fun
        (t :
          (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j') ⟶
            (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)) ↦
      t.app j')
    ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).map φ.op ≫
      (((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)))
  ((fun
        (t :
          (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j') ⟶
            (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)) ↦
      t.app j')
    ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j') ≫
      (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op))
Tactic: have := congrArg (fun t ↦ t.app j') <|
        dayConvolutionInternalHomDiagramFunctor
          F |>.map f |>.app c |>.naturality φ.op
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  Eq.{v₂ + 1} (α :=
    ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j')).obj j' ⟶
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).obj j')
    ((fun
          (t :
            (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j') ⟶
              (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)) ↦
        t.app j')
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).map φ.op ≫
        (((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)))
    ((fun
          (t :
            (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j') ⟶
              (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)) ↦
        t.app j')
      ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j') ≫
        (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op))
⊢ Eq (α := H.obj c ⟶ ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).obj j')
    ((fun (j : C) ↦ ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)) j)
        j ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).map φ)
    ((fun (j : C) ↦ ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)) j)
        j' ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op).app j')
have dsimp : (ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ≫
    Functor.map (ihom (F.obj j)) (G'.map (φ ▷ c)) =
  (ℌ.π c j' ≫ Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))) ≫
    NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  Eq (α :=
    Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j')) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    (NatTrans.app (MonoidalClosed.pre (F.map φ)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
      Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    (Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
⊢ (ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ≫
      Functor.map (ihom (F.obj j)) (G'.map (φ ▷ c)) =
    (ℌ.π c j' ≫ Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))) ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))
have rw : Eq (α := H.obj c ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
  (ℌ.π c j' ≫
    NatTrans.app (MonoidalClosed.pre (F.map φ)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
      Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
  ((ℌ.π c j' ≫ Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))) ≫
    NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
Tactic: rw [Category.assoc, ← (ihom (F.obj j)).map_comp, ← f.naturality,
        Functor.map_comp, reassoc_of% ℌ.hπ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
        (fun (j : C) ↦
          ℌ.π c' j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c').app (op j)) j)
        ⋯ =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦
          ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c).app (op j)) j)
        ⋯ ≫
      H'.map f
have apply : ∀ (j : (multicospanShapeEnd.{v₁, u₁} C).L),
  (H.map f ≫
        Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦
            ℌ.π c' j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c').app (op j)) j)
          sorry) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') sorry) j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
          (fun (j : C) ↦
            ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c).app (op j)) j)
          sorry ≫
        H'.map f) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') sorry) j
Tactic: apply Wedge.IsLimit.hom_ext (ℌ'.isLimitWedge c')
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd.{v₁, u₁} C).L
⊢ (H.map f ≫
        Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦
            ℌ.π c' j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c').app (op j)) j)
          ⋯) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
          (fun (j : C) ↦
            ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c).app (op j)) j)
          ⋯ ≫
        H'.map f) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j
have dsimp : (H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
        (fun (j : C) ↦ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c'))) sorry) ≫
    ℌ'.π c' j =
  (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) sorry ≫
      H'.map f) ≫
    ℌ'.π c' j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd.{v₁, u₁} C).L
⊢ (H.map f ≫
        Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c'))) ⋯) ≫
      ℌ'.π c' j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
          (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
        H'.map f) ≫
      ℌ'.π c' j
have simp : H.map f ≫
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
        (fun (j : C) ↦ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c'))) sorry ≫
      ℌ'.π c' j =
  Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
      (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) sorry ≫
    ℌ'.π c j ≫ Functor.map (ihom (F.obj j)) (G'.map (j ◁ f))
Tactic: simp only [Category.assoc, map_comp_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd.{v₁, u₁} C).L
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c'))) ⋯ ≫
        ℌ'.π c' j =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      ℌ'.π c j ≫ Functor.map (ihom (F.obj j)) (G'.map (j ◁ f))
have rw : H.map f ≫ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c')) =
  (ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ≫
    Functor.map (ihom (F.obj j)) (G'.map (j ◁ f))
Tactic: rw [← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c')
        (H'.obj c') (ℌ'.π c') (ℌ'.hπ c'),
      ← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
        (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
      Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c'),
      Wedge.IsLimit.lift_ι_assoc (ℌ'.isLimitWedge c)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j : C
⊢ (ℌ.map f ℌ').app c ≫ ℌ'.π c j = ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
have dsimp : Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
      (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) sorry ≫
    ℌ'.π c j =
  ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j : C
⊢ Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      ℌ'.π c j =
    ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
have rw : Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
      (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) sorry ≫
    Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) sorry) j =
  ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
Tactic: rw [← Wedge.mk_ι
      (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
      (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
    Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j : C
rw :
  Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j =
    ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
⊢ Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      ℌ'.π c j =
    ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
have rw₁ : ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c)) =
  ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
Tactic: rw [← Wedge.mk_ι
      (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
      (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
    Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
⊢ (unop (op (F ⊠ H))).map f ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
    MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫
      (Functor.obj (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C)) G).map f
have this : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
      (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
  ((fun
        (t :
          H.obj x.2 ⟶
            Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))) ↦
      (F.obj x.1 ◁ t :
        tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
          tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
            (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))))
    (ℌ.π x.2 x.1 ≫ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2))))
  ((fun
        (t :
          H.obj x.2 ⟶
            Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))) ↦
      (F.obj x.1 ◁ t :
        tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
          tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
            (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))))
    (ℌ.π x.2 y.1 ≫ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
Tactic: have := congrArg (fun t ↦ F.obj x.1 ◁ t) <| ℌ.hπ x.2 f.1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    ((fun
          (t :
            H.obj x.2 ⟶
              Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))) ↦
        (F.obj x.1 ◁ t :
          tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
            tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
              (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))))
      (ℌ.π x.2 x.1 ≫ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2))))
    ((fun
          (t :
            H.obj x.2 ⟶
              Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))) ↦
        (F.obj x.1 ◁ t :
          tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
            tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
              (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))))
      (ℌ.π x.2 y.1 ≫ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
⊢ (unop (op (F ⊠ H))).map f ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
    MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫
      (Functor.obj (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C)) G).map f
have dsimp : (F.map f.1 ▷ H.obj x.2 ≫ F.obj y.1 ◁ H.map f.2) ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
  MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫ G.map (f.1 ⊗ₘ f.2)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    (F.obj x.1 ◁ (ℌ.π x.2 x.1 ≫ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2))))
    (F.obj x.1 ◁
      (ℌ.π x.2 y.1 ≫ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
⊢ (F.map f.1 ▷ H.obj x.2 ≫ F.obj y.1 ◁ H.map f.2) ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
    MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫ G.map (f.1 ⊗ₘ f.2)
have this₁ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
      (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
  (F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2)))
  (F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
    F.obj x.1 ◁ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))
Tactic: simp only [whiskerLeft_comp] at this
Cleared hypotheses: this