awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
e_1 :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
      ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
⊢ inclusionObj n ◁ f ≫ Iso.hom (normalizeIsoApp C Y { as := n : Discrete (NormalMonoidalObject C) }) =
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom
have h : inclusionObj n ◁ f ≫ Iso.hom (normalizeIsoApp' C Y { as := n : Discrete (NormalMonoidalObject C) }.as) =
  inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom
Tactic: rw [normalizeIsoApp_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
e_1 :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
      ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
⊢ ((normalizeIsoAux C X).hom ≫ (normalize' C).map f).app { as := n } =
    (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
have h : Eq (α :=
  tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj'.obj { as := n }).as)
  (Iso.hom (normalizeIsoApp C X { as := n : Discrete (NormalMonoidalObject C) }) ≫ eqToHom sorry :
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
      inclusionObj (Y.normalizeObj'.obj { as := n }).as)
  ((normalizeIsoApp' C X n).hom ≫ eqToHom sorry :
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
e_1 :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
      ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
⊢ Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
      inclusionObj (Y.normalizeObj'.obj { as := n }).as)
    (Iso.hom (normalizeIsoApp C X { as := n : Discrete (NormalMonoidalObject C) }) ≫ eqToHom ⋯ :
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
        inclusionObj (Y.normalizeObj'.obj { as := n }).as)
    ((normalizeIsoApp' C X n).hom ≫ eqToHom ⋯ :
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
have h : Eq (α :=
  tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj'.obj { as := n }).as)
  (Iso.hom (normalizeIsoApp' C X { as := n : Discrete (NormalMonoidalObject C) }.as) ≫ eqToHom sorry)
  ((normalizeIsoApp' C X n).hom ≫ eqToHom sorry)
Tactic: rw [normalizeIsoApp_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
⊢ Eq (α := obj (𝟭 (F C)) X ⟶ (fullNormalize C ⋙ inclusion).obj Y)
    (map (𝟭 (F C)) f ≫
      Iso.hom
        ((fun (X : F C) ↦
            (Iso.trans (Y :=
                tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
                (Iso.symm (λ_ X)) (((normalizeIso C).app X).app { as := NormalMonoidalObject.unit }) :
              obj (𝟭 (F C)) X ≅ (fullNormalize C ⋙ inclusion).obj X))
          Y))
    (Iso.hom
        ((fun (X : F C) ↦
            (Iso.trans (Y :=
                tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
                (Iso.symm (λ_ X)) (((normalizeIso C).app X).app { as := NormalMonoidalObject.unit }) :
              obj (𝟭 (F C)) X ≅ (fullNormalize C ⋙ inclusion).obj X))
          X) ≫
      (fullNormalize C ⋙ inclusion).map f)
have dsimp : Eq (α := X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
  (f ≫
      CategoryStruct.comp (Y :=
        tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) Y)
        (Iso.inv (λ_ Y)) (((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit }) :
    X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
  (CategoryStruct.comp (Y := inclusionObj ((fullNormalize C).obj X).as)
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
        (Iso.inv (λ_ X)) (((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit }))
      (eqToHom sorry) :
    X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
⊢ Eq (α := X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
    (f ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) Y)
          (Iso.inv (λ_ Y)) (((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit }) :
      X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
    (CategoryStruct.comp (Y := inclusionObj ((fullNormalize C).obj X).as)
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
          (Iso.inv (λ_ X)) (((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit }))
        (eqToHom ⋯) :
      X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
have rw : (𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory) ◁ f ≫
    ((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit } =
  CategoryStruct.comp (Y := inclusionObj ((fullNormalize C).obj X).as)
    (((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit : Discrete (NormalMonoidalObject C) })
    (eqToHom sorry)
Tactic: rw [leftUnitor_inv_naturality_assoc, Category.assoc, Iso.cancel_iso_inv_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (hypothesis)
Goal:
C : Type u
X Y : F C
f g : X ⟶ Y
⊢ f = g
have hfg : (fullNormalize C).map f = (fullNormalize C).map g
Tactic: have hfg : (fullNormalize C).map f = (fullNormalize C).map g := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (hypothesis)
Goal:
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
⊢ f = g
have hf : (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y = map (𝟭 (F C)) f
Tactic: have hf := NatIso.naturality_2 (fullNormalizeIso.{u} C) f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (hypothesis)
Goal:
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y =
    map (𝟭 (F C)) f
⊢ f = g
have hg : (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map g ≫ (fullNormalizeIso C).inv.app Y = map (𝟭 (F C)) g
Tactic: have hg := NatIso.naturality_2 (fullNormalizeIso.{u} C) g
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (Iso.inv (λ_ (F.obj X))) (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.inv (λ_ X)))
have rw : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
  (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.hom (λ_ (F.obj X)) ≫ F.map (Iso.inv (λ_ X)))
Tactic: rw [Iso.inv_comp_eq, left_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.hom (λ_ (F.obj X)) ≫ F.map (Iso.inv (λ_ X)))
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (Iso.inv (λ_ (F.obj X))) (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.inv (λ_ X)))
have rw₁ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
  (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫
    F.map (Iso.inv (λ_ X)))
Tactic: rw [Iso.inv_comp_eq, left_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.hom (λ_ (F.obj X)) ≫ F.map (Iso.inv (λ_ X)))
rw₁ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
        (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫
      F.map (Iso.inv (λ_ X)))
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (Iso.inv (λ_ (F.obj X))) (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.inv (λ_ X)))
have rw₂ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
  (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
    (ε F ▷ F.obj X) ((μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫ F.map (Iso.inv (λ_ X))))
Tactic: rw [Iso.inv_comp_eq, left_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.hom (λ_ (F.obj X)) ≫ F.map (Iso.inv (λ_ X)))
rw₁ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
        (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫
      F.map (Iso.inv (λ_ X)))
rw₂ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (ε F ▷ F.obj X) ((μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫ F.map (Iso.inv (λ_ X))))
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (Iso.inv (λ_ (F.obj X))) (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.inv (λ_ X)))
have rw₃ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
  (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
    (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X)) ≫ F.map (Iso.inv (λ_ X))))
Tactic: rw [Iso.inv_comp_eq, left_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.hom (λ_ (F.obj X)) ≫ F.map (Iso.inv (λ_ X)))
rw₁ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
        (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫
      F.map (Iso.inv (λ_ X)))
rw₂ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (ε F ▷ F.obj X) ((μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫ F.map (Iso.inv (λ_ X))))
rw₃ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X)) ≫ F.map (Iso.inv (λ_ X))))
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (Iso.inv (λ_ (F.obj X))) (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.inv (λ_ X)))
have rw₄ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
  (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
    (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X) ≫ Iso.inv (λ_ X))))
Tactic: rw [Iso.inv_comp_eq, left_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (Iso.inv (ρ_ (F.obj X))) (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.map (Iso.inv (ρ_ X)))
have rw : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
  (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (ρ_ (F.obj X)) ≫ F.map (Iso.inv (ρ_ X)))
Tactic: rw [Iso.inv_comp_eq, right_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (ρ_ (F.obj X)) ≫ F.map (Iso.inv (ρ_ X)))
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (Iso.inv (ρ_ (F.obj X))) (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.map (Iso.inv (ρ_ X)))
have rw₁ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
  (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.obj X ◁ ε F) (μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))) ≫
    F.map (Iso.inv (ρ_ X)))
Tactic: rw [Iso.inv_comp_eq, right_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (ρ_ (F.obj X)) ≫ F.map (Iso.inv (ρ_ X)))
rw₁ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.obj X ◁ ε F) (μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))) ≫
      F.map (Iso.inv (ρ_ X)))
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (Iso.inv (ρ_ (F.obj X))) (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.map (Iso.inv (ρ_ X)))
have rw₂ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
  (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.obj X ◁ ε F) ((μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))) ≫ F.map (Iso.inv (ρ_ X))))
Tactic: rw [Iso.inv_comp_eq, right_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]