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
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (Iso.inv (εIso F)))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (Iso.inv (εIso F)))
have ε : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
  (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (Iso.inv (εIso F)))
  (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F))
Tactic: rw [εIso_inv, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_inv]
-- 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
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
⊢ Eq (α :=
    (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F)
    (μ F)
have μ : ∀ (x x_1 : C),
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1))
    (μ F x x_1) (μ F x x_1)
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
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
x x_1 : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1))
    (μ F x x_1) (μ F x x_1)
have μ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (Iso.inv (μIso F x x_1)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (Iso.inv (μIso F x x_1)))
Tactic: rw [← cancel_mono (μIso F _ _).inv]
-- 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
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
x x_1 : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (Iso.inv (μIso F x x_1)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (Iso.inv (μIso F x x_1)))
have μ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (Iso.inv (μIso F x x_1)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (δ F x x_1))
Tactic: rw [μIso_inv, μ_δ, ← @μ_δ _ _ _ _ _ _ _ a, ← μIso_inv]
-- 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
εIso : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ≅ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μIso : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    Iso.inv (μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        (μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality :
  ∀ (X : C),
    Iso.inv (λ_ (F.obj X)) =
      F.map (Iso.inv (λ_ X)) ≫ Iso.inv (μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ εIso.inv ▷ F.obj X
oplax_right_unitality :
  ∀ (X : C),
    Iso.inv (ρ_ (F.obj X)) =
      F.map (Iso.inv (ρ_ X)) ≫ Iso.inv (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj X ◁ εIso.inv
X Y Z : C
⊢ (μIso X Y).hom ▷ F.obj Z ≫ Iso.hom (μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫ F.map (Iso.hom (α_ X Y Z)) =
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      F.obj X ◁ (μIso Y Z).hom ≫ Iso.hom (μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
have rw : Iso.inv (μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
    (μIso X Y).inv ▷ F.obj Z ≫
      (μIso X Y).hom ▷ F.obj Z ≫ Iso.hom (μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫ F.map (Iso.hom (α_ X Y Z)) =
  F.map (Iso.hom (α_ X Y Z)) ≫
    Iso.inv (μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
      F.obj X ◁ (μIso Y Z).inv ≫ F.obj X ◁ (μIso Y Z).hom ≫ Iso.hom (μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: rw [← cancel_epi ((μIso X Y).inv ▷ F.obj Z), ← cancel_epi (μIso (X ⊗ Y) Z).inv,
      reassoc_of% oplax_associativity]
-- 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
εIso : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ≅ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μIso : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    Iso.inv (μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        (μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality :
  ∀ (X : C),
    Iso.inv (λ_ (F.obj X)) =
      F.map (Iso.inv (λ_ X)) ≫ Iso.inv (μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ εIso.inv ▷ F.obj X
oplax_right_unitality :
  ∀ (X : C),
    Iso.inv (ρ_ (F.obj X)) =
      F.map (Iso.inv (ρ_ X)) ≫ Iso.inv (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj X ◁ εIso.inv
X : C
⊢ Iso.hom (λ_ (F.obj X)) =
    εIso.hom ▷ F.obj X ≫ Iso.hom (μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ F.map (Iso.hom (λ_ X))
have rw : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X)) =
  (εIso.hom ▷ F.obj X ≫ Iso.hom (μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ F.map (Iso.hom (λ_ X))) ≫
    F.map (Iso.inv (λ_ X)) ≫ Iso.inv (μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ εIso.inv ▷ F.obj X
Tactic: rw [← cancel_mono (λ_ (F.obj X)).inv, Iso.hom_inv_id, oplax_left_unitality]
-- 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
εIso : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ≅ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μIso : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    Iso.inv (μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        (μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality :
  ∀ (X : C),
    Iso.inv (λ_ (F.obj X)) =
      F.map (Iso.inv (λ_ X)) ≫ Iso.inv (μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ εIso.inv ▷ F.obj X
oplax_right_unitality :
  ∀ (X : C),
    Iso.inv (ρ_ (F.obj X)) =
      F.map (Iso.inv (ρ_ X)) ≫ Iso.inv (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj X ◁ εIso.inv
X : C
⊢ Iso.hom (ρ_ (F.obj X)) =
    F.obj X ◁ εIso.hom ≫ Iso.hom (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ X))
have rw : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
  (F.obj X ◁ εIso.hom ≫ Iso.hom (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ X))) ≫
    F.map (Iso.inv (ρ_ X)) ≫ Iso.inv (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj X ◁ εIso.inv
Tactic: rw [← cancel_mono (ρ_ (F.obj X)).inv, Iso.hom_inv_id, oplax_right_unitality]
-- 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
h : F.CoreMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
⊢ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 = F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
have rw : (h.μIso X x_1).hom ≫ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 =
  (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_left_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
rw :
  (h.μIso X x_1).hom ≫ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 =
    (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
⊢ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 = F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
have rw₁ : F.map x ▷ F.obj x_1 = (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_left_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
rw :
  (h.μIso X x_1).hom ≫ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 =
    (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
rw₁ : F.map x ▷ F.obj x_1 = (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
⊢ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 = F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
have rw₂ : F.map x ▷ F.obj x_1 = F.map x ▷ F.obj x_1 ≫ (h.μIso Y x_1).hom ≫ (h.μIso Y x_1).inv
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_left_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
rw :
  (h.μIso X x_1).hom ≫ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 =
    (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
rw₁ : F.map x ▷ F.obj x_1 = (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
rw₂ : F.map x ▷ F.obj x_1 = F.map x ▷ F.obj x_1 ≫ (h.μIso Y x_1).hom ≫ (h.μIso Y x_1).inv
⊢ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 = F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
have rw₃ : F.map x ▷ F.obj x_1 = F.map x ▷ F.obj x_1 ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_left_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
rw :
  (h.μIso X x_1).hom ≫ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 =
    (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
rw₁ : F.map x ▷ F.obj x_1 = (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
rw₂ : F.map x ▷ F.obj x_1 = F.map x ▷ F.obj x_1 ≫ (h.μIso Y x_1).hom ≫ (h.μIso Y x_1).inv
rw₃ : F.map x ▷ F.obj x_1 = F.map x ▷ F.obj x_1 ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))
⊢ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 = F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
have rw₄ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))
  (F.map x ▷ F.obj x_1) (F.map x ▷ F.obj x_1)
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_left_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y x : C
x_1 : X ⟶ Y
⊢ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
have rw : (h.μIso x X).hom ≫ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_right_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y x : C
x_1 : X ⟶ Y
rw : (h.μIso x X).hom ≫ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
⊢ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
have rw₁ : F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_right_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y x : C
x_1 : X ⟶ Y
rw : (h.μIso x X).hom ≫ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
rw₁ : F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
⊢ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
have rw₂ : F.obj x ◁ F.map x_1 = F.obj x ◁ F.map x_1 ≫ (h.μIso x Y).hom ≫ (h.μIso x Y).inv
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_right_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y x : C
x_1 : X ⟶ Y
rw : (h.μIso x X).hom ≫ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
rw₁ : F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
rw₂ : F.obj x ◁ F.map x_1 = F.obj x ◁ F.map x_1 ≫ (h.μIso x Y).hom ≫ (h.μIso x Y).inv
⊢ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
have rw₃ : F.obj x ◁ F.map x_1 = F.obj x ◁ F.map x_1 ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_right_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y x : C
x_1 : X ⟶ Y
rw : (h.μIso x X).hom ≫ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
rw₁ : F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
rw₂ : F.obj x ◁ F.map x_1 = F.obj x ◁ F.map x_1 ≫ (h.μIso x Y).hom ≫ (h.μIso x Y).inv
rw₃ : F.obj x ◁ F.map x_1 = F.obj x ◁ F.map x_1 ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
⊢ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
have rw₄ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
  (F.obj x ◁ F.map x_1) (F.obj x ◁ F.map x_1)
Tactic: rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_right_assoc, Iso.hom_inv_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
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
h : F.CoreMonoidal
X Y Z : C
⊢ Iso.inv (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
have rw : Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
    Iso.inv (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
  Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
    F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
Tactic: rw [← cancel_epi (h.μIso (X ⊗ Y) Z).hom, Iso.hom_inv_id_assoc,
      ← cancel_epi ((h.μIso X Y).hom ▷ F.obj Z), hom_inv_whiskerRight_assoc,
      associativity_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv, 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
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
h : F.CoreMonoidal
X Y Z : C
rw :
  Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      Iso.inv (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
⊢ Iso.inv (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
have rw₁ : (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
  Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
    F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
Tactic: rw [← cancel_epi (h.μIso (X ⊗ Y) Z).hom, Iso.hom_inv_id_assoc,
      ← cancel_epi ((h.μIso X Y).hom ▷ F.obj Z), hom_inv_whiskerRight_assoc,
      associativity_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv, 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
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
h : F.CoreMonoidal
X Y Z : C
rw :
  Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      Iso.inv (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
rw₁ :
  (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
⊢ Iso.inv (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
have rw₂ : (h.μIso X Y).hom ▷ F.obj Z ≫ (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
  (h.μIso X Y).hom ▷ F.obj Z ≫
    Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
Tactic: rw [← cancel_epi (h.μIso (X ⊗ Y) Z).hom, Iso.hom_inv_id_assoc,
      ← cancel_epi ((h.μIso X Y).hom ▷ F.obj Z), hom_inv_whiskerRight_assoc,
      associativity_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv, comp_id]