awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : BraidedCategory.{v₁, u₁} C
rw : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) = Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have rw₁ : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    tensorUnit.{v₁, u₁} C (𝒞 := inst))
  (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: rw [braiding_leftUnitor, unitors_equal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Multifunctor (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalCategory.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
f : F₁ ⟶ F₂
x x_1 : C
x_2 : x ⟶ x_1
⊢ (curriedTensorPre F₁).map x_2 ≫ { app := fun (X₂ : C) ↦ f.app x_1 ⊗ₘ f.app X₂, naturality := ⋯ } =
    { app := fun (X₂ : C) ↦ f.app x ⊗ₘ f.app X₂, naturality := ⋯ :
        NatTrans ((curriedTensorPre F₁).obj x) ((curriedTensorPre F₂).obj x) } ≫
      (curriedTensorPre F₂).map x_2
have w : ∀ (x_3 : C),
  NatTrans.app ((curriedTensorPre F₁).map x_2 ≫ { app := fun (X₂ : C) ↦ f.app x_1 ⊗ₘ f.app X₂, naturality := sorry }) x_3 =
    NatTrans.app
      ({ app := fun (X₂ : C) ↦ f.app x ⊗ₘ f.app X₂, naturality := sorry :
          NatTrans ((curriedTensorPre F₁).obj x) ((curriedTensorPre F₂).obj x) } ≫
        (curriedTensorPre F₂).map x_2)
      x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ G₂ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst_13 : IsMonoidal τ
inst_14 : IsMonoidal τ'
X Y : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F₁ ⋙ G₁).obj X) ((F₁ ⋙ G₁).obj Y) ⟶
      (F₂ ⋙ G₂).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (F₁ ⋙ G₁) X Y ≫ (τ ◫ τ').app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((τ ◫ τ').app X ⊗ₘ (τ ◫ τ').app Y) ≫ μ (F₂ ⋙ G₂) X Y)
have simp : Eq (α :=
  tensorObj.{v₃, u₃} (𝒞 := inst_4) (G₁.obj (F₁.obj X)) (G₁.obj (F₁.obj Y)) ⟶
    G₂.obj (F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
  ((τ'.app (F₁.obj X) ⊗ₘ τ'.app (F₁.obj Y)) ≫
    CategoryStruct.comp (Y := G₂.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₁.obj X) (F₁.obj Y)))
      (μ G₂ (F₁.obj X) (F₁.obj Y)) (G₂.map (μ F₁ X Y) ≫ G₂.map (τ.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))))
  ((τ'.app (F₁.obj X) ⊗ₘ τ'.app (F₁.obj Y)) ≫
    CategoryStruct.comp (Y := G₂.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₁.obj X) (F₁.obj Y)))
      (μ G₂ (F₁.obj X) (F₁.obj Y)) (G₂.map (τ.app X ⊗ₘ τ.app Y) ≫ G₂.map (μ F₂ X Y)))
Tactic: simp only [comp_obj, comp_μ, hcomp_app, assoc, naturality_assoc,
      tensor_assoc, ← tensorHom_comp_tensorHom, μ_natural_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : IsMonoidal τ
⊢ IsMonoidal (Functor.whiskerRight τ G₁)
have rw : IsMonoidal (τ ◫ 𝟙 G₁)
Tactic: rw [← Functor.hcomp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ G₂ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst_13 : IsMonoidal τ'
⊢ IsMonoidal (F₁.whiskerLeft τ')
have rw : IsMonoidal (𝟙 F₁ ◫ τ')
Tactic: rw [← Functor.id_hcomp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ⟶ (G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (G.prod' K))
have h₁ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
  (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₁ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ⟶ (G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (G.prod' K))
have h₂ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
  (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 (ε (G.prod' K)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1
have h₁ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
  ((ε (F.prod' H)).1 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
Tactic: rw [prod_comp_fst, prod'_ε_fst, prod'_ε_fst, prod'_app_fst, IsMonoidal.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₁ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    ((ε (F.prod' H)).1 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1
have h₂ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
  (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
Tactic: rw [prod_comp_fst, prod'_ε_fst, prod'_ε_fst, prod'_app_fst, IsMonoidal.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₁ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    ((ε (F.prod' H)).1 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1
have h₃ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
  (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε G)
Tactic: rw [prod_comp_fst, prod'_ε_fst, prod'_ε_fst, prod'_app_fst, IsMonoidal.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₁ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    ((ε (F.prod' H)).1 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
h₃ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε G)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1
have h₄ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
  (ε F ≫ α.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε G)
Tactic: rw [prod_comp_fst, prod'_ε_fst, prod'_ε_fst, prod'_app_fst, IsMonoidal.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₁ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    ((ε (F.prod' H)).1 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
h₃ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε G)
h₄ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ α.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε G)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1
have h₅ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
  (ε G) (ε G)
Tactic: rw [prod_comp_fst, prod'_ε_fst, prod'_ε_fst, prod'_app_fst, IsMonoidal.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 (ε (G.prod' K)).2
have h₂ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
  ((ε (F.prod' H)).2 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
Tactic: rw [prod_comp_snd, prod'_ε_snd, prod'_ε_snd, prod'_app_snd, IsMonoidal.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    ((ε (F.prod' H)).2 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 (ε (G.prod' K)).2
have h₃ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
  (ε H ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
Tactic: rw [prod_comp_snd, prod'_ε_snd, prod'_ε_snd, prod'_app_snd, IsMonoidal.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    ((ε (F.prod' H)).2 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
h₃ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε H ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 (ε (G.prod' K)).2
have h₄ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
  (ε H ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε K)
Tactic: rw [prod_comp_snd, prod'_ε_snd, prod'_ε_snd, prod'_app_snd, IsMonoidal.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    ((ε (F.prod' H)).2 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
h₃ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε H ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
h₄ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε H ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε K)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 (ε (G.prod' K)).2
have h₅ : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
    ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
  (ε H ≫ β.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε K)
Tactic: rw [prod_comp_snd, prod'_ε_snd, prod'_ε_snd, prod'_app_snd, IsMonoidal.unit]