mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
⊢ (fun g ↦ { app := fun j ↦ (eHomEquiv V).symm (g ≫ end_.π (diagram V F₁ F₂) j), naturality := ⋯ })
      ((fun τ ↦ end_.lift (fun j ↦ (eHomEquiv V) (τ.app j)) ⋯) τ) =
    τ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
g : 𝟙_ V ⟶ enrichedHom V F₁ F₂
⊢ (fun τ ↦ end_.lift (fun j ↦ (eHomEquiv V) (τ.app j)) ⋯)
      ((fun g ↦ { app := fun j ↦ (eHomEquiv V).symm (g ≫ end_.π (diagram V F₁ F₂) j), naturality := ⋯ }) g) =
    g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
j : J
⊢ (homEquiv V) τ ≫ enrichedHomπ V F₁ F₂ j = (eHomEquiv V) (τ.app j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₁
j : J
⊢ enrichedId V F₁ ≫ end_.π (diagram V F₁ F₁) j = eId V (F₁.obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ Z✝ : C ≌ D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mkHom ((conjugateEquiv Z✝.toAdjunction X✝.toAdjunction) (asNatTrans (x✝¹ ≫ x✝)))).op.unop =
    ((mkHom ((conjugateEquiv Y✝.toAdjunction X✝.toAdjunction) (asNatTrans x✝¹))).op ≫
        (mkHom ((conjugateEquiv Z✝.toAdjunction Y✝.toAdjunction) (asNatTrans x✝))).op).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ Z✝ : D ≌ C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mkHom ((conjugateEquiv X✝.symm.toAdjunction Z✝.symm.toAdjunction).invFun (asNatTrans (x✝¹ ≫ x✝)))).op.unop =
    ((mkHom ((conjugateEquiv X✝.symm.toAdjunction Y✝.symm.toAdjunction).invFun (asNatTrans x✝¹))).op ≫
        (mkHom ((conjugateEquiv Y✝.symm.toAdjunction Z✝.symm.toAdjunction).invFun (asNatTrans x✝))).op).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ : C ≌ D
x✝ : X✝ ⟶ Y✝
⊢ (𝟭 (C ≌ D)).map x✝ ≫ (Iso.refl ((𝟭 (C ≌ D)).obj Y✝)).hom =
    (Iso.refl ((𝟭 (C ≌ D)).obj X✝)).hom ≫ (symmEquivFunctor C D ⋙ symmEquivInverse C D).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ : (D ≌ C)ᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (symmEquivInverse C D ⋙ symmEquivFunctor C D).map x✝ ≫ (Iso.refl (Opposite.unop Y✝)).op.hom =
    (Iso.refl (Opposite.unop X✝)).op.hom ≫ (𝟭 (D ≌ C)ᵒᵖ).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : C ≌ D
⊢ (symmEquivFunctor C D).map ((ofComponents (fun e ↦ Iso.refl ((𝟭 (C ≌ D)).obj e)) ⋯).hom.app X) ≫
      (ofComponents (fun e ↦ (Iso.refl (Opposite.unop e)).op) ⋯).hom.app ((symmEquivFunctor C D).obj X) =
    𝟙 ((symmEquivFunctor C D).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
e f : C ≌ D
α : e ≅ f
⊢ ((inverseFunctor C D).mapIso α.symm).unop = ((functorFunctor C D).mapIso α).isoInverseOfIsoFunctor

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X✝ Y✝ Z✝ : (C ≌ D)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ mkHom
      ((whiskeringLeft D C E).map
        ((conjugateEquiv (Opposite.unop X✝).toAdjunction (Opposite.unop Z✝).toAdjunction)
          (asNatTrans (x✝¹ ≫ x✝).unop))) =
    mkHom
        ((whiskeringLeft D C E).map
          ((conjugateEquiv (Opposite.unop X✝).toAdjunction (Opposite.unop Y✝).toAdjunction) (asNatTrans x✝¹.unop))) ≫
      mkHom
        ((whiskeringLeft D C E).map
          ((conjugateEquiv (Opposite.unop Y✝).toAdjunction (Opposite.unop Z✝).toAdjunction) (asNatTrans x✝.unop)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝¹ x✝ : Cᵒᵖ
⊢ (λ_ (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (id (Opposite.unop x✝¹) ▷ Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ≫
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝¹) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝¹) =
    𝟙 (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
R✝ X✝ : C
p₁✝ p₂✝ : R✝ ⟶ X✝
X Y : C
f : X ⟶ Y
R : C
p₁ p₂ : R ⟶ X
t : PullbackCone p₂ p₁
ht : IsLimit t
h : IsKernelPair f p₁ p₂
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
R✝ X✝ : C
p₁✝ p₂✝ : R✝ ⟶ X✝
X Y : C
f : X ⟶ Y
R : C
p₁ p₂ : R ⟶ X
t : PullbackCone p₂ p₁
ht : IsLimit t
h : IsKernelPair f p₁ p₂
⊢ (t.fst ≫ p₁) ≫ f = (t.snd ≫ p₂) ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
R X : C
p₁ p₂ : R ⟶ X
e : ReflexiveRelation p₁ p₂
F : C ⥤ D
inst✝ : JointlyMono₂ (F.map p₁) (F.map p₂)
⊢ F.map e.r ≫ F.map p₁ = 𝟙 (F.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
R X : C
p₁ p₂ : R ⟶ X
e : ReflexiveRelation p₁ p₂
F : C ⥤ D
inst✝ : JointlyMono₂ (F.map p₁) (F.map p₂)
⊢ F.map e.r ≫ F.map p₂ = 𝟙 (F.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
R X : C
p₁ p₂ : R ⟶ X
e : SymmetricRelation p₁ p₂
F : C ⥤ D
inst✝ : JointlyMono₂ (F.map p₁) (F.map p₂)
⊢ F.map e.s ≫ F.map p₁ = F.map p₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
R X : C
p₁ p₂ : R ⟶ X
e : SymmetricRelation p₁ p₂
F : C ⥤ D
inst✝ : JointlyMono₂ (F.map p₁) (F.map p₂)
⊢ F.map e.s ≫ F.map p₂ = F.map p₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝¹ x✝ : Cᵒᵖ
⊢ (ρ_ (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁ id (Opposite.unop x✝) ≫
        (β_ (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝) (Opposite.unop x✝¹) =
    𝟙 (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X✝ : Type w
φ✝ : X✝ → X✝ → Prop
X : Type w
φ : X → X → Prop
hφ : IsTrans X φ
x✝ : (Types.pullbackCone (p₂OfRel φ) (p₁OfRel φ)).pt
x₁ snd✝ : X
h : Function.uncurry φ (x₁, snd✝)
fst✝ x₂' : X
h' : Function.uncurry φ (fst✝, x₂')
h₁₂ :
  (ConcreteCategory.hom (p₂OfRel φ)) (⟨(x₁, snd✝), h⟩, ⟨(fst✝, x₂'), h'⟩).1 =
    (ConcreteCategory.hom (p₁OfRel φ)) (⟨(x₁, snd✝), h⟩, ⟨(fst✝, x₂'), h'⟩).2
⊢ ROfRel φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X R : Type w
p₁ p₂ : R ⟶ X
e : ReflexiveRelation p₁ p₂
x : X
⊢ (ConcreteCategory.hom p₂) ((ConcreteCategory.hom e.r) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X R : Type w
p₁ p₂ : R ⟶ X
e : SymmetricRelation p₁ p₂
x₁ x₂ : X
x✝ : Rel.ofPair p₁ p₂ x₁ x₂
r : R
hr₁ : (ConcreteCategory.hom p₁) r = x₁
hr₂ : (ConcreteCategory.hom p₂) r = x₂
⊢ (ConcreteCategory.hom p₁) ((ConcreteCategory.hom e.s) r) = x₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X R : Type w
p₁ p₂ : R ⟶ X
e : SymmetricRelation p₁ p₂
x₁ x₂ : X
x✝ : Rel.ofPair p₁ p₂ x₁ x₂
r : R
hr₁ : (ConcreteCategory.hom p₁) r = x₁
hr₂ : (ConcreteCategory.hom p₂) r = x₂
⊢ (ConcreteCategory.hom p₂) ((ConcreteCategory.hom e.s) r) = x₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X₁ Y₁ X₂ Y₂ : LocalizedMonoidal L W ε} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ₘ g = f ▷ X₂ ≫ Y₁ ◁ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X₁ Y₁ X₂ Y₂ : LocalizedMonoidal L W ε} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ₘ g = f ▷ X₂ ≫ Y₁ ◁ g

Tactic:
by intros; simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ (X₁ X₂ : LocalizedMonoidal L W ε), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
by intros; simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ (X Y : LocalizedMonoidal L W ε), X ◁ 𝟙 Y = 𝟙 (X ⊗ Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ (X Y : LocalizedMonoidal L W ε), 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X R : Type w
p₁ p₂ : R ⟶ X
e : TransitiveRelation p₁ p₂
x₁ x₂ x₃ : X
⊢ Rel.ofPair p₁ p₂ x₁ x₂ → Rel.ofPair p₁ p₂ x₂ x₃ → Rel.ofPair p₁ p₂ x₁ x₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X Y : LocalizedMonoidal L W ε} (f : X ⟶ Y), 𝟙_ (LocalizedMonoidal L W ε) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X Y : LocalizedMonoidal L W ε} (f : X ⟶ Y), 𝟙_ (LocalizedMonoidal L W ε) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
by intros; simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y Z : C
⊢ (μ L W ε X Y).hom ▷ (toMonoidalCategory L W ε).obj Z ≫
      (μ L W ε (X ⊗ Y) Z).hom ≫ (toMonoidalCategory L W ε).map (α_ X Y Z).hom =
    (α_ ((toMonoidalCategory L W ε).obj X) ((toMonoidalCategory L W ε).obj Y) ((toMonoidalCategory L W ε).obj Z)).hom ≫
      (toMonoidalCategory L W ε).obj X ◁ (μ L W ε Y Z).hom ≫ (μ L W ε X (Y ⊗ Z)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y Z : C
⊢ (α_ (L'.obj X) (L'.obj Y) (L'.obj Z)).hom =
    Functor.LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫
      Functor.LaxMonoidal.μ L' (X ⊗ Y) Z ≫
        L'.map (α_ X Y Z).hom ≫ Functor.OplaxMonoidal.δ L' X (Y ⊗ Z) ≫ L'.obj X ◁ Functor.OplaxMonoidal.δ L' Y Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝³ x✝² x✝¹ x✝ : Cᵒᵖ
⊢ (α_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (((β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)).hom ≫
            comp (Opposite.unop x✝¹) (Opposite.unop x✝²) (Opposite.unop x✝³)) ▷
          Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ≫
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝³) =
    (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁
        ((β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²)) ≫
      (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝²)).hom ≫
        comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y Z : C
⊢ (α_ (L'.obj X) (L'.obj Y) (L'.obj Z)).inv =
    L'.obj X ◁ Functor.LaxMonoidal.μ L' Y Z ≫
      Functor.LaxMonoidal.μ L' X (Y ⊗ Z) ≫
        L'.map (α_ X Y Z).inv ≫ Functor.OplaxMonoidal.δ L' (X ⊗ Y) Z ≫ Functor.OplaxMonoidal.δ L' X Y ▷ L'.obj Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R : 𝒮
a : 𝒳
ha : p.obj a = R
⊢ p.IsHomLift (𝟙 R) (𝟙 a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ z ⟶[V] y
g : w ⟶ y ⟶[V] x
⊢ (f ⊗ₘ g) ≫ eComp V z y x = (β_ v w).hom ≫ (g ⊗ₘ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.obj a = R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.obj b = S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : ForgetEnrichment V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
⊢ (f ≫ g).op = f.op ≫ g.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
f : p.obj a ⟶ p.obj b
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ f = p.map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom hb
⊢ p.IsHomLift f φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
⊢ f = p.map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ = eqToHom ha ≫ f ≫ eqToHom ⋯
⊢ p.IsHomLift f φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
⊢ f = p.map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ ≫ eqToHom hb = eqToHom ha ≫ f
⊢ p.IsHomLift f φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
⊢ (f ≫ g).unop = f.unop ≫ g.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
inst✝³ : BraidedCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u
inst✝¹ : Category.{v, u} D
inst✝ : EnrichedOrdinaryCategory V D
X✝ Y✝ Z✝ : Dᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Quiver.Hom.opEquiv.symm.trans homEquiv) (f ≫ g) =
    (λ_ (𝟙_ V)).inv ≫
      ((Quiver.Hom.opEquiv.symm.trans homEquiv) f ⊗ₘ (Quiver.Hom.opEquiv.symm.trans homEquiv) g) ≫ eComp V X✝ Y✝ Z✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.IsHomLift (f ≫ g) (φ ≫ ψ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
S T : 𝒮
f : S ⟶ T
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
by

Goal state after: