mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⊗ Y.fst)) ⊗≫ (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:
;

Goal state after:
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 ⊗ Y.fst)) ⊗≫ (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)
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 ⊗≫ ((X₁.snd.β U).hom ≫ U ◁ f.f) ▷ 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:
;

Goal state after:
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 ⊗≫ ((X₁.snd.β U).hom ≫ U ◁ f.f) ▷ 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
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 rw [f.comm]; monoidal

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:
;

Goal state after:
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✝
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✝).f = (whiskerRight f✝ X₂✝ ≫ Y₁✝.whiskerLeft g✝).f

Tactic:
;

Goal state after:
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✝).f = (whiskerRight f✝ X₂✝ ≫ Y₁✝.whiskerLeft g✝).f
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)).f = 𝟙 ((X ⊗ Y) ⊗ Z).fst

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (𝟙 ((X ⊗ Y) ⊗ Z)).f = 𝟙 ((X ⊗ Y) ⊗ Z).fst
Module: Mathlib.CategoryTheory.Monoidal.Center

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

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (𝟙 (𝟙_ (Center C) ⊗ X)).f = 𝟙 (𝟙_ (Center C) ⊗ X).fst
Module: Mathlib.CategoryTheory.Monoidal.Center

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

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (𝟙 (X ⊗ 𝟙_ (Center C))).f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst
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 f.f
⊢ IsIso f

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ B✝ : Center C
f : A✝ ⟶ B✝
i : IsIso f.f
⊢ IsIso f
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 f.f
⊢ IsIso (isoMk f).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ B✝ : Center C
f : A✝ ⟶ B✝
i : IsIso f.f
⊢ IsIso (isoMk f).hom
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:
rw [isCoskeletal_iff]
  exact isRightKanExtension_iff_isIso ((coskAdj n).unit.app X)
    ((coskAdj n).counit.app _) (𝟙 _) ((coskAdj n).left_triangle_components X)

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

Goal state before:
pp: case mk
C D : Cat
G : ↑C ⥤ ↑D
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
hyp : forget.map { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.toCatHom = forget.map G.toCatHom
⊢ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } = G

Tactic:
;

Goal state after:
case mk
C D : Cat
G : ↑C ⥤ ↑D
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
hyp : forget.map { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.toCatHom = forget.map G.toCatHom
⊢ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } = G
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk
C D : Cat
obj✝¹ : ↑C → ↑D
map✝¹ : {X Y : ↑C} → (X ⟶ Y) → (obj✝¹ X ⟶ obj✝¹ Y)
map_id✝¹ : ∀ (X : ↑C), map✝¹ (𝟙 X) = 𝟙 (obj✝¹ X)
map_comp✝¹ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
hyp :
  forget.map { obj := obj✝¹, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toCatHom =
    forget.map { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.toCatHom
⊢ { obj := obj✝¹, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
;

Goal state after:
case mk.mk
C D : Cat
obj✝¹ : ↑C → ↑D
map✝¹ : {X Y : ↑C} → (X ⟶ Y) → (obj✝¹ X ⟶ obj✝¹ Y)
map_id✝¹ : ∀ (X : ↑C), map✝¹ (𝟙 X) = 𝟙 (obj✝¹ X)
map_comp✝¹ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
hyp :
  forget.map { obj := obj✝¹, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toCatHom =
    forget.map { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.toCatHom
⊢ { obj := obj✝¹, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk.refl
C D : Cat
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝¹ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝¹ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
⊢ { obj := obj✝, map := map✝, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
;

Goal state after:
case mk.mk.refl
C D : Cat
obj✝ : ↑C → ↑D
map✝ : {X Y : ↑C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝¹ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝¹ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
map_id✝ : ∀ (X : ↑C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
⊢ { obj := obj✝, map := map✝, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk
V W : ReflQuiv
G : ↑V ⥤rq ↑W
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp : forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = forgetToQuiv.map G
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = G

Tactic:
;

Goal state after:
case mk
V W : ReflQuiv
G : ↑V ⥤rq ↑W
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp : forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = forgetToQuiv.map G
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝ } = G
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk
V W : ReflQuiv
toPrefunctor✝¹ : ↑V ⥤q ↑W
map_id✝¹ : ∀ (X : ↑V), toPrefunctor✝¹.map (𝟙rq X) = 𝟙rq (toPrefunctor✝¹.obj X)
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp :
  forgetToQuiv.map { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } =
    forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }
⊢ { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }

Tactic:
;

Goal state after:
case mk.mk
V W : ReflQuiv
toPrefunctor✝¹ : ↑V ⥤q ↑W
map_id✝¹ : ∀ (X : ↑V), toPrefunctor✝¹.map (𝟙rq X) = 𝟙rq (toPrefunctor✝¹.obj X)
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
hyp :
  forgetToQuiv.map { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } =
    forgetToQuiv.map { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }
⊢ { toPrefunctor := toPrefunctor✝¹, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk.refl
V W : ReflQuiv
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝¹ map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }

Tactic:
;

Goal state after:
case mk.mk.refl
V W : ReflQuiv
toPrefunctor✝ : ↑V ⥤q ↑W
map_id✝¹ map_id✝ : ∀ (X : ↑V), toPrefunctor✝.map (𝟙rq X) = 𝟙rq (toPrefunctor✝.obj X)
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝¹ } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝ }
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 ⋯
x✝ : Paths V
⊢ (quotientFunctor V ⋙ F).obj x✝ = (quotientFunctor V ⋙ G).obj x✝

Tactic:
;

Goal state after:
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 ⋯
x✝ : Paths V
⊢ (quotientFunctor V ⋙ F).obj x✝ = (quotientFunctor V ⋙ G).obj x✝
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case id
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
x✝ : V
⊢ 𝟙rq x✝ = default

Tactic:
;

Goal state after:
case id
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
x✝ : V
⊢ 𝟙rq x✝ = default
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
⊢ (freeReflMap (𝟙 X)).toCatHom.toFunctor = (𝟙 (of (FreeRefl ↑X))).toFunctor

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ (freeReflMap (𝟙 X)).toCatHom.toFunctor = (𝟙 (of (FreeRefl ↑X))).toFunctor
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 Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ (freeReflMap (f ≫ g)).toCatHom.toFunctor = ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ (freeReflMap (f ≫ g)).toCatHom.toFunctor = ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor
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 w : ReflQuiv
f : v ⟶ w
⊢ ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor =
    ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor =
    ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: X'✝ X✝ : ReflQuiv
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ forget.obj Y✝
⊢ (((Cat.Hom.equivFunctor (Cat.freeRefl.obj X'✝) Y✝).trans adj.homEquiv).symm (x✝¹ ≫ x✝)).toFunctor =
    (Cat.freeRefl.map x✝¹ ≫ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X✝) Y✝).trans adj.homEquiv).symm x✝).toFunctor

Tactic:
;

Goal state after:
X'✝ X✝ : ReflQuiv
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ forget.obj Y✝
⊢ (((Cat.Hom.equivFunctor (Cat.freeRefl.obj X'✝) Y✝).trans adj.homEquiv).symm (x✝¹ ≫ x✝)).toFunctor =
    (Cat.freeRefl.map x✝¹ ≫ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X✝) Y✝).trans adj.homEquiv).symm x✝).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
i : Fin n
x :
  Fin
    ((unop
          ((inclusion 2).op.obj
            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len +
      1)
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop)
        x) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        x)

Tactic:
;

Goal state after:
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
i : Fin n
x :
  Fin
    ((unop
          ((inclusion 2).op.obj
            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len +
      1)
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop)
        x) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «0»
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩)) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩))

Tactic:
;

Goal state after:
case «0»
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩)) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
i : Fin n
x :
  Fin
    ((unop
          ((inclusion 2).op.obj
            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len +
      1)
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop)
        x) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        x)

Tactic:
;

Goal state after:
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
i : Fin n
x :
  Fin
    ((unop
          ((inclusion 2).op.obj
            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len +
      1)
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop)
        x) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «0»
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩)) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩))

Tactic:
;

Goal state after:
case «0»
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩)) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ (Truncated.Edge.map (𝟙rq x) f).edge =
    (𝟙rq ((ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := _proof_1 }))) x)).edge

Tactic:
;

Goal state after:
S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ (Truncated.Edge.map (𝟙rq x) f).edge =
    (𝟙rq ((ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := _proof_1 }))) x)).edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ Truncated.Edge.map (𝟙rq x) f = 𝟙rq ((ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := _proof_1 }))) x)

Tactic:
by ext; simp [← NatTrans.naturality_apply, reflQuiver_id]

Goal state after: