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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.symm.inverse.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε e.symm.inverse) (e.symm.unit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.symm.inverse.map (η e.symm.functor))
have dsimp : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε e.functor)
  (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse))
Tactic: dsimp [symm]
-- 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
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε e.functor)
    (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse))
have rw : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε e.functor)
  (ε e.functor)
Tactic: rw [counitIso_inv_app_comp_functor_map_η_inverse]
-- 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
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
X Y : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ⟶
      e.symm.inverse.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.symm.inverse X Y)
    (e.symm.toAdjunction.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y)) ≫
      e.symm.inverse.map
        (δ e.symm.functor (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ≫
          (e.symm.toAdjunction.counit.app X ⊗ₘ e.symm.toAdjunction.counit.app Y)))
have simp : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ⟶
    e.symm.inverse.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (μ e.symm.inverse X Y)
  (e.symm.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y)) ≫
    e.symm.inverse.map
      (δ e.symm.functor (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ≫ (e.symm.counit.app X ⊗ₘ e.symm.counit.app Y)))
Tactic: simp only [toAdjunction]
-- 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
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
X Y : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ⟶
      e.symm.inverse.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.symm.inverse X Y)
    (e.symm.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y)) ≫
      e.symm.inverse.map
        (δ e.symm.functor (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ≫ (e.symm.counit.app X ⊗ₘ e.symm.counit.app Y)))
have dsimp : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y) ⟶
    e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (μ e.functor X Y)
  (e.counitIso.inv.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)) ≫
    e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y) ≫ (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y)))
Tactic: dsimp [symm]
-- 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
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
X Y : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y) ⟶
      e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.functor X Y)
    (e.counitIso.inv.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y) ≫ (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y)))
have rw : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y) ⟶
    e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (μ e.functor X Y)
  (μ e.functor X Y ≫
    e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y) ≫
      e.functor.map (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y))
Tactic: rw [map_comp, counitIso_inv_app_tensor_comp_functor_map_δ_inverse_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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
e' : Equivalence.{v₂, v₃, u₂, u₃} D E
inst_10 : e'.functor.Monoidal
inst_11 : e'.inverse.Monoidal
inst_12 : e'.IsMonoidal
⊢ (e.trans e').toAdjunction.IsMonoidal
have rw : (e.toAdjunction.comp e'.toAdjunction).IsMonoidal
Tactic: rw [trans_toAdjunction]
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (Iso.hom ((i.symm.app X ⊗ᵢ i.symm.app Y) ≪≫ μIso F X Y ≪≫ i.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ▷ G.obj Z ≫
      Iso.hom
          ((i.symm.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ᵢ i.symm.app Z) ≪≫
            μIso F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≪≫
              i.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) ≫
        G.map (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ Iso.hom ((i.symm.app Y ⊗ᵢ i.symm.app Z) ≪≫ μIso F Y Z ≪≫ i.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
        Iso.hom
          ((i.symm.app X ⊗ᵢ i.symm.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≪≫
            μIso F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≪≫
              i.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))))
have simp : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
    LaxMonoidal.μ F X Y ▷ G.obj Z ≫
      i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
        (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z) ≫
          LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
            i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
              G.map (Iso.hom (α_ X Y Z)))
  (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
    G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
      G.obj X ◁ LaxMonoidal.μ F Y Z ≫
        G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
          (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
            LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
              i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
Tactic: simp only [Iso.trans_hom, tensorIso_hom, Iso.app_hom, Iso.symm_hom, μIso_hom, comp_whiskerRight,
      Category.assoc, MonoidalCategory.whiskerLeft_comp]
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
          (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
              i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
                G.map (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
              LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
                i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
have rw : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
    LaxMonoidal.μ F X Y ▷ G.obj Z ≫
      i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
        (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z) ≫
          LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
            F.map (Iso.hom (α_ X Y Z)) ≫
              i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
    G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
      G.obj X ◁ LaxMonoidal.μ F Y Z ≫
        G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
          (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
            LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
              i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
Tactic: rw [← i.hom.naturality, map_associator_assoc, Functor.OplaxMonoidal.associativity_assoc,
      whiskerLeft_δ_μ_assoc, δ_μ_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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
          (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
              F.map (Iso.hom (α_ X Y Z)) ≫
                i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
              LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
                i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
have simp : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  (((((((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫ LaxMonoidal.μ F X Y ▷ G.obj Z) ≫
            i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z) ≫
          (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z)) ≫
        LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      F.map (Iso.hom (α_ X Y Z))) ≫
    i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  ((((((Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
            G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
        (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
    i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
Tactic: simp only [← Category.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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (((((((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫ LaxMonoidal.μ F X Y ▷ G.obj Z) ≫
              i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z) ≫
            (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z)) ≫
          LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        F.map (Iso.hom (α_ X Y Z))) ≫
      i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((((((Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
              G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
            G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
          (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
        LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
      i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
have e_a : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  ((((((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫ LaxMonoidal.μ F X Y ▷ G.obj Z) ≫
          i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z) ≫
        (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z)) ≫
      LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
    F.map (Iso.hom (α_ X Y Z)))
  (((((Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
          G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
        G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
      (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
    LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: congr 1
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
| i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
    (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z)
have a : i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ
  𝟙 (G.obj Z) ≫ i.inv.app Z
Tactic: rw [← tensorHom_id, tensorHom_comp_tensorHom]
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
| i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ
    𝟙 (G.obj Z) ≫ i.inv.app Z
have a : F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ◁ i.inv.app Z
Tactic: simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom]
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
| i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
    (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z)
have a : F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ◁ i.inv.app Z
Tactic: rw [← tensorHom_id, tensorHom_comp_tensorHom]
      simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom]
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((((((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫ LaxMonoidal.μ F X Y ▷ G.obj Z) ≫
            i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z) ≫
          (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z)) ≫
        LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      F.map (Iso.hom (α_ X Y Z)))
    (((((Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
            G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
        (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
have e_a : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
    LaxMonoidal.μ F X Y ▷ G.obj Z ≫
      (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ◁ i.inv.app Z ≫
          LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        F.map (Iso.hom (α_ X Y Z)))
  (((((Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
          G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
        G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
      (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
    LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: slice_lhs 3 4 =>
      rw [← tensorHom_id, tensorHom_comp_tensorHom]
      simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom]
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ◁ i.inv.app Z ≫
            LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
          F.map (Iso.hom (α_ X Y Z)))
    (((((Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
            G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
        (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
have e_a : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
    LaxMonoidal.μ F X Y ▷ G.obj Z ≫
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ◁ i.inv.app Z ≫
        LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))
  (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
    G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
      G.obj X ◁ LaxMonoidal.μ F Y Z ≫
        G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
          (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
            LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: simp only [Category.assoc]