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 : 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) ▷ 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)))
have rw : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
        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 [← comp_whiskerRight_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
| (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) ≫
        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]
      dsimp
      rw [← comp_whiskerRight_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
| Iso.hom (α_ X Y Z) ≫
    (adj.unit.app X ⊗ₘ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
      μ G (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
        G.map
          (F.obj X ◁
            ((Equiv.symm
                    (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
                      (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) :
                  Equiv.{v₁ + 1, v₂ + 1}
                    (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
                    (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ⟶
                      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) :
                (a : Y ⊗ Z ⟶ G.obj (F.obj Y ⊗ F.obj Z)) → F.obj (Y ⊗ Z) ⟶ F.obj Y ⊗ F.obj Z)
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))
have rw : adj.unit.app X ▷ Y ▷ Z ≫
  Iso.hom (α_ ((F ⋙ G).obj X) Y Z) ≫
    (F ⋙ G).obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
      G.obj (F.obj X) ◁
          (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
            G.map
              (F.map (μ G (F.obj Y) (F.obj Z)) ≫
                adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))) ≫
        μ G (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
Tactic: rw [← μ_natural_right, homEquiv_counit, map_comp_assoc,
        map_comp, tensorHom_def_assoc, ← associator_naturality_left_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
| adj.unit.app X ▷ Y ▷ Z ≫
    Iso.hom (α_ ((F ⋙ G).obj X) Y Z) ≫
      (F ⋙ G).obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        G.obj (F.obj X) ◁
            (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map
                (F.map (μ G (F.obj Y) (F.obj Z)) ≫
                  adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))) ≫
          μ G (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
have dsimp : adj.unit.app X ▷ Y ▷ Z ≫
  Iso.hom (α_ (G.obj (F.obj X)) Y Z) ≫
    G.obj (F.obj X) ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
      G.obj (F.obj X) ◁
          (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
            G.map
              (F.map (μ G (F.obj Y) (F.obj Z)) ≫
                adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))) ≫
        μ G (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
Tactic: dsimp
-- 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 X ▷ Y ▷ Z ≫
    Iso.hom (α_ (G.obj (F.obj X)) Y Z) ≫
      G.obj (F.obj X) ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        G.obj (F.obj X) ◁
            (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map
                (F.map (μ G (F.obj Y) (F.obj Z)) ≫
                  adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))) ≫
          μ G (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
have rw : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
  ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (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 [← MonoidalCategory.whiskerLeft_comp_assoc, map_comp,
        unit_naturality_assoc, MonoidalCategory.whiskerLeft_comp,
        unit_naturality_assoc, right_triangle_components, comp_id, assoc,
        tensorHom_def, MonoidalCategory.whiskerLeft_comp_assoc,
        ← associator_naturality_middle_assoc, ← associator_naturality_right_assoc,
        ← associativity G, ← comp_whiskerRight_assoc, ← tensorHom_def,
        ← whisker_exchange_assoc, ← comp_whiskerRight_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
| Iso.hom (α_ X Y Z) ≫
    (adj.unit.app X ⊗ₘ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
      μ G (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
        G.map
          (F.obj X ◁
            ((Equiv.symm
                    (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
                      (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) :
                  Equiv.{v₁ + 1, v₂ + 1}
                    (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
                    (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ⟶
                      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) :
                (a : Y ⊗ Z ⟶ G.obj (F.obj Y ⊗ F.obj Z)) → F.obj (Y ⊗ Z) ⟶ F.obj Y ⊗ F.obj Z)
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))
have rw : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
  ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (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 [← μ_natural_right, homEquiv_counit, map_comp_assoc,
        map_comp, tensorHom_def_assoc, ← associator_naturality_left_assoc]
      dsimp
      rw [← MonoidalCategory.whiskerLeft_comp_assoc, map_comp,
        unit_naturality_assoc, MonoidalCategory.whiskerLeft_comp,
        unit_naturality_assoc, right_triangle_components, comp_id, assoc,
        tensorHom_def, MonoidalCategory.whiskerLeft_comp_assoc,
        ← associator_naturality_middle_assoc, ← associator_naturality_right_assoc,
        ← associativity G, ← comp_whiskerRight_assoc, ← tensorHom_def,
        ← whisker_exchange_assoc, ← comp_whiskerRight_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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
⊢ adj.IsMonoidal
have refine_1 : 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))
Tactic: refine ⟨?_, fun X Y ↦ ?_⟩
-- 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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
refine_1 :
  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))
⊢ adj.IsMonoidal
have refine_2 : ∀ (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)))
Tactic: refine ⟨?_, fun X Y ↦ ?_⟩
-- 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
x : G.LaxMonoidal
⊢ (fun (x : F.OplaxMonoidal) ↦ (adj.rightAdjointLaxMonoidal : G.LaxMonoidal))
      ((fun (x : G.LaxMonoidal) ↦ (adj.leftAdjointOplaxMonoidal : F.OplaxMonoidal)) x) =
    x
have ε : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G) (ε G)
Tactic: ext
-- 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
x : G.LaxMonoidal
ε :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (LaxMonoidal.ε G)
    (LaxMonoidal.ε G)
⊢ (fun (x : F.OplaxMonoidal) ↦ (adj.rightAdjointLaxMonoidal : G.LaxMonoidal))
      ((fun (x : G.LaxMonoidal) ↦ (adj.leftAdjointOplaxMonoidal : F.OplaxMonoidal)) x) =
    x
have μ : ∀ (x_1 x_2 : D),
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj x_1) (G.obj x_2) ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) x_1 x_2))
    (μ G x_1 x_2) (μ G x_1 x_2)
Tactic: ext
-- 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
x : F.OplaxMonoidal
⊢ (fun (x : G.LaxMonoidal) ↦ (adj.leftAdjointOplaxMonoidal : F.OplaxMonoidal))
      ((fun (x : F.OplaxMonoidal) ↦ (adj.rightAdjointLaxMonoidal : G.LaxMonoidal)) x) =
    x
have η : Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (η F)
Tactic: ext
-- 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
x : F.OplaxMonoidal
η :
  Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (OplaxMonoidal.η F)
    (OplaxMonoidal.η F)
⊢ (fun (x : G.LaxMonoidal) ↦ (adj.leftAdjointOplaxMonoidal : F.OplaxMonoidal))
      ((fun (x : F.OplaxMonoidal) ↦ (adj.rightAdjointLaxMonoidal : G.LaxMonoidal)) x) =
    x
have δ : ∀ (x_1 x_2 : C),
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
    (δ F x_1 x_2) (δ F x_1 x_2)
Tactic: ext
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
this : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
⊢ IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (LaxMonoidal.ε e.inverse)
have simp : IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (e.toAdjunction.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inverse.map (OplaxMonoidal.η e.functor))
Tactic: simp only [this, Adjunction.rightAdjointLaxMonoidal_ε, Adjunction.homEquiv_unit]
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
this : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
⊢ e.inverse.Monoidal
have this₁ : IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (LaxMonoidal.ε e.inverse)
Tactic: have : IsIso (LaxMonoidal.ε e.inverse) := by
    simp only [this, Adjunction.rightAdjointLaxMonoidal_ε, Adjunction.homEquiv_unit]
    infer_instance
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
this_1 : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this :
  IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (LaxMonoidal.ε e.inverse)
X Y : D
⊢ IsIso (X := tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) (Y :=
    e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (LaxMonoidal.μ e.inverse X Y)
have simp : IsIso (X := tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) (Y :=
  e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
  (e.toAdjunction.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) ≫
    e.inverse.map
      (OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y) ≫
        (e.toAdjunction.counit.app X ⊗ₘ e.toAdjunction.counit.app Y)))
Tactic: simp only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
this_1 : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this :
  IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (LaxMonoidal.ε e.inverse)
⊢ e.inverse.Monoidal
have this₁ : ∀ (X Y : D),
  IsIso (X := tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) (Y :=
    e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (LaxMonoidal.μ e.inverse X Y)
Tactic: have : ∀ (X Y : D), IsIso (LaxMonoidal.μ e.inverse X Y) := fun X Y ↦ by
    simp only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]
    infer_instance
-- 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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) (ε e.functor)
have rw : Eq (α := e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
    (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)))
  (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor) (ε e.functor))
Tactic: rw [← cancel_epi (η e.functor), Monoidal.η_ε, ← functor_map_ε_inverse_comp_counitIso_hom_app,
    Category.assoc, Iso.hom_inv_id_app_assoc, Monoidal.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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
rw :
  Eq (α := e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
      (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)))
    (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor) (ε e.functor))
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) (ε e.functor)
have rw₁ : CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
    (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
  𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: rw [← cancel_epi (η e.functor), Monoidal.η_ε, ← functor_map_ε_inverse_comp_counitIso_hom_app,
    Category.assoc, Iso.hom_inv_id_app_assoc, Monoidal.map_ε_η]