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

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X : C
⊢ (eId (Type v) X ≫ ↾fun f ↦ F.map f) = eId (Type v) (F.obj X)

Tactic:
by

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

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
⊢ (eComp (Type v) X Y Z ≫ ↾fun f ↦ F.map f) =
    ((↾fun f ↦ F.map f) ⊗ₘ ↾fun f ↦ F.map f) ≫ eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ range ((A.prod B).ι ≫ snd X Y) ≤ B

Tactic:
by

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

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
⊢ (((Center.ofBraided (Type v)).obj (unop α)).snd.β (X ⟶[Type v] Y)).hom ≫
      (F.map X Y ⊗ₘ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app Y) ≫ eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y) =
    ((↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X) ⊗ₘ G.map X Y) ≫ eComp (Type v) (F.obj X) (G.obj X) (G.obj Y)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ range (A.ι ⊗ₘ B.ι) ≤ A.prod B

Tactic:
by

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

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
⊢ ∀ {X Y : Type vᵒᵖ} (f : X ⟶ Y),
    (enrichedNatTransYoneda F G).map f ≫
        { hom := ↾fun σ ↦ ↾fun x ↦ { app := fun X ↦ (ConcreteCategory.hom (σ.app X)) x, naturality := ⋯ },
            inv := ↾fun σ ↦ { app := fun X ↦ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X, naturality := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom =
      { hom := ↾fun σ ↦ ↾fun x ↦ { app := fun X_1 ↦ (ConcreteCategory.hom (σ.app X_1)) x, naturality := ⋯ },
            inv := ↾fun σ ↦ { app := fun X_1 ↦ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X_1, naturality := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : (X ⊗ Y).obj n
⊢ x ∈ (S.unionProd T).obj n ↔ x.2 ∈ T.obj n ∨ x.1 ∈ S.obj n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ range (X ◁ T.ι) ≤ S.unionProd T

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ range (S.ι ▷ Y) ≤ S.unionProd T

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      (f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (Y.snd.β U).hom) ⊗≫ (X₂.snd.β U).hom ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ (f.f ▷ U ≫ (X₂.snd.β U).hom) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ⊤.prod T ⊓ S.prod ⊤ = S.prod T

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).preimage (β_ Y X).hom = T.unionProd S

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).preimage (β_ X Y).inv = T.unionProd S

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).image (β_ X Y).hom = T.unionProd S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ (f.f ▷ U ≫ (X₂.snd.β U).hom) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    ((α_ X₁.fst Y.fst U).hom ≫
        X₁.fst ◁ (Y.snd.β U).hom ≫ (α_ X₁.fst U Y.fst).inv ≫ (X₁.snd.β U).hom ▷ Y.fst ≫ (α_ U X₁.fst Y.fst).hom) ≫
      U ◁ f.f ▷ Y.fst

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).image (β_ Y X).inv = T.unionProd S

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ range ((S.unionProd T).ι ≫ (β_ X Y).hom) ≤ T.unionProd S

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ range ((T.unionProd S).ι ≫ (β_ Y X).hom) ≤ S.unionProd T

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ f.f ▷ Y.fst ▷ U ≫ ((X₂.tensorObj Y).snd.β U).hom = ((X₁.tensorObj Y).snd.β U).hom ≫ U ◁ f.f ▷ Y.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ Y₁ X₂ Y₂ : Center C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
⊢ (f.f ⊗ₘ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd.β U).hom = ((X₁.tensorObj X₂).snd.β U).hom ≫ U ◁ (f.f ⊗ₘ g.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
U : C
⊢ (α_ X.fst Y.fst Z.fst).hom ▷ U ≫ ((X.tensorObj (Y.tensorObj Z)).snd.β U).hom =
    (((X.tensorObj Y).tensorObj Z).snd.β U).hom ≫ U ◁ (α_ X.fst Y.fst Z.fst).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
U : C
⊢ (λ_ X.fst).hom ▷ U ≫ (X.snd.β U).hom = ((tensorUnit.tensorObj X).snd.β U).hom ≫ U ◁ (λ_ X.fst).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
U : C
⊢ (ρ_ X.fst).hom ▷ U ≫ (X.snd.β U).hom = ((X.tensorObj tensorUnit).snd.β U).hom ≫ U ◁ (ρ_ X.fst).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ∀ {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), tensorHom f g = whiskerRight f X₂ ≫ Y₁.whiskerLeft g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (α_ X Y Z).inv.f = (α_ X.fst Y.fst Z.fst).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W ((e (X✝ ⟶[V] Z✝)) (ForgetEnrichment.homTo V (f ≫ g))) =
    ForgetEnrichment.homOf W ((e (X✝ ⟶[V] Y✝)) (ForgetEnrichment.homTo V f)) ≫
      ForgetEnrichment.homOf W ((e (Y✝ ⟶[V] Z✝)) (ForgetEnrichment.homTo V g))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (λ_ X).inv.f = (λ_ X.fst).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (ρ_ X).inv.f = (ρ_ X.fst).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ B✝ : Center C
f : A✝ ⟶ B✝
i : IsIso ((forget C).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ (X.snd.β Y.fst).hom ▷ U ≫ ((Y ⊗ X).snd.β U).hom = ((X ⊗ Y).snd.β U).hom ≫ U ◁ (X.snd.β Y.fst).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ ForgetEnrichment.homOf V
      ((e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)).symm (ForgetEnrichment.homTo W (𝟙 X))) =
    𝟙 (ForgetEnrichment.of V (ForgetEnrichment.to W X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf V
      ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W (f ≫ g))) =
    ForgetEnrichment.homOf V
        ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f)) ≫
      ForgetEnrichment.homOf V
        ((e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
⊢ ∀ {X Y : TransportEnrichment F (ForgetEnrichment V D)} (f : X ⟶ Y),
    (𝟭 (TransportEnrichment F (ForgetEnrichment V D))).map f ≫
        (Iso.refl ((𝟭 (TransportEnrichment F (ForgetEnrichment V D))).obj Y)).hom =
      (Iso.refl ((𝟭 (TransportEnrichment F (ForgetEnrichment V D))).obj X)).hom ≫
        (forgetEnrichmentEquivFunctor F D e h ⋙ forgetEnrichmentEquivInverse F D e h).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
⊢ (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h).map f ≫
      (Iso.refl ((forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h).obj Y✝)).hom =
    (Iso.refl ((forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h).obj X✝)).hom ≫
      (𝟭 (ForgetEnrichment W (TransportEnrichment F D))).map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
inst✝ : X.IsCoskeletal n
⊢ CostructuredArrow.IsUniversal (rightExtensionInclusion X n)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
⊢ X.IsCoskeletal n ↔ IsIso ((coskAdj n).unit.app X)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
inst✝ : X.IsCoskeletal n
⊢ IsIso ((coskAdj n).unit.app X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : TransportEnrichment F (ForgetEnrichment V D)
⊢ (forgetEnrichmentEquivFunctor F D e h).map
        ((NatIso.ofComponents (fun x ↦ Iso.refl ((𝟭 (TransportEnrichment F (ForgetEnrichment V D))).obj x)) ⋯).hom.app
          X) ≫
      (NatIso.ofComponents
              (fun x ↦ Iso.refl ((forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h).obj x))
              ⋯).hom.app
        ((forgetEnrichmentEquivFunctor F D e h).obj X) =
    𝟙 ((forgetEnrichmentEquivFunctor F D e h).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Terminal

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
inst✝¹ : Unique T
inst✝ : IsDiscrete T
x✝¹ : Cat
x✝ : x✝¹ ⟶ of T
⊢ ∀ (X : ↑x✝¹), x✝.toFunctor.obj X = ((const ↑x✝¹).obj default).toCatHom.toFunctor.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Terminal

Goal state before:
pp: ⊢ HasTerminal Cat

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (𝟙 X) = eId V X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X✝ Y✝ Z✝ : P.FullSubcategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (f ≫ g) =
    (λ_ (𝟙_ V)).inv ≫
      ((P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) f ⊗ₘ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) g) ≫
        eComp V X✝ Y✝ Z✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: C D : Cat
F G : ↑C ⥤ ↑D
hyp : forget.map F.toCatHom = forget.map G.toCatHom
⊢ F = G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : ReflQuiv
F G : ↑V ⥤rq ↑W
hyp : forgetToQuiv.map F = forgetToQuiv.map G
⊢ F = G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
Y : ↑(of W)
⊢ (Quiv.homEquivOfIso e) (e.inv.map (𝟙rq Y)) = (Quiv.homEquivOfIso e) (𝟙rq (e.inv.obj Y))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ { toPrefunctor := e.hom, map_id := h_id } ≫ { toPrefunctor := e.inv, map_id := ⋯ } = 𝟙 (of V)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ { toPrefunctor := e.inv, map_id := ⋯ } ≫ { toPrefunctor := e.hom, map_id := h_id } = 𝟙 (of W)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
x y : V
e : x ⟶ y
⊢ morphismPropertyHomMk V (homMk e)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : FreeRefl V
f : x ⟶ y
⊢ motive f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
⊢ ⊤ ≤ (morphismPropertyHomMk V).multiplicativeClosure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : MorphismProperty (FreeRefl V)
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
⊢ W ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : MorphismProperty (FreeRefl V)
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
⊢ ⊤ ≤ W

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F : V ⥤rq D
⊢ ∀ (x y : Paths V) (f₁ f₂ : x ⟶ y),
    FreeReflRel V x y f₁ f₂ → (Paths.lift F.toPrefunctor).map f₁ = (Paths.lift F.toPrefunctor).map f₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
obj : V → D
map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w)
map_id : ∀ (v : V), map (𝟙rq v) = 𝟙 (obj v)
v w : V
f : v ⟶ w
⊢ (lift' obj (fun {v w} ↦ map) map_id).map (homMk f) = map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F G : FreeRefl V ⥤ D
h₁ : ∀ (v : V), F.obj (mk v) = G.obj (mk v)
h₂ : ∀ {v w : V} (f : v ⟶ w), F.map (homMk f) = eqToHom ⋯ ≫ G.map (homMk f) ≫ eqToHom ⋯
⊢ (quotientFunctor V ⋙ F).obj = (quotientFunctor V ⋙ G).obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x y : FreeRefl V
f : x ⟶ y
⊢ f = homMk default

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : ∀ (x y : V), Subsingleton (x ⟶ y)
x✝ y✝ : FreeRefl V
x y : V
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : ∀ (x y : V), Subsingleton (x ⟶ y)
x✝ y✝ : FreeRefl V
x y : V
⊢ Unique (x ⟶ y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F : V ⥤rq D
v : V
⊢ (toFreeRefl V ⋙rq (lift F).toReflPrefunctor).obj v = F.obj v

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F : V ⥤rq D
⊢ ∀ (X Y : V) (f : X ⟶ Y), (toFreeRefl V ⋙rq (lift F).toReflPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (F.map f))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v : V
⊢ FreeRefl.homMk (F.map (𝟙rq v)) = 𝟙 (FreeRefl.mk (F.obj v))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_3
W : Type u_4
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
F : V ⥤rq W
⊢ ∀ (a b : V) (e : a ⟶ b),
    (FreeRefl.quotientFunctor V ⋙ freeReflMap F).map e.toPath =
      eqToHom ⋯ ≫ (freeMap F.toPrefunctor ⋙ FreeRefl.quotientFunctor W).map e.toPath ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ ∀ (v : ↑X),
    (freeReflMap (𝟙 X)).toCatHom.toFunctor.obj (FreeRefl.mk v) = (𝟙 (of (FreeRefl ↑X))).toFunctor.obj (FreeRefl.mk v)

Tactic:
by

Goal state after: