awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ▷ F.obj A ≫
        Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))
have simp_rw : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
    F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.obj A))
        (F.map Δ ▷ F.obj A) (δ F A A ▷ F.obj A) ≫
      Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))
Tactic: simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc,
      MonoidalCategory.whiskerLeft_comp, δ_natural_right_assoc,
      ← F.map_comp_assoc, comul_assoc, F.map_comp, Category.assoc, associativity]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
simp_rw :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.obj A))
          (F.map Δ ▷ F.obj A) (δ F A A ▷ F.obj A) ≫
        Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ▷ F.obj A ≫
        Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))
have simp_rw₁ : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (δ F A A ≫ F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (δ F A A ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.obj A))
        (F.map Δ ▷ F.obj A) (δ F A A ▷ F.obj A ≫ Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))))
Tactic: simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc,
      MonoidalCategory.whiskerLeft_comp, δ_natural_right_assoc,
      ← F.map_comp_assoc, comul_assoc, F.map_comp, Category.assoc, associativity]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
simp_rw :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.obj A))
          (F.map Δ ▷ F.obj A) (δ F A A ▷ F.obj A) ≫
        Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))
simp_rw₁ :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
      (δ F A A ≫ F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
      (δ F A A ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.obj A)) (F.map Δ ▷ F.obj A)
          (δ F A A ▷ F.obj A ≫ Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))))
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ▷ F.obj A ≫
        Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))
have simp_rw₂ : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj A)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (δ F A A ≫ F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
      (F.map (Δ ▷ A))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ δ F A A ▷ F.obj A ≫ Iso.hom (α_ (F.obj A) (F.obj A) (F.obj A)))))
Tactic: simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc,
      MonoidalCategory.whiskerLeft_comp, δ_natural_right_assoc,
      ← F.map_comp_assoc, comul_assoc, F.map_comp, Category.assoc, associativity]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.OplaxMonoidal
A : Comon.{v₁, u₁} C
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom (V := Comon.{v₂, u₂} D) { X := F.obj A.X, comon := obj.instComonObj A.X F }
      { X := F.obj A.X, comon := obj.instComonObj A.X F })
    { hom := F.map (Comon.Hom.hom (𝟙 A)), isComonHom_hom := ⋯ } (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F })
have w : Eq.{v₂ + 1} (α :=
  Comon.X.{v₂, u₂} { X := F.obj A.X, comon := obj.instComonObj A.X F : Comon.{v₂, u₂} D } ⟶
    Comon.X.{v₂, u₂} { X := F.obj A.X, comon := obj.instComonObj A.X F })
  (Comon.Hom.hom { hom := F.map (Comon.Hom.hom (𝟙 A)), isComonHom_hom := sorry })
  (Comon.Hom.hom (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.OplaxMonoidal
X Y Z : Comon.{v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom (V := Comon.{v₂, u₂} D) { X := F.obj X.X, comon := obj.instComonObj X.X F }
      { X := F.obj Z.X, comon := obj.instComonObj Z.X F })
    { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ }
    (CategoryStruct.comp (Y := { X := F.obj Y.X, comon := obj.instComonObj Y.X F })
      { hom := F.map f.hom, isComonHom_hom := ⋯ } { hom := F.map g.hom, isComonHom_hom := ⋯ })
have w : Eq.{v₂ + 1} (α :=
  Comon.X.{v₂, u₂} { X := F.obj X.X, comon := obj.instComonObj X.X F : Comon.{v₂, u₂} D } ⟶
    Comon.X.{v₂, u₂} { X := F.obj Z.X, comon := obj.instComonObj Z.X F })
  (Comon.Hom.hom { hom := F.map (f ≫ g).hom, isComonHom_hom := sorry })
  (Comon.Hom.hom
    (CategoryStruct.comp (Y := { X := F.obj Y.X, comon := obj.instComonObj Y.X F })
      { hom := F.map f.hom, isComonHom_hom := sorry } { hom := F.map g.hom, isComonHom_hom := sorry }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Conv (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
⊢ f * g * h = f * (g * h)
have simp : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (f ▷ M ≫ N ◁ g ≫ μ) ▷ M ≫ N ◁ h ≫ μ) =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
    (f ▷ M ≫ N ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (g ▷ M ≫ N ◁ h ≫ μ) ≫ μ)
Tactic: simp only [mul_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Conv (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (f ▷ M ≫ N ◁ g ≫ μ) ▷ M ≫ N ◁ h ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫ N ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (g ▷ M ≫ N ◁ h ≫ μ) ≫ μ)
have simp : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
    (Δ ▷ M ≫ f ▷ M ▷ M ≫ Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ μ ▷ M ≫ N ◁ h ≫ μ) =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
    (f ▷ M ≫
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (N ◁ Δ)
        (N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ))
Tactic: simp only [comp_whiskerRight, whisker_assoc, Category.assoc,
      MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Conv (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
| μ ▷ M ≫ N ◁ h
have a : tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Conv (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (Δ ▷ M ≫ f ▷ M ▷ M ≫ Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ μ ▷ M ≫ N ◁ h ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (N ◁ Δ)
          (N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ))
have slice_lhs : Δ ≫
    Δ ▷ M ≫
      f ▷ M ▷ M ≫
        Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ (tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N) ≫ μ =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
    (f ▷ M ≫
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (N ◁ Δ)
        (N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ))
Tactic: slice_lhs 7 8 =>
      rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Conv (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
| f ▷ M ≫ N ◁ Δ
have a : M ◁ Δ ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Conv (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
⊢ Δ ≫
      Δ ▷ M ≫
        f ▷ M ▷ M ≫
          Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ (tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N) ≫ μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (N ◁ Δ)
          (N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ))
have slice_rhs : Δ ≫
    Δ ▷ M ≫
      f ▷ M ▷ M ≫
        Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ (tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N) ≫ μ =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) N N))
        (((M ◁ Δ ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ N ◁ g ▷ M) ≫ N ◁ N ◁ h) (N ◁ μ) ≫
      μ)
Tactic: slice_rhs 2 3 =>
      rw [← whisker_exchange]
-- 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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).obj (x, y))
      (NatTrans.app (unit F G) (x, y)) (NatTrans.app (Iso.hom (braiding F G)) (tensorObj.{v₁, u₁} (𝒞 := inst) x y)) =
    Iso.hom (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)) ≫
      NatTrans.app (unit G F) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 G F _).map (Iso.hom (β_ (y, x).1 (y, x).2))
have F₁ : CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).obj (x, y))
    (NatTrans.app (unit F G) (x, y))
    (NatTrans.app (Iso.hom (braiding F G)) (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (x, y))) =
  Iso.hom (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)) ≫
    NatTrans.app (unit G F) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 G F _).map (Iso.hom (β_ (y, x).1 (y, x).2))
Tactic: change
    (unit F G).app (x, y) ≫ (braiding F G).hom.app ((tensor C).obj (x, y)) = _
-- 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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G F _).obj (x, y))
      (NatTrans.app (unit G F) (x, y)) (NatTrans.app (Iso.inv (braiding F G)) (tensorObj.{v₁, u₁} (𝒞 := inst) x y)) =
    Iso.inv (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)) ≫
      NatTrans.app (unit F G) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 F G _).map (Iso.inv (β_ (y, x).2 (y, x).1))
have G₁ : CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G F _).obj (x, y))
    (NatTrans.app (unit G F) (x, y))
    (NatTrans.app (Iso.inv (braiding F G)) (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (x, y))) =
  Iso.inv (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)) ≫
    NatTrans.app (unit F G) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 F G _).map (Iso.inv (β_ (y, x).2 (y, x).1))
Tactic: change
    (unit G F).app (x, y) ≫ (braiding F G).inv.app ((tensor C).obj (x, y)) = _
-- 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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
⊢ Eq (α := @convolution _ _ _ _ inst_2 inst_4 H F _ ⟶ @convolution _ _ _ _ inst_2 inst_4 G H _)
    (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η) (Iso.hom (braiding H G)))
    (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F)) (map η (𝟙 H)))
have hγ : Eq (α := H ⊠ F ⟶ tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G H _)
  (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
    (Functor.whiskerLeft (tensor C)
      (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η) (Iso.hom (braiding H G)))))
  (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
    (Functor.whiskerLeft (tensor C)
      (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F)) (map η (𝟙 H)))))
Tactic: apply Functor.hom_ext_of_isLeftKanExtension (H ⊛ F) (unit H F)
-- 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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
⊢ Eq (α := H ⊠ F ⟶ tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G H _)
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η) (Iso.hom (braiding H G)))))
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F)) (map η (𝟙 H)))))
have hγ : ∀ (fst snd : C),
  Eq (α := (H ⊠ F).obj (fst, snd) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G H _).obj (fst, snd))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η) (Iso.hom (braiding H G)))))
      (fst, snd))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F)) (map η (𝟙 H)))))
      (fst, snd))
Tactic: ext ⟨_, _⟩
-- 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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
⊢ Eq (α := @convolution _ _ _ _ inst_2 inst_4 F H _ ⟶ @convolution _ _ _ _ inst_2 inst_4 H G _)
    (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H)) (Iso.hom (braiding G H)))
    (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H)) (map (𝟙 H) η))
have hγ : Eq (α := F ⊠ H ⟶ tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H G _)
  (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
    (Functor.whiskerLeft (tensor C)
      (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H)) (Iso.hom (braiding G H)))))
  (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
    (Functor.whiskerLeft (tensor C)
      (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H)) (map (𝟙 H) η))))
Tactic: apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ H) (unit F H)
-- 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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
⊢ Eq (α := F ⊠ H ⟶ tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H G _)
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H)) (Iso.hom (braiding G H)))))
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H)) (map (𝟙 H) η))))
have hγ : ∀ (fst snd : C),
  Eq (α := (F ⊠ H).obj (fst, snd) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H G _).obj (fst, snd))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H)) (Iso.hom (braiding G H)))))
      (fst, snd))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H)) (map (𝟙 H) η))))
      (fst, snd))
Tactic: ext ⟨_, _⟩