awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ◁ i.inv.app Z ≫
          LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
              LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
have e_a : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ◁ i.inv.app Z ≫
      LaxMonoidal.μ F X Y ▷ F.obj Z ≫
        LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))
  (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
    G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
      G.obj X ◁ LaxMonoidal.μ F Y Z ≫
        G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
          (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
            LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: rw [← whisker_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ◁ i.inv.app Z ≫
        LaxMonoidal.μ F X Y ▷ F.obj Z ≫
          LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
              LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
have e_a : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
    Iso.hom (α_ (F.obj X) (F.obj Y) (G.obj Z)) ≫
      F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫
        F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
  (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
    G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
      G.obj X ◁ LaxMonoidal.μ F Y Z ≫
        G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
          (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
            LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: simp only [tensor_whiskerLeft, Functor.LaxMonoidal.associativity, Category.assoc,
      Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      Iso.hom (α_ (F.obj X) (F.obj Y) (G.obj Z)) ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫
          F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
              LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
have e_a : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
    (i.inv.app X ⊗ₘ i.inv.app Y ⊗ₘ 𝟙 (G.obj Z)) ≫
      F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫
        F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
  (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
    G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
      G.obj X ◁ LaxMonoidal.μ F Y Z ≫
        G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
          (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
            LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: rw [← tensorHom_id, associator_naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (G.obj X) ⟶ G.obj X)
    (Iso.hom (λ_ (G.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (G.obj X))
      (Iso.hom (εIso F ≪≫ i.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ G.obj X)
      (Iso.hom
          ((i.symm.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ᵢ i.symm.app X) ≪≫
            μIso F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≪≫
              i.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)) ≫
        G.map (Iso.hom (λ_ X))))
have simp : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (G.obj X) ⟶ G.obj X)
  (Iso.hom (λ_ (G.obj X)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
    (LaxMonoidal.ε F ⊗ₘ i.inv.app X)
    (LaxMonoidal.μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫
      i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ G.map (Iso.hom (λ_ X))))
Tactic: simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Iso.hom_inv_id_app,
      Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (G.obj X) ⟶ G.obj X)
    (Iso.hom (λ_ (G.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (LaxMonoidal.ε F ⊗ₘ i.inv.app X)
      (LaxMonoidal.μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ G.map (Iso.hom (λ_ X))))
have rw : Iso.hom (λ_ (G.obj X)) =
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
    ((𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⊗ₘ i.inv.app X) ≫ (LaxMonoidal.ε F ⊗ₘ 𝟙 (F.obj X)))
    (LaxMonoidal.μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X)) ≫ i.hom.app X)
Tactic: rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶ G.obj X)
    (Iso.hom (ρ_ (G.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (G.obj X ◁ Iso.hom (εIso F ≪≫ i.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (Iso.hom
          ((i.symm.app X ⊗ᵢ i.symm.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≪≫
            μIso F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≪≫
              i.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        G.map (Iso.hom (ρ_ X))))
have simp : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶ G.obj X)
  (Iso.hom (ρ_ (G.obj X)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (i.inv.app X ⊗ₘ LaxMonoidal.ε F)
    (LaxMonoidal.μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ G.map (Iso.hom (ρ_ X))))
Tactic: simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← id_tensorHom, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Category.id_comp,
      Iso.hom_inv_id_app, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶ G.obj X)
    (Iso.hom (ρ_ (G.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (i.inv.app X ⊗ₘ LaxMonoidal.ε F)
      (LaxMonoidal.μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ G.map (Iso.hom (ρ_ X))))
have rw : Iso.hom (ρ_ (G.obj X)) =
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    ((i.inv.app X ⊗ₘ 𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≫ (𝟙 (F.obj X) ⊗ₘ LaxMonoidal.ε F))
    (LaxMonoidal.μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X)) ≫ i.hom.app X)
Tactic: rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (α.app Y ⊗ₘ β.app Y) = (α.app X ⊗ₘ β.app X) ≫ (tensorObj G G').map f
have dsimp : Eq (α :=
  MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
  ((F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    ((F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
have rw : Eq (α :=
  MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
  (F.map f ≫ α.app Y ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
Tactic: rw [tensorHom_comp_tensorHom, α.naturality, β.naturality, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (F.map f ≫ α.app Y ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    ((F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
have rw₁ : Eq (α :=
  MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
  (α.app X ≫ G.map f ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
Tactic: rw [tensorHom_comp_tensorHom, α.naturality, β.naturality, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (F.map f ≫ α.app Y ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
rw₁ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (α.app X ≫ G.map f ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    ((F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
have rw₂ : Eq (α :=
  MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
  (α.app X ≫ G.map f ⊗ₘ β.app X ≫ G'.map f) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
Tactic: rw [tensorHom_comp_tensorHom, α.naturality, β.naturality, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (F.map f ≫ α.app Y ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
rw₁ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (α.app X ≫ G.map f ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
rw₂ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (α.app X ≫ G.map f ⊗ₘ β.app X ≫ G'.map f) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    ((F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
have rw₃ : Eq (α :=
  MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
  ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
Tactic: rw [tensorHom_comp_tensorHom, α.naturality, β.naturality, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F_1 G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F_1 ⟶ G
β_1 : F' ⟶ G'
F : Functor.{v₁, v₂, u₁, u₂} C D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ F.obj Y ◁ β.app Y = F.obj X ◁ β.app X ≫ (tensorObj F G').map f
have simp : (tensorObj F F').map f ≫ (𝟙 (F.obj Y) ⊗ₘ β.app Y) = (𝟙 (F.obj X) ⊗ₘ β.app X) ≫ (tensorObj F G').map f
Tactic: simp only [← id_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F'_1 G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F'_1 ⟶ G'
F' : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ α.app Y ▷ F'.obj Y = α.app X ▷ F'.obj X ≫ (tensorObj G F').map f
have simp : (tensorObj F F').map f ≫ (α.app Y ⊗ₘ 𝟙 (F'.obj Y)) = (α.app X ⊗ₘ 𝟙 (F'.obj X)) ≫ (tensorObj G F').map f
Tactic: simp only [← tensorHom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X₁ Y₁ X₂ Y₂ : Functor.{v₁, v₂, u₁, u₂} C D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) X₁ X₂ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) Y₁ Y₂)
    (f ⊗ₘ g) (f ▷ X₂ ≫ Y₁ ◁ g)
have w : ∀ (x : C),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) X₁ X₂).obj x ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj x)
    (NatTrans.app (f ⊗ₘ g) x) (NatTrans.app (f ▷ X₂ ≫ Y₁ ◁ g) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G H K : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Iso.hom (α_ F G H) ▷ K ≫
      Iso.hom (α_ F (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H) K) ≫ F ◁ Iso.hom (α_ G H K) =
    Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H K) ≫
      Iso.hom (α_ F G (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H K))
have w : ∀ (X : C),
  NatTrans.app
      (Iso.hom (α_ F G H) ▷ K ≫
        Iso.hom (α_ F (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H) K) ≫ F ◁ Iso.hom (α_ G H K))
      X =
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H K) ≫
          Iso.hom (α_ F G (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H K))).app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G H K : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ NatTrans.app
      (Iso.hom (α_ F G H) ▷ K ≫
        Iso.hom (α_ F (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H) K) ≫ F ◁ Iso.hom (α_ G H K))
      X =
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H K) ≫
          Iso.hom (α_ F G (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H K))).app
      X
have w : Eq (α :=
  MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
      (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X))
      (K.obj X) ⟶
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X)
      (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
  (Iso.hom (α_ (F.obj X) (G.obj X) (H.obj X)) ▷ K.obj X ≫
    Iso.hom (α_ (F.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X) (H.obj X)) (K.obj X)) ≫
      F.obj X ◁ Iso.hom (α_ (G.obj X) (H.obj X) (K.obj X)))
  (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X) (K.obj X)) ≫
    Iso.hom (α_ (F.obj X) (G.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
Tactic: dsimp