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 : 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))
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)))
⊢ 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.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (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_ε_η]
-- 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))
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)))
rw₂ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
      (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ 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 := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
    (e.functor.map (ε e.inverse))
    (e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫
      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_ε_η]
-- 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))
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)))
rw₂ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
      (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₃ :
  CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
      (e.functor.map (ε e.inverse))
      (e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫
        e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ 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 := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
    (e.functor.map (ε e.inverse)) (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_ε_η]
-- 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))
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)))
rw₂ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
      (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₃ :
  CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
      (e.functor.map (ε e.inverse))
      (e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫
        e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₄ :
  CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
      (e.functor.map (ε e.inverse)) (e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ 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.{v₂ + 1} (α := e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (𝟙 (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_ε_η]
-- 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
X Y : C
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)) ⟶
      e.functor.obj
        (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj 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.functor X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y))
have rw : Eq (α :=
  e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
    e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj 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.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y))
Tactic: rw [← cancel_epi (δ e.functor _ _), Monoidal.δ_μ_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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
X Y : C
⊢ Eq (α :=
    e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      e.functor.obj
        (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj 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.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y))
have a : Eq (α :=
  e.inverse.obj (e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ⟶
    e.inverse.obj
      (e.functor.obj
        (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y)))))
  (e.inverse.map
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj 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.inverse.map (e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y)))
Tactic: apply e.inverse.map_injective
-- 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.counitInv.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.counitInv.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.counitInv.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.counitInv.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.counitInv.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_ε_η]
-- 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.counitInv.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))
rw₁ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (e.counitInv.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.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (e.counitInv.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_ε_η]
-- 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.counitInv.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))
rw₁ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₂ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
      (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) (ε e.functor)
have rw₃ : CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
    (e.functor.map (ε e.inverse))
    (e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫
      e.counitInv.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_ε_η]
-- 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.counitInv.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))
rw₁ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₂ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
      (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₃ :
  CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
      (e.functor.map (ε e.inverse))
      (e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫
        e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) (ε e.functor)
have rw₄ : CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
    (e.functor.map (ε e.inverse)) (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_ε_η]
-- 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.counitInv.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))
rw₁ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₂ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
      (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₃ :
  CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
      (e.functor.map (ε e.inverse))
      (e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫
        e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₄ :
  CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
      (e.functor.map (ε e.inverse)) (e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) (ε e.functor)
have rw₅ : Eq.{v₂ + 1} (α := e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (𝟙 (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_ε_η]
-- 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.toAdjunction.unit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.symm.inverse.map (η e.symm.functor))
have simp : 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))
Tactic: simp only [toAdjunction]