awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : D
⊢ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
        (F.map (μ G X Y)) ≫
      adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
have rw : CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
    (F.map (μ G X Y) ≫ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) =
  (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
Tactic: rw [assoc, map_μ_comp_counit_app_tensor, μ_δ_assoc, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : D
rw :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
      (F.map (μ G X Y) ≫ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
⊢ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
        (F.map (μ G X Y)) ≫
      adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
have rw₁ : CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
    (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)) =
  (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
Tactic: rw [assoc, map_μ_comp_counit_app_tensor, μ_δ_assoc, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : D
rw :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
      (F.map (μ G X Y) ≫ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
rw₁ :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
      (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
⊢ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
        (F.map (μ G X Y)) ≫
      adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
have rw₂ : adj.counit.app X ⊗ₘ adj.counit.app Y = (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
Tactic: rw [assoc, map_μ_comp_counit_app_tensor, μ_δ_assoc, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : D
rw :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
      (F.map (μ G X Y) ≫ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
rw₁ :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
      (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
rw₂ :
  adj.counit.app X ⊗ₘ adj.counit.app Y =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
⊢ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
        (F.map (μ G X Y)) ≫
      adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
have rw₃ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj Y)) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
  (adj.counit.app X ⊗ₘ adj.counit.app Y) (adj.counit.app X ⊗ₘ adj.counit.app Y)
Tactic: rw [assoc, map_μ_comp_counit_app_tensor, μ_δ_assoc, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (hypothesis)
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
X Y Z : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
α : X.Hom Y
β : Y.Hom Z
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)
have this : NatTrans.IsMonoidal α.hom
Tactic: have := α.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (hypothesis)
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
X Y Z : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
α : X.Hom Y
β : Y.Hom Z
this : NatTrans.IsMonoidal α.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)
have this₁ : NatTrans.IsMonoidal β.hom
Tactic: have := β.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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 G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
α β : F ⟶ G
h : α.hom = β.hom
⊢ α = β
have mk : ∀ (hom : F.toFunctor ⟶ G.toFunctor) (isMonoidal : NatTrans.IsMonoidal hom)
  (h : { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom = β.hom),
  { hom := hom, isMonoidal := isMonoidal : F.Hom G } = β
Tactic: cases α
Cleared hypotheses: α, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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 G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
β : F ⟶ G
hom : F.toFunctor ⟶ G.toFunctor
isMonoidal : NatTrans.IsMonoidal hom
h : { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom = β.hom
⊢ { hom := hom, isMonoidal := isMonoidal : F.Hom G } = β
have mk : ∀ (hom_1 : F.toFunctor ⟶ G.toFunctor) (isMonoidal_1 : NatTrans.IsMonoidal hom_1)
  (h : { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom = { hom := hom_1, isMonoidal := isMonoidal_1 }.hom),
  { hom := hom, isMonoidal := isMonoidal : F.Hom G } = { hom := hom_1, isMonoidal := isMonoidal_1 }
Tactic: cases β
Cleared hypotheses: β, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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 G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
hom : F.toFunctor ⟶ G.toFunctor
isMonoidal : NatTrans.IsMonoidal hom
hom_1 : F.toFunctor ⟶ G.toFunctor
isMonoidal_1 : NatTrans.IsMonoidal hom_1
h : { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom = { hom := hom_1, isMonoidal := isMonoidal_1 }.hom
⊢ { hom := hom, isMonoidal := isMonoidal : F.Hom G } = { hom := hom_1, isMonoidal := isMonoidal_1 }
have mk : ∀ (isMonoidal_2 : NatTrans.IsMonoidal { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom),
  { hom := hom, isMonoidal := isMonoidal : F.Hom G } =
    { hom := { hom := hom, isMonoidal := isMonoidal }.hom, isMonoidal := isMonoidal_2 }
Tactic: subst h
Cleared hypotheses: hom_1, isMonoidal_1, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε F.toFunctor ≫ Iso.hom (e (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (ε G.toFunctor)
tensor :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F.toFunctor X Y ≫ Iso.hom (e (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y)
⊢ NatTrans.IsMonoidal (NatIso.ofComponents e ⋯).hom
have unit₁ : autoParam
  (Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε F.toFunctor ≫ (NatIso.ofComponents e sorry).hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε G.toFunctor))
  NatTrans.IsMonoidal.unit._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε F.toFunctor ≫ Iso.hom (e (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (ε G.toFunctor)
tensor :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F.toFunctor X Y ≫ Iso.hom (e (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y)
unit₁ :
  autoParam
    (Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (ε F.toFunctor ≫ (NatIso.ofComponents e ⋯).hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε G.toFunctor))
    NatTrans.IsMonoidal.unit._autoParam
⊢ NatTrans.IsMonoidal (NatIso.ofComponents e ⋯).hom
have tensor₁ : autoParam
  (∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F.toFunctor X Y ≫ (NatIso.ofComponents e sorry).hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (((NatIso.ofComponents e sorry).hom.app X ⊗ₘ (NatIso.ofComponents e sorry).hom.app Y) ≫ μ G.toFunctor X Y))
  NatTrans.IsMonoidal.tensor._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
e : F ≅ G
this : G.Monoidal := transport e
⊢ NatTrans.IsMonoidal e.hom
have refine : ∀ (X Y : C),
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.hom.app X ⊗ₘ e.hom.app Y) ≫ LaxMonoidal.μ G X Y)
Tactic: refine ⟨rfl, fun X Y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X))
    (Iso.hom (α_ X Y Z) ≫
      CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
        (Iso.hom (coprod.braiding X (tensorObj.{v, u} (𝒞 := inst) Y Z)) :
          tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
            tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
        (Iso.hom (α_ Y Z X) :
          tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X ⟶
            tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X)))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y X) Z)
      (Iso.hom (coprod.braiding X Y) ▷ Z :
        tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
          tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y X) Z)
      (Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (coprod.braiding X Z) :
        tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y X) Z ⟶
          tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X)))
have dsimp : Eq.{v + 1} (α := coprod.{v, u} (coprod.{v, u} X Y) Z ⟶ coprod.{v, u} Y (coprod.{v, u} Z X))
  (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} Y Z))
    (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} Y Z) X) (coprod.desc coprod.inr coprod.inl)
      (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))))
  (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} Y X) Z) (coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Z))
    (CategoryStruct.comp (Y := coprod.{v, u} Y (coprod.{v, u} X Z))
      (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))
      (coprod.map (𝟙 Y) (coprod.desc coprod.inr coprod.inl))))
Tactic: dsimp [monoidalOfHasFiniteCoproducts.associator_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z X) Y)
    (Iso.inv (α_ X Y Z) ≫
      CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) X Y))
        (Iso.hom (coprod.braiding (tensorObj.{v, u} (𝒞 := inst) X Y) Z) :
          tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
            tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) X Y))
        (Iso.inv (α_ Z X Y) :
          tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) X Y) ⟶
            tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z X) Y))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Z Y))
      (X ◁ Iso.hom (coprod.braiding Y Z) :
        tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
          tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Z Y))
      (Iso.inv (α_ X Z Y) ≫ Iso.hom (coprod.braiding X Z) ▷ Y :
        tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Z Y) ⟶
          tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z X) Y))
have dsimp : Eq.{v + 1} (α := coprod.{v, u} X (coprod.{v, u} Y Z) ⟶ coprod.{v, u} (coprod.{v, u} Z X) Y)
  (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X Y) Z)
    (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))
    (CategoryStruct.comp (Y := coprod.{v, u} Z (coprod.{v, u} X Y)) (coprod.desc coprod.inr coprod.inl)
      (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))))
  (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} Z Y)) (coprod.map (𝟙 X) (coprod.desc coprod.inr coprod.inl))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X Z) Y)
      (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))
      (coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Y))))
Tactic: dsimp [monoidalOfHasFiniteCoproducts.associator_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : C
inst_2 : MonObj M
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))
        { unmop := M : Cᴹᵒᵖ } ⟶
      { unmop := M })
    (Quiver.Hom.mop MonObj.one ▷ { unmop := M } ≫ Quiver.Hom.mop MonObj.mul) (Iso.hom (λ_ { unmop := M }))
have apply : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
      (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))
        { unmop := M : Cᴹᵒᵖ }) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
    (Quiver.Hom.mop MonObj.one ▷ { unmop := M } ≫ Quiver.Hom.mop MonObj.mul))
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (Iso.hom (λ_ { unmop := M })))
Tactic: apply mopEquiv C |>.fullyFaithfulInverse.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : C
inst_2 : MonObj M
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ }
        (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) ⟶
      { unmop := M })
    ({ unmop := M } ◁ Quiver.Hom.mop MonObj.one ≫ Quiver.Hom.mop MonObj.mul) (Iso.hom (ρ_ { unmop := M }))
have apply : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
      (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ }
        (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
    ({ unmop := M } ◁ Quiver.Hom.mop MonObj.one ≫ Quiver.Hom.mop MonObj.mul))
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (Iso.hom (ρ_ { unmop := M })))
Tactic: apply mopEquiv C |>.fullyFaithfulInverse.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : C
inst_2 : MonObj M
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory)
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ })
        { unmop := M : Cᴹᵒᵖ } ⟶
      { unmop := M })
    (Quiver.Hom.mop MonObj.mul ▷ { unmop := M : Cᴹᵒᵖ } ≫ Quiver.Hom.mop MonObj.mul)
    (Iso.hom (α_ { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ }) ≫
      { unmop := M : Cᴹᵒᵖ } ◁ Quiver.Hom.mop MonObj.mul ≫ Quiver.Hom.mop MonObj.mul)
have apply : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
      (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory)
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ })
        { unmop := M : Cᴹᵒᵖ }) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
    (Quiver.Hom.mop MonObj.mul ▷ { unmop := M : Cᴹᵒᵖ } ≫ Quiver.Hom.mop MonObj.mul))
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
    (Iso.hom (α_ { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ }) ≫
      { unmop := M : Cᴹᵒᵖ } ◁ Quiver.Hom.mop MonObj.mul ≫ Quiver.Hom.mop MonObj.mul))
Tactic: apply mopEquiv C |>.fullyFaithfulInverse.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : C
inst_2 : MonObj M
N : C
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
⊢ Eq (α := tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory) ⟶ { unmop := N : Cᴹᵒᵖ }) (MonObj.one ≫ f.mop)
    MonObj.one
have apply : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
      (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := N : Cᴹᵒᵖ })
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (MonObj.one ≫ f.mop))
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) MonObj.one)
Tactic: apply mopEquiv C |>.fullyFaithfulInverse.map_injective