awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
J' : Type u₂
inst_1 : Category.{v₂, u₂} J'
V : Type u'
inst_2 : Category.{v', u'} V
inst_3 : MonoidalCategory.{v', u'} V
C : Type u
inst_4 : Category.{v, u} C
inst_5 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
inst_6 : HasConicalLimits.{v', v, u, u'} V C
⊢ HasLimits.{v, u} C

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
inst_4 : HasConicalProducts.{w, v', v, u, u'} V C
⊢ HasProducts.{w, v, u} C

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasConicalPullback.{v', v, u, u'} V f g
⊢ HasPullback f g

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
inst_4 : HasConicalPullbacks.{v', v, u, u'} V C
⊢ HasPullbacks.{v, u} C

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
inst_4 : HasConicalTerminal.{u', v', u, v} V C
⊢ HasTerminal.{v, u} C

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
inst_4 : HasConicalProducts.{w, v', v, u, u'} V C
⊢ HasConicalTerminal.{u', v', u, v} V C

Tactic:
HasConicalLimitsOfShape.of_equiv V C emptyEquivalence.functor

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Enriched.HasConicalLimitsOfShape.of_equiv, CategoryTheory.emptyEquivalence
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 : Cᵒᵖ
simp :
  Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (ρ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁ id (Opposite.unop x) ≫
        comp (Opposite.unop x_1) (Opposite.unop x) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (λ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      id (Opposite.unop x) ▷ @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ≫
        Iso.hom
            (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x) (Opposite.unop x))
              (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
          comp (Opposite.unop x_1) (Opposite.unop x) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))

Tactic:
simp only [braiding_naturality_left_assoc, braiding_tensorUnit_left,
      Category.assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.braiding_tensorUnit_left, CategoryTheory.BraidedCategory.braiding_naturality_left_assoc
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (ρ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁ id (Opposite.unop x) ≫
        comp (Opposite.unop x_1) (Opposite.unop x) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))

Tactic:
EnrichedCategory.comp_id _ _

Premises used: CategoryTheory.EnrichedCategory.comp_id
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (ρ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁ id (Opposite.unop x) ≫
        comp (Opposite.unop x_1) (Opposite.unop x) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))

Tactic:
exact EnrichedCategory.comp_id _ _

Premises used: CategoryTheory.EnrichedCategory.comp_id
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 : Cᵒᵖ
simp :
  Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (λ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      id (Opposite.unop x_1) ▷ @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ≫
        comp (Opposite.unop x_1) (Opposite.unop x_1) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (ρ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ◁ id (Opposite.unop x_1) ≫
        Iso.hom
            (β_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
              (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x_1))) ≫
          comp (Opposite.unop x_1) (Opposite.unop x_1) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))

Tactic:
simp only [braiding_naturality_right_assoc, braiding_tensorUnit_right,
      Category.assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.braiding_tensorUnit_right, CategoryTheory.BraidedCategory.braiding_naturality_right_assoc
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (λ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      id (Opposite.unop x_1) ▷ @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ≫
        comp (Opposite.unop x_1) (Opposite.unop x_1) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))

Tactic:
EnrichedCategory.id_comp _ _

Premises used: CategoryTheory.EnrichedCategory.id_comp
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x x_1 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V) (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))
      (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))
    (Iso.inv (λ_ (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x))) ≫
      id (Opposite.unop x_1) ▷ @Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x) ≫
        comp (Opposite.unop x_1) (Opposite.unop x_1) (Opposite.unop x))
    (𝟙 (@Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x_1) (Opposite.unop x)))

Tactic:
exact EnrichedCategory.id_comp _ _

Premises used: CategoryTheory.EnrichedCategory.id_comp
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := V)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ z y)
        (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ y x))
      (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ z x))
    (eComp V z y x)
    (Iso.hom
        (β_ (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop y) (Opposite.unop z))
          (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x) (Opposite.unop y))) ≫
      eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z))

Tactic:
rfl

Premises used: CategoryTheory.eComp, rfl
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ z y
g : w ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ y x
rw :
  (f ⊗ₘ g) ≫
      Iso.hom
          (β_ (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop y) (Opposite.unop z))
            (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x) (Opposite.unop y))) ≫
        eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z) =
    Iso.hom (β_ v w) ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)
⊢ (f ⊗ₘ g) ≫ eComp V z y x = Iso.hom (β_ v w) ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)

Tactic:
rw [eComp_op_eq]

Premises used: CategoryTheory.eComp_op_eq
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ z y
g : w ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ y x
⊢ (f ⊗ₘ g) ≫
      Iso.hom
          (β_ (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop y) (Opposite.unop z))
            (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x) (Opposite.unop y))) ≫
        eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z) =
    Iso.hom (β_ v w) ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)

Tactic:
braiding_naturality_assoc f g _

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_assoc
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ z y
g : w ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ y x
⊢ (f ⊗ₘ g) ≫
      Iso.hom
          (β_ (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop y) (Opposite.unop z))
            (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ (Opposite.unop x) (Opposite.unop y))) ≫
        eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z) =
    Iso.hom (β_ v w) ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)

Tactic:
exact braiding_naturality_assoc f g _

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_assoc
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : ForgetEnrichment.{v₁, u₁, u} V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
⊢ f ≫ g = homTo V (f ≫ g)

Tactic:
have : (f ≫ g) = homTo V (f ≫ g) := rfl
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : ForgetEnrichment.{v₁, u₁, u} V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
rw :
  ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫ (homTo V g ⊗ₘ homTo V f)) ≫
        eComp V (Opposite.unop («to» V z)) (Opposite.unop («to» V y)) (Opposite.unop («to» V x))).op =
    f.op ≫ g.op
⊢ (f ≫ g).op = f.op ≫ g.op

Tactic:
rw [this, ForgetEnrichment.homTo_comp, Category.assoc, tensorHom_eComp_op_eq,
      leftUnitor_inv_braiding_assoc, ← unitors_inv_equal, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.leftUnitor_inv_braiding_assoc, CategoryTheory.ForgetEnrichment.homTo_comp, CategoryTheory.tensorHom_eComp_op_eq, CategoryTheory.MonoidalCategory.unitors_inv_equal
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : ForgetEnrichment.{v₁, u₁, u} V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
⊢ ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫ (homTo V g ⊗ₘ homTo V f)) ≫
        eComp V (Opposite.unop («to» V z)) (Opposite.unop («to» V y)) (Opposite.unop («to» V x))).op =
    f.op ≫ g.op

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
⊢ g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)

Tactic:
have : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop) := rfl
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
rw :
  Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop
⊢ g.unop ≫ f.unop = f.unop ≫ g.unop

Tactic:
rw [this, ForgetEnrichment.homTo_comp, Category.assoc, unitors_inv_equal,
      ← leftUnitor_inv_braiding_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.leftUnitor_inv_braiding_assoc, CategoryTheory.ForgetEnrichment.homTo_comp, CategoryTheory.MonoidalCategory.unitors_inv_equal
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z

Tactic:
have : (β_ _ _).hom ≫ (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
      eComp V («to» V z.unop) («to» V y.unop) («to» V x.unop) =
      ((homTo V f.unop) ⊗ₘ (homTo V g.unop)) ≫ eComp V x y z := (tensorHom_eComp_op_eq V _ _).symm
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this_1 : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
rw :
  Eq (α := x ⟶ z)
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫ (homTo V f.unop ⊗ₘ homTo V g.unop)) ≫ eComp V x y z :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ («to» V (Opposite.unop z)) («to» V (Opposite.unop x)))
    (f.unop ≫ g.unop : x ⟶ z)
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop

Tactic:
rw [this, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
x y z : (ForgetEnrichment.{v₁, u₁, u} V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this_1 : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  Iso.hom (β_ (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
⊢ Eq (α := x ⟶ z)
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫ (homTo V f.unop ⊗ₘ homTo V g.unop)) ≫ eComp V x y z :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ («to» V (Opposite.unop z)) («to» V (Opposite.unop x)))
    (f.unop ≫ g.unop : x ⟶ z)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
D : Type u
inst_4 : Category.{v, u} D
inst_5 : EnrichedOrdinaryCategory.{v₁, v, u, u₁} V D
X Y Z : Dᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
simp :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
        (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ Y Z)
            (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Y))
          ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g ⊗ₘ
            (Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f)
          (eComp V (Opposite.unop Z) (Opposite.unop Y) (Opposite.unop X))) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
        (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
        (((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f ⊗ₘ
            (Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g) ≫
          eComp V X Y Z) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)

Tactic:
simp only [tensorHom_eComp_op_eq, leftUnitor_inv_braiding_assoc, ← unitors_inv_equal]

Premises used: CategoryTheory.leftUnitor_inv_braiding_assoc, CategoryTheory.tensorHom_eComp_op_eq, CategoryTheory.MonoidalCategory.unitors_inv_equal
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
D : Type u
inst_4 : Category.{v, u} D
inst_5 : EnrichedOrdinaryCategory.{v₁, v, u, u₁} V D
X Y Z : Dᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
        (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ Y Z)
            (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Y))
          ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g ⊗ₘ
            (Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f)
          (eComp V (Opposite.unop Z) (Opposite.unop Y) (Opposite.unop X))) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)

Tactic:
homEquiv_comp g.unop f.unop

Premises used: CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp, Quiver.Hom.unop