awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
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))
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)))
⊢ 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)))
  (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.map x ▷ 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]
-- 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 x : C
x_1 : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj X) ⟶ (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y))
    ((F ⋙ G).obj x ◁ (F ⋙ G).map x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      (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)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
  (G.obj (F.obj x) ◁ (F ⋙ G).map x_1 ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
      (G.map (μ F x Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
      (G.map (μ F x X)) ≫
    (F ⋙ G).map (x ◁ x_1))
Tactic: simp_rw [comp_obj, F.comp_map, μ_natural_right_assoc, assoc, ← G.map_comp, μ_natural_right]
-- 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 x : C
x_1 : X ⟶ Y
simp_rw :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj X)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
    (G.obj (F.obj x) ◁ (F ⋙ G).map x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      (F ⋙ G).map (x ◁ x_1))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj X) ⟶ (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y))
    ((F ⋙ G).obj x ◁ (F ⋙ G).map x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      (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)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
  (G.obj (F.obj x) ◁ G.map (F.map x_1) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
      (G.map (μ F x Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
      (G.map (μ F x X)) ≫
    G.map (F.map (x ◁ x_1)))
Tactic: simp_rw [comp_obj, F.comp_map, μ_natural_right_assoc, assoc, ← G.map_comp, μ_natural_right]
-- 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 x : C
x_1 : X ⟶ Y
simp_rw :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj X)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
    (G.obj (F.obj x) ◁ (F ⋙ G).map x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      (F ⋙ G).map (x ◁ x_1))
simp_rw₁ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj X)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
    (G.obj (F.obj x) ◁ G.map (F.map x_1) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      G.map (F.map (x ◁ x_1)))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj X) ⟶ (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y))
    ((F ⋙ G).obj x ◁ (F ⋙ G).map x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      (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)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
    (G.map (F.obj x ◁ F.map x_1) ≫ G.map (μ F x Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
      (G.map (μ F x X)) ≫
    G.map (F.map (x ◁ x_1)))
Tactic: simp_rw [comp_obj, F.comp_map, μ_natural_right_assoc, assoc, ← G.map_comp, μ_natural_right]
-- 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 x : C
x_1 : X ⟶ Y
simp_rw :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj X)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
    (G.obj (F.obj x) ◁ (F ⋙ G).map x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      (F ⋙ G).map (x ◁ x_1))
simp_rw₁ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj X)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
    (G.obj (F.obj x) ◁ G.map (F.map x_1) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      G.map (F.map (x ◁ x_1)))
simp_rw₂ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj X)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
      (G.map (F.obj x ◁ F.map x_1) ≫ G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      G.map (F.map (x ◁ x_1)))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj X) ⟶ (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y))
    ((F ⋙ G).obj x ◁ (F ⋙ G).map x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (μ G (F.obj x) (F.obj Y))
        (G.map (μ F x Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
        (G.map (μ F x X)) ≫
      (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)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
    (G.map (F.obj x ◁ F.map x_1) ≫ G.map (μ F x Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (μ G (F.obj x) (F.obj X))
    (G.map (μ F x X) ≫ G.map (F.map (x ◁ x_1))))
Tactic: simp_rw [comp_obj, F.comp_map, μ_natural_right_assoc, assoc, ← G.map_comp, μ_natural_right]
-- 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 x_1 x_2 : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj x_1))
        ((F ⋙ G).obj x_2) ⟶
      (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
    (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).obj x_2 ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
          (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
          (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2)) ≫
        (F ⋙ G).map (Iso.hom (α_ x x_1 x_2)))
    (Iso.hom (α_ ((F ⋙ G).obj x) ((F ⋙ G).obj x_1) ((F ⋙ G).obj x_2)) ≫
      (F ⋙ G).obj x ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
have dsimp : Eq (α :=
  tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
      (G.obj (F.obj x_2)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
  (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.obj (F.obj x_2) ≫
    CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
        (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
        (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2)) ≫
      G.map (F.map (Iso.hom (α_ x x_1 x_2))))
  (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
    G.obj (F.obj x) ◁
        CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
          (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
      CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
        (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
        (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
Tactic: dsimp
-- 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.OplaxMonoidal
X : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (η F ▷ F.obj X ≫ Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
have rw : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
    (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (Iso.hom (λ_ (F.obj X))))
  (F.map (Iso.hom (λ_ X)))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (η F ▷ F.obj X ≫ Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
have rw₁ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
  (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (F.map (Iso.hom (λ_ X)) ≫ Iso.inv (λ_ (F.obj X)))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
    (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (F.map (Iso.hom (λ_ X)) ≫ Iso.inv (λ_ (F.obj X)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (η F ▷ F.obj X ≫ Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
have rw₂ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
  (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X)
  (F.map (Iso.hom (λ_ X)) ≫
    CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
      (F.map (Iso.inv (λ_ X))) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
    (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (F.map (Iso.hom (λ_ X)) ≫ Iso.inv (λ_ (F.obj X)))
rw₂ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
    (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X)
    (F.map (Iso.hom (λ_ X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
        (F.map (Iso.inv (λ_ X))) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (η F ▷ F.obj X ≫ Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
have rw₃ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
  (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.hom (λ_ X)) ≫ F.map (Iso.inv (λ_ X))) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]