awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
rw :
  Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
    (f.f ≫ (adj.homEquiv A₂.a A₂.a : (a : F.obj A₂.a ⟶ A₂.a) → A₂.a ⟶ G.obj A₂.a) A₂.str : A₁.a ⟶ G.obj A₂.a)
rw₁ :
  Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (F.map f.f ≫ A₂.str) : A₁.a ⟶ G.obj A₂.a)
rw₂ rw₃ :
  Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
⊢ Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₁.a : (a : F.obj A₁.a ⟶ A₁.a) → A₁.a ⟶ G.obj A₁.a) A₁.str ≫ G.map f.f : A₁.a ⟶ G.obj A₂.a)
    (f.f ≫ (adj.homEquiv A₂.a A₂.a : (a : F.obj A₂.a ⟶ A₂.a) → A₂.a ⟶ G.obj A₂.a) A₂.str : A₁.a ⟶ G.obj A₂.a)

Tactic:
rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]

Premises used: CategoryTheory.Endofunctor.Algebra.Hom.h, CategoryTheory.Adjunction.homEquiv_naturality_right, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
rw :
  Eq (α := F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
      F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₁.V) : (a : V₁.V ⟶ G.obj V₁.V) → F.obj V₁.V ⟶ V₁.V) V₁.str ≫ f.f :
      F.obj V₁.V ⟶ V₂.V)
rw₁ :
  Eq (α := F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
      F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (V₁.str ≫ G.map f.f) :
      F.obj V₁.V ⟶ V₂.V)
rw₂ rw₃ :
  Eq (α := F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
      F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
      F.obj V₁.V ⟶ V₂.V)
⊢ Eq (α := F.obj V₁.V ⟶ V₂.V)
    (F.map f.f ≫ (Equiv.symm (adj.homEquiv V₂.V V₂.V) : (a : V₂.V ⟶ G.obj V₂.V) → F.obj V₂.V ⟶ V₂.V) V₂.str)
    ((Equiv.symm (adj.homEquiv V₁.V V₁.V) : (a : V₁.V ⟶ G.obj V₁.V) → F.obj V₁.V ⟶ V₁.V) V₁.str ≫ f.f)

Tactic:
rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm,
    f.h]

Premises used: CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_left_symm
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
A : Algebra F
w :
  autoParam
    (((Algebra.toCoalgebraOf adj).map ((AlgCoalgEquiv.unitIso adj).hom.app A) ≫
          (AlgCoalgEquiv.counitIso adj).hom.app ((Algebra.toCoalgebraOf adj).obj A)).f =
      Coalgebra.Hom.f (𝟙 ((Algebra.toCoalgebraOf adj).obj A)))
    Coalgebra.ext._auto_1
⊢ (Algebra.toCoalgebraOf adj).map ((AlgCoalgEquiv.unitIso adj).hom.app A) ≫
      (AlgCoalgEquiv.counitIso adj).hom.app ((Algebra.toCoalgebraOf adj).obj A) =
    𝟙 ((Algebra.toCoalgebraOf adj).obj A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
A : Algebra F
⊢ autoParam
    (((Algebra.toCoalgebraOf adj).map ((AlgCoalgEquiv.unitIso adj).hom.app A) ≫
          (AlgCoalgEquiv.counitIso adj).hom.app ((Algebra.toCoalgebraOf adj).obj A)).f =
      Coalgebra.Hom.f (𝟙 ((Algebra.toCoalgebraOf adj).obj A)))
    Coalgebra.ext._auto_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X : C
⊢ Eq.{v + 1} (α := End X) 1 (𝟙 X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X : C
xs ys : End X
⊢ xs * ys = ys ≫ xs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X : C
x y : End X
h : x.asHom = y.asHom
⊢ x = y

Tactic:
h

Premises used: CategoryTheory.End
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
r : End Y
f : X ⟶ Y
⊢ r • f = f ≫ r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
r : (End X)ᵐᵒᵖ
f : X ⟶ Y
⊢ r • f = MulOpposite.unop r ≫ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ f * inv f = 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ inv f * f = 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X : C
φ₁ φ₂ : Aut X
h : φ₁.hom = φ₂.hom
⊢ φ₁ = φ₂

Tactic:
Iso.ext h

Premises used: CategoryTheory.Aut, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f g : Aut X
⊢ f * g = g ≪≫ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : Aut X
⊢ f⁻¹ = Iso.symm f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f g : (End X)ˣ
mk :
  ∀ (val inv : End X) (val_inv : val * inv = 1) (inv_val : inv * val = 1),
    { hom := (↑({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } * g) : End X),
        inv := ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } * g).inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ : X ≅ X } =
      { hom := (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } : End X),
          inv := { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ }.inv, hom_inv_id := ⋯,
          inv_hom_id := ⋯ : X ≅ X } *
        { hom := (↑g : End X), inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X }
⊢ { hom := (↑(f * g) : End X), inv := (f * g).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X } =
    { hom := (↑f : End X), inv := f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X } *
      { hom := (↑g : End X), inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X }

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X : C
g : (End X)ˣ
val inv : End X
val_inv : val * inv = 1
inv_val : inv * val = 1
mk :
  ∀ (val_1 inv_1 : End X) (val_inv_1 : val_1 * inv_1 = 1) (inv_val_1 : inv_1 * val_1 = 1),
    {
        hom :=
          (↑({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } *
                { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }) :
            End X),
        inv :=
          ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } *
              { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }).inv,
        hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X } =
      { hom := (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } : End X),
          inv := { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ }.inv, hom_inv_id := ⋯,
          inv_hom_id := ⋯ : X ≅ X } *
        { hom := (↑{ val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ } : End X),
          inv := { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }.inv,
          hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X }
⊢ { hom := (↑({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } * g) : End X),
      inv := ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } * g).inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ : X ≅ X } =
    { hom := (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } : End X),
        inv := { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ : X ≅ X } *
      { hom := (↑g : End X), inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X }

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X : C
val inv : End X
val_inv : val * inv = 1
inv_val : inv * val = 1
val_1 inv_1 : End X
val_inv_1 : val_1 * inv_1 = 1
inv_val_1 : inv_1 * val_1 = 1
⊢ {
      hom :=
        (↑({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } *
              { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }) :
          End X),
      inv :=
        ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } *
            { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }).inv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X } =
    { hom := (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } : End X),
        inv := { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ : X ≅ X } *
      { hom := (↑{ val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ } : End X),
        inv := { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }.inv,
        hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Endomorphism
Goal:
C : Type u
inst : Category.{v, u} C
X_1 X Y : C
h : X ≅ Y
⊢ ∀ (x y : Aut X),
    { hom := h.inv ≫ (x * y).hom ≫ h.hom, inv := h.inv ≫ (x * y).inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ :
        Y ≅ Y } =
      { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ : Y ≅ Y } *
        { hom := h.inv ≫ y.hom ≫ h.hom, inv := h.inv ≫ y.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ : Y ≅ Y }

Tactic:
simp [Aut_mul_def]

Premises used: CategoryTheory.Aut.Aut_mul_def
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
X Y : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
    (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ≫ eComp V X X Y)
    (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
EnrichedCategory.id_comp X Y

Premises used: CategoryTheory.EnrichedCategory.id_comp, CategoryTheory.eComp, CategoryTheory.eId
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
X Y : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
    (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y ≫ eComp V X Y Y)
    (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
EnrichedCategory.comp_id X Y

Premises used: CategoryTheory.EnrichedCategory.comp_id, CategoryTheory.eComp, CategoryTheory.eId
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W X Y Z : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V)
      (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
        (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
    (Iso.inv
        (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
      eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
    (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X ◁ eComp V X Y Z ≫ eComp V W X Z)

Tactic:
EnrichedCategory.assoc W X Y Z

Premises used: CategoryTheory.eComp, CategoryTheory.EnrichedCategory.assoc
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W X Y Z : C
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V)
      (tensorObj.{w, v} (𝒞 := inst)
        (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
    (Iso.hom
        (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
      Iso.inv
          (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
            (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
            (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
        eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
    (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
rw₁ rw₂ :
  Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V)
      (tensorObj.{w, v} (𝒞 := inst)
        (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
    (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
    (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V)
      (tensorObj.{w, v} (𝒞 := inst)
        (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
    (Iso.hom
        (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
      @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X ◁ eComp V X Y Z ≫ eComp V W X Z)
    (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)

Tactic:
rw [← e_assoc V W X Y Z, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.e_assoc
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
simp :
  F.map (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))) ≫
      F.map (eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ≫ F.map (eComp V X X Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
⊢ CategoryStruct.comp (Y :=
      tensorObj.{w', v'} (𝒞 := inst_3) (tensorUnit.{w', v'} W (𝒞 := inst_3))
        (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)))
      (Iso.inv (λ_ (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))))
      ((ε F ≫ F.map (eId V X)) ▷ F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ≫
        μ F (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X X)
            (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ≫
          F.map (eComp V X X Y)) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
simp only [comp_whiskerRight, Category.assoc, Functor.LaxMonoidal.μ_natural_left_assoc,
      Functor.LaxMonoidal.left_unitality_inv_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc, CategoryTheory.Functor.LaxMonoidal.left_unitality_inv_assoc
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
simp_rw :
  F.map
      (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
        eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ≫ eComp V X X Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
⊢ F.map (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))) ≫
      F.map (eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ≫ F.map (eComp V X X Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
simp_rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
F.map_id _

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
h :
  Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
    (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ≫ eComp V X X Y)
    (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
⊢ F.map
      (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
        eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ≫ eComp V X X Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
convert! F.map_id _

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
    (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ≫ eComp V X X Y)
    (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
simp :
  F.map (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))) ≫
      F.map (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y) ≫ F.map (eComp V X Y Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
⊢ CategoryStruct.comp (Y :=
      tensorObj.{w', v'} (𝒞 := inst_3) (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
        (tensorUnit.{w', v'} W (𝒞 := inst_3)))
      (Iso.inv (ρ_ (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))))
      (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ◁ (ε F ≫ F.map (eId V Y)) ≫
        μ F (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
            (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Y) ≫
          F.map (eComp V X Y Y)) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc,
      Functor.LaxMonoidal.μ_natural_right_assoc,
      Functor.LaxMonoidal.right_unitality_inv_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Functor.LaxMonoidal.μ_natural_right_assoc, CategoryTheory.Functor.LaxMonoidal.right_unitality_inv_assoc
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
simp_rw :
  F.map
      (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
        @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y ≫ eComp V X Y Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
⊢ F.map (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))) ≫
      F.map (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y) ≫ F.map (eComp V X Y Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
simp_rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
h :
  Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
    (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y ≫ eComp V X Y Y)
    (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
⊢ F.map
      (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
        @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y ≫ eComp V X Y Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))

Tactic:
convert! F.map_id _

Premises used: CategoryTheory.Functor.map_id