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
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))
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))
⊢ 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) ≫ (e.hom.app X ⊗ₘ e.hom.app Y) ≫ LaxMonoidal.μ F₂ 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))
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))
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) ≫ (e.hom.app X ⊗ₘ e.hom.app Y) ≫ LaxMonoidal.μ F₂ 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.hom.app X ⊗ₘ e.inv.app Y ≫ e.hom.app Y) ≫ LaxMonoidal.μ F₂ 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (F ⋙ G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (𝟭 C) ≫ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F ⋙ G))
have dsimp : 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
  CategoryStruct.comp (Y := G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G) (G.map (ε F))
Tactic: dsimp
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
⊢ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    CategoryStruct.comp (Y := G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G) (G.map (ε F))
have rw : adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
  adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ 𝟙 (G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: rw [id_comp, ← unit_app_unit_comp_map_η adj, assoc, Monoidal.map_η_ε]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
⊢ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ 𝟙 (G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have rw : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
  (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: rw [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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) (obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) ⟶
      (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (𝟭 C) X Y ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ (F ⋙ G) X Y)
have dsimp : 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
  (adj.unit.app X ⊗ₘ adj.unit.app 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))
Tactic: dsimp
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : C
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    (adj.unit.app X ⊗ₘ adj.unit.app 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))
have rw : 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
  adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
      (G.map (μ F X Y))
Tactic: rw [← unit_app_tensor_comp_map_δ_assoc, id_comp, Monoidal.map_δ_μ, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : C
rw :
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
        (G.map (μ F X Y))
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    (adj.unit.app X ⊗ₘ adj.unit.app 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))
have rw₁ : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
      (G.map (μ F X Y)))
Tactic: rw [← unit_app_tensor_comp_map_δ_assoc, id_comp, Monoidal.map_δ_μ, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : C
rw :
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
        (G.map (μ F X Y))
rw₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
        (G.map (μ F X Y)))
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    (adj.unit.app X ⊗ₘ adj.unit.app 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))
have rw₂ : adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
  adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ 𝟙 (G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
Tactic: rw [← unit_app_tensor_comp_map_δ_assoc, id_comp, Monoidal.map_δ_μ, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : C
rw :
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
        (G.map (μ F X Y))
rw₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
        (G.map (μ F X Y)))
rw₂ :
  adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ 𝟙 (G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    (adj.unit.app X ⊗ₘ adj.unit.app 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))
have rw₃ : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
Tactic: rw [← unit_app_tensor_comp_map_δ_assoc, id_comp, Monoidal.map_δ_μ, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (ε (G ⋙ F) ≫ adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε (𝟭 D))
have dsimp : CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (F.map (ε G)) ≫
    adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) =
  𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
Tactic: dsimp
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
⊢ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (F.map (ε G)) ≫
      adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
have rw : CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F)
    (F.map (ε G) ≫ adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
  𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
Tactic: rw [assoc, map_ε_comp_counit_app_unit adj, ε_η]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
rw :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F)
      (F.map (ε G) ≫ adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
⊢ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (F.map (ε G)) ≫
      adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
have rw₁ : CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) =
  𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
Tactic: rw [assoc, map_ε_comp_counit_app_unit adj, ε_η]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
rw :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F)
      (F.map (ε G) ≫ adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
rw₁ :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
⊢ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (F.map (ε G)) ≫
      adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
have rw₂ : Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
  (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
Tactic: rw [assoc, map_ε_comp_counit_app_unit adj, ε_η]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : D
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) ((G ⋙ F).obj X) ((G ⋙ F).obj Y) ⟶
      obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (μ (G ⋙ F) X Y ≫ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    ((adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ μ (𝟭 D) X Y)
have dsimp : CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
      (F.map (μ G X Y)) ≫
    adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) =
  (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
Tactic: dsimp