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
inst_4 : F.LaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (μ F X Y ▷ F.obj Z ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) ≫ F.map (Iso.inv (α_ X Y Z)))
rw₁ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z) ≫ Iso.inv (α_ X Y Z)))
rw₂ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (μ F X Y ▷ F.obj Z ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
        F.map (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
rw₃ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (μ F X Y ▷ F.obj Z ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
        𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (Iso.inv (α_ X Y Z)))
have rw₄ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
  (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
  (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
Tactic: rw [← associativity_assoc, ← F.map_comp, Iso.hom_inv_id, map_id, Category.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 Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
    (Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))
have rw : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
  (Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: rw [associativity, Iso.inv_hom_id_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
    (Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
    (Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))
have rw₁ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
  (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
Tactic: rw [associativity, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y : C
f : X ⟶ Y
X' : C
⊢ F.map f ▷ F.obj X' ≫ μ Y X' = μ X X' ≫ F.map (f ▷ X')
have simp_rw : (F.map f ⊗ₘ 𝟙 (F.obj X')) ≫ μ Y X' = μ X X' ≫ F.map (f ⊗ₘ 𝟙 X')
Tactic: simp_rw [← tensorHom_id, ← F.map_id, μ_natural]
-- 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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y : C
f : X ⟶ Y
X' : C
simp_rw : (F.map f ⊗ₘ 𝟙 (F.obj X')) ≫ μ Y X' = μ X X' ≫ F.map (f ⊗ₘ 𝟙 X')
⊢ F.map f ▷ F.obj X' ≫ μ Y X' = μ X X' ≫ F.map (f ▷ X')
have simp_rw₁ : (F.map f ⊗ₘ F.map (𝟙 X')) ≫ μ Y X' = μ X X' ≫ F.map (f ⊗ₘ 𝟙 X')
Tactic: simp_rw [← tensorHom_id, ← F.map_id, μ_natural]
-- 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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y X' : C
f : X ⟶ Y
⊢ F.obj X' ◁ F.map f ≫ μ X' Y = μ X' X ≫ F.map (X' ◁ f)
have simp_rw : (𝟙 (F.obj X') ⊗ₘ F.map f) ≫ μ X' Y = μ X' X ≫ F.map (𝟙 X' ⊗ₘ f)
Tactic: simp_rw [← id_tensorHom, ← F.map_id, μ_natural]
-- 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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y X' : C
f : X ⟶ Y
simp_rw : (𝟙 (F.obj X') ⊗ₘ F.map f) ≫ μ X' Y = μ X' X ≫ F.map (𝟙 X' ⊗ₘ f)
⊢ F.obj X' ◁ F.map f ≫ μ X' Y = μ X' X ≫ F.map (X' ◁ f)
have simp_rw₁ : (F.map (𝟙 X') ⊗ₘ F.map f) ≫ μ X' Y = μ X' X ≫ F.map (𝟙 X' ⊗ₘ f)
Tactic: simp_rw [← id_tensorHom, ← F.map_id, μ_natural]
-- 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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y Z : C
⊢ μ X Y ▷ F.obj Z ≫ μ (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 ◁ μ Y Z ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
have simp_rw : (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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 ◁ μ Y Z ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
Tactic: simp_rw [← tensorHom_id, ← id_tensorHom, 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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y Z : C
simp_rw :
  (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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 ◁ μ Y Z ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
⊢ μ X Y ▷ F.obj Z ≫ μ (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 ◁ μ Y Z ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
have simp_rw₁ : (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
Tactic: simp_rw [← tensorHom_id, ← id_tensorHom, 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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X : C
⊢ Iso.hom (λ_ (F.obj X)) = ε ▷ F.obj X ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
have simp_rw : Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
Tactic: simp_rw [← tensorHom_id, 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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (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) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X : C
⊢ Iso.hom (ρ_ (F.obj X)) = F.obj X ◁ ε ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
have simp_rw : Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
Tactic: simp_rw [← id_tensorHom, 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.LaxMonoidal
inst_8 : G.LaxMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj x_1) ⟶
      (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1))
    ((F ⋙ G).map x ▷ (F ⋙ G).obj x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
        (μ G (F.obj Y) (F.obj x_1)) (G.map (μ F Y x_1)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj x_1)))
        (μ G (F.obj X) (F.obj x_1)) (G.map (μ F X x_1)) ≫
      (F ⋙ G).map (x ▷ x_1))
have simp_rw : Eq (α :=
  tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X)) (G.obj (F.obj x_1)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
  ((F ⋙ G).map x ▷ G.obj (F.obj x_1) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
      (μ G (F.obj Y) (F.obj x_1)) (G.map (μ F Y x_1)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj x_1))) (μ G (F.obj X) (F.obj x_1))
      (G.map (μ F X x_1)) ≫
    (F ⋙ G).map (x ▷ x_1))
Tactic: simp_rw [comp_obj, F.comp_map, μ_natural_left_assoc, assoc, ← G.map_comp, μ_natural_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.LaxMonoidal
inst_8 : G.LaxMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
simp_rw :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X)) (G.obj (F.obj x_1)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
    ((F ⋙ G).map x ▷ G.obj (F.obj x_1) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
        (μ G (F.obj Y) (F.obj x_1)) (G.map (μ F Y x_1)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj x_1)))
        (μ G (F.obj X) (F.obj x_1)) (G.map (μ F X x_1)) ≫
      (F ⋙ G).map (x ▷ x_1))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj x_1) ⟶
      (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1))
    ((F ⋙ G).map x ▷ (F ⋙ G).obj x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
        (μ G (F.obj Y) (F.obj x_1)) (G.map (μ F Y x_1)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj x_1)))
        (μ G (F.obj X) (F.obj x_1)) (G.map (μ F X x_1)) ≫
      (F ⋙ G).map (x ▷ x_1))
have simp_rw₁ : Eq (α :=
  tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X)) (G.obj (F.obj x_1)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
  (G.map (F.map x) ▷ G.obj (F.obj x_1) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
      (μ G (F.obj Y) (F.obj x_1)) (G.map (μ F Y x_1)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj x_1))) (μ G (F.obj X) (F.obj x_1))
      (G.map (μ F X x_1)) ≫
    G.map (F.map (x ▷ x_1)))
Tactic: simp_rw [comp_obj, F.comp_map, μ_natural_left_assoc, assoc, ← G.map_comp, μ_natural_left]