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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y')
    (F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y'))
    ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
    G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
    G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))
Tactic: rw [this]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))
have suffices : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y')
  (F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y'))
  ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)
Tactic: suffices F.obj (G.obj X) ◁ F.map (G.map g) ≫ _ =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
      F.map (G.map (δ F (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
        F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ G.obj Z) ≫
          δ F (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (G.obj Z) ≫
            (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) ⊗ₘ adj.counit.app Z) ≫ Iso.hom (α_ X Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
have rw : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
  (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z) ≫
    F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
      F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
          (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) ⊗ₘ adj.counit.app Z) ≫ Iso.hom (α_ X Y Z))
  (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
    F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
          δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
            (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
Tactic: rw [← δ_natural_left_assoc, ← δ_natural_left_assoc, ← δ_natural_left_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (hypothesis)
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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z) ≫
      F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) ⊗ₘ adj.counit.app Z) ≫ Iso.hom (α_ X Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
have this : ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D}
  (h : tensorObj.{v₂, u₂} (𝒞 := inst_2) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X') ⟶ Z),
  (G ⋙ F).map f ▷ (G ⋙ F).obj X' ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ map (𝟭 D) f ▷ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X' ≫ h
Tactic: haveI := @NatTrans.whiskerRight_app_tensor_app_assoc _ _ _ _ _ _ _ _ _ adj.counit adj.counit
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z) ≫
      F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) ⊗ₘ adj.counit.app Z) ≫ Iso.hom (α_ X Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
have rw : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
  (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
    δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
      F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z))
  (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
    F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
          δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
            (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
Tactic: rw [this, this, tensorHom_def, assoc, ← comp_whiskerRight_assoc,
      left_triangle_components, id_whiskerRight, id_comp,
      whisker_exchange_assoc, whisker_exchange_assoc, ← tensorHom_def_assoc,
      associator_naturality, OplaxMonoidal.associativity_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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
have rw : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
  (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
    δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
      F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z))
  (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
    δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
      F.obj (G.obj X) ◁ F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
Tactic: rw [← δ_natural_right_assoc, ← δ_natural_right_assoc, ← δ_natural_right_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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
        F.obj (G.obj X) ◁ F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
          F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
            F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
have nth_rw : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
  (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
    δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
      F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z))
  (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
    δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
      F.obj (G.obj X) ◁ F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            adj.counit.app X ▷ F.obj (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              X ◁ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
Tactic: nth_rw 4 [tensorHom_def]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
⊢ adj.IsMonoidal
have leftAdjoint_ε : autoParam
  (Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G)
    (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ G.map (η F)))
  IsMonoidal.leftAdjoint_ε._autoParam
Tactic: constructor
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
leftAdjoint_ε :
  autoParam
    (Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G)
      (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ G.map (η F)))
    IsMonoidal.leftAdjoint_ε._autoParam
⊢ adj.IsMonoidal
have leftAdjoint_μ : autoParam
  (∀ (X Y : D),
    Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
      (μ G X Y)
      (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ≫
        G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y))))
  IsMonoidal.leftAdjoint_μ._autoParam
Tactic: constructor
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
inst_8 : G.LaxMonoidal
inst_9 : adj.IsMonoidal
F' : Functor.{v₂, v₃, u₂, u₃} D E
G' : Functor.{v₃, v₂, u₃, u₂} E D
adj' : F' ⊣ G'
inst_10 : F'.OplaxMonoidal
inst_11 : G'.LaxMonoidal
inst_12 : adj'.IsMonoidal
X Y : E
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) ((G' ⋙ G).obj X) ((G' ⋙ G).obj Y) ⟶
      (G' ⋙ G).obj (tensorObj.{v₃, u₃} (𝒞 := inst_4) X Y))
    (μ (G' ⋙ G) X Y)
    ((adj.comp adj').unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) ((G' ⋙ G).obj X) ((G' ⋙ G).obj Y)) ≫
      (G' ⋙ G).map
        (δ (F ⋙ F') ((G' ⋙ G).obj X) ((G' ⋙ G).obj Y) ≫ ((adj.comp adj').counit.app X ⊗ₘ (adj.comp adj').counit.app Y)))
have simp : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y)) ⟶
    G.obj (G'.obj (tensorObj.{v₃, u₃} (𝒞 := inst_4) X Y)))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y))) ≫
    G.map
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj (G'.obj X))) (F.obj (G.obj (G'.obj Y))))
        (δ F (G.obj (G'.obj X)) (G.obj (G'.obj Y)))
        ((adj.counit.app (G'.obj X) ⊗ₘ adj.counit.app (G'.obj Y)) ≫
          adj'.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G'.obj X) (G'.obj Y)) ≫
            G'.map (δ F' (G'.obj X) (G'.obj Y) ≫ (adj'.counit.app X ⊗ₘ adj'.counit.app Y)))))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y))) ≫
    G.map
      (adj'.unit.app (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y)))) ≫
        G'.map
          (CategoryStruct.comp (Y :=
            F'.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj (G'.obj X))) (F.obj (G.obj (G'.obj Y)))))
            (F'.map (δ F (G.obj (G'.obj X)) (G.obj (G'.obj Y))))
            (F'.map (adj.counit.app (G'.obj X) ⊗ₘ adj.counit.app (G'.obj Y)) ≫
              δ F' (G'.obj X) (G'.obj Y) ≫ (adj'.counit.app X ⊗ₘ adj'.counit.app Y)))))
Tactic: simp only [comp_obj, comp_μ, IsMonoidal.leftAdjoint_μ (adj := adj), id_obj,
      IsMonoidal.leftAdjoint_μ (adj := adj'), assoc, ← map_comp, comp_unit_app, comp_δ,
      comp_counit_app, ← tensorHom_comp_tensorHom, δ_natural_assoc, Functor.comp_map]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ adj.unit.app Z) ≫
    CategoryStruct.comp (Y :=
      G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)))
      (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (G.map
        (((Equiv.symm
                    (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
                      (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) :
                  Equiv.{v₁ + 1, v₂ + 1}
                    (tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
                    (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
                      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) :
                (a : X ⊗ Y ⟶ G.obj (F.obj X ⊗ F.obj Y)) → F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y)
              ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z))))
have rw : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
  adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ (F ⋙ G).obj Z ≫
    (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
          G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫
            G.map (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))) ▷
        G.obj (F.obj Z) ≫
      μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ≫
        G.map (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
Tactic: rw [homEquiv_counit, map_comp_assoc, map_comp,
        ← μ_natural_left_assoc, map_comp, map_comp, tensorHom_def'_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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : G.LaxMonoidal
X Y Z : C
| tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ (F ⋙ G).obj Z ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫
              G.map (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))) ▷
          G.obj (F.obj Z) ≫
        μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ≫
          G.map (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
have dsimp : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
  adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj (F.obj Z) ≫
    (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
          G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫
            G.map (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))) ▷
        G.obj (F.obj Z) ≫
      μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ≫
        G.map (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
Tactic: dsimp