awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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)
  (ε K) (ε 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 β
X Y : C
⊢ Eq (α :=
    tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y) ⟶
      (G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y)
have h₁ : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y)).1 ⟶
    ((G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1)
  (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1
  (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).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 β
X Y : C
h₁ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y)).1 ⟶
      ((G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1)
    (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1
    (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).1
⊢ Eq (α :=
    tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y) ⟶
      (G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y)
have h₂ : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y)).2 ⟶
    ((G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2)
  (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2
  (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₂ ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F₁)
have rw : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  ((LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (LaxMonoidal.ε F₁)
Tactic: rw [← NatTrans.IsMonoidal.unit (τ := e.hom), assoc, hom_inv_id_app, comp_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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
rw :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁)
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₂ ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F₁)
have rw₁ : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (LaxMonoidal.ε F₁)
Tactic: rw [← NatTrans.IsMonoidal.unit (τ := e.hom), assoc, hom_inv_id_app, comp_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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
rw :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁)
rw₁ :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁)
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₂ ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F₁)
have rw₂ : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (LaxMonoidal.ε F₁ ≫ 𝟙 (F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (LaxMonoidal.ε F₁)
Tactic: rw [← NatTrans.IsMonoidal.unit (τ := e.hom), assoc, hom_inv_id_app, comp_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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
rw :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁)
rw₁ :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁)
rw₂ :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁ ≫ 𝟙 (F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (LaxMonoidal.ε F₁)
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₂ ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F₁)
have rw₃ : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F₁)
  (LaxMonoidal.ε F₁)
Tactic: rw [← NatTrans.IsMonoidal.unit (τ := e.hom), assoc, hom_inv_id_app, comp_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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₁.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y)
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  ((LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
    e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
Tactic: rw [← cancel_mono (e.hom.app (X ⊗ Y)), assoc, assoc, inv_hom_id_app, comp_id,
      NatTrans.IsMonoidal.tensor, MonoidalCategory.tensorHom_comp_tensorHom_assoc,
      inv_hom_id_app, inv_hom_id_app, tensorHom_id, id_whiskerRight, id_comp]
-- 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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
X Y : C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₁.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y)
have rw₁ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (LaxMonoidal.μ F₂ X Y ≫
    e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
Tactic: rw [← cancel_mono (e.hom.app (X ⊗ Y)), assoc, assoc, inv_hom_id_app, comp_id,
      NatTrans.IsMonoidal.tensor, MonoidalCategory.tensorHom_comp_tensorHom_assoc,
      inv_hom_id_app, inv_hom_id_app, tensorHom_id, id_whiskerRight, id_comp]
-- 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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
X Y : C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₁ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫
      e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₁.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y)
have rw₂ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (LaxMonoidal.μ F₂ X Y ≫
    e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
Tactic: rw [← cancel_mono (e.hom.app (X ⊗ Y)), assoc, assoc, inv_hom_id_app, comp_id,
      NatTrans.IsMonoidal.tensor, MonoidalCategory.tensorHom_comp_tensorHom_assoc,
      inv_hom_id_app, inv_hom_id_app, tensorHom_id, id_whiskerRight, id_comp]
-- 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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
X Y : C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₁ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫
      e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₂ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫
      e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₁.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y)
have rw₃ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (LaxMonoidal.μ F₂ X Y ≫ 𝟙 (F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
  ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
Tactic: rw [← cancel_mono (e.hom.app (X ⊗ Y)), assoc, assoc, inv_hom_id_app, comp_id,
      NatTrans.IsMonoidal.tensor, MonoidalCategory.tensorHom_comp_tensorHom_assoc,
      inv_hom_id_app, inv_hom_id_app, tensorHom_id, id_whiskerRight, id_comp]
-- 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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
X Y : C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₁ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫
      e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₂ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫
      e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₃ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫ 𝟙 (F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₁.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y)
have rw₄ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (LaxMonoidal.μ F₂ X Y)
  ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
Tactic: rw [← cancel_mono (e.hom.app (X ⊗ Y)), assoc, assoc, inv_hom_id_app, comp_id,
      NatTrans.IsMonoidal.tensor, MonoidalCategory.tensorHom_comp_tensorHom_assoc,
      inv_hom_id_app, inv_hom_id_app, tensorHom_id, id_whiskerRight, id_comp]