mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X : C
⊢ (ρ_ ((coyoneda.obj (op (𝟙_ C))).obj X)).hom =
    (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun x ↦ 𝟙 (unop (op (𝟙_ C)))) ≫
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (ρ_ X).hom

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).arrow i =
    sx.spineToDiagonal (f.interval (↑i) 2 ⋯)

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
p : X.Path 0
⊢ X.spine 0 (p.vertex 0) = p

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 0 < i.succ.castSucc

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 1 + n ≤ n + 1

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 1 + ↑i = ↑i.succ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path n
⊢ { s // X.spine n s = p }

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p✝ : X.Path n
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (p.arrow 0) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ 0).op)) (spineToSimplex h (p.interval 1 n ⋯))

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op)) (spineToSimplex h p) = p.arrow 0

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (spineToSimplex h p) = spineToSimplex h (p.interval 1 n ⋯)

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n✝ n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (spineToSimplex h (X.spine (n + 1) s)) =
    (ConcreteCategory.hom (SimplicialObject.δ X 0)) s

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋n⦌
⊢ spineToSimplex h (X.spine n s) = s

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
⊢ ∀ (n : ℕ), X.spine n ∘ StrictSegalCore.spineToSimplex h = id

Tactic:
by

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
⊢ StrictSegalCore.spineToSimplex h ∘ X.spine n = id

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
f : nerve C _⦋1⦌
s : nerve C _⦋n⦌
h :
  (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) f =
    (ConcreteCategory.hom ((nerve C).map (⦋0⦌.const ⦋n⦌ 0).op)) s
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom ((nerve C).map (mkOfSucc 0).op))
        (ComposableArrows.precomp s (ComposableArrows.hom f ≫ eqToHom ⋯))) =
    eqToHom ⋯ ≫ ComposableArrows.hom f ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
⊢ X.Quasicategory

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η ≍ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) ≍ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c d : CatEnriched C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ hComp (hComp η θ) κ = eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    hComp (𝟙 (f ≫ g)) η = (eqToIso ⋯).hom ≫ hComp (𝟙 f) (hComp (𝟙 g) η) ≫ (eqToIso ⋯).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    hComp η (𝟙 (g ≫ h)) = (eqToIso ⋯).inv ≫ hComp (hComp η (𝟙 g)) (𝟙 h) ≫ (eqToIso ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    hComp (hComp (𝟙 f) η) (𝟙 h) = (eqToIso ⋯).hom ≫ hComp (𝟙 f) (hComp η (𝟙 h)) ≫ (eqToIso ⋯).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
⊢ hComp (eqToIso ⋯).hom (𝟙 i) ≫ (eqToIso ⋯).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (eqToIso ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
⊢ (eqToIso ⋯).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = hComp (eqToIso ⋯).hom (𝟙 g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ homEquiv (𝟙 a) = 𝟙 a.toBase

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
X Y : C
⊢ eHomWhiskerRight V (𝟙 X) Y = 𝟙 (X ⟶[V] Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ homEquiv (f ≫ g) = homEquiv f ≫ homEquiv g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α β : f ⟶ g
H : base α = base β
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α : f = g
⊢ base (eqToHom α) = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (𝟙 f) (𝟙 g) = 𝟙 (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f₁ f₂ f₃ : a ⟶ b
g₁ g₂ g₃ : b ⟶ c
η : f₁ ⟶ f₂
η' : f₂ ⟶ f₃
θ : g₁ ⟶ g₂
θ' : g₂ ⟶ g₃
⊢ hComp η θ ≫ hComp η' θ' = hComp (η ≫ η') (θ ≫ θ')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η ≍ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) ≍ η

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
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ eHomWhiskerRight V (f ≫ f') Y = eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y

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
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ eHomWhiskerRight V f Z = (eHomWhiskerRight V f Y ▷ Y ⟶[V] Z) ≫ eComp V X Y Z

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
X Y : C
⊢ eHomWhiskerLeft V X (𝟙 Y) = 𝟙 (X ⟶[V] Y)

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
f g : X ⟶ Y
w : f.f = g.f
⊢ f = 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 : Center C
f : X ⟶ Y
inst✝ : IsIso f.f
U : C
⊢ inv f.f ▷ U ≫ (X.snd.β U).hom = (Y.snd.β U).hom ≫ U ◁ inv f.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
f : X ⟶ Y
inst✝ : IsIso f.f
⊢ IsIso 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
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ eHomWhiskerLeft V X (g ≫ g') = eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X 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 : Center C
U U' : C
⊢ (α_ X.fst Y.fst (U ⊗ U')).hom ≫
      X.fst ◁
          ((α_ Y.fst U U').inv ≫
            (Y.snd.β U).hom ▷ U' ≫ (α_ U Y.fst U').hom ≫ U ◁ (Y.snd.β U').hom ≫ (α_ U U' Y.fst).inv) ≫
        (α_ X.fst (U ⊗ U') Y.fst).inv ≫
          ((α_ X.fst U U').inv ≫
                (X.snd.β U).hom ▷ U' ≫ (α_ U X.fst U').hom ≫ U ◁ (X.snd.β U').hom ≫ (α_ U U' X.fst).inv) ▷
              Y.fst ≫
            (α_ (U ⊗ U') X.fst Y.fst).hom =
    𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.fst ⊗ U) ◁ (Y.snd.β U').hom ≫ (X.snd.β U).hom ▷ (U' ⊗ Y.fst)) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst)

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
X Y Z Z' : C
g : Z ⟶ Z'
⊢ eComp V X Y Z ≫ eHomWhiskerLeft V X g = (X ⟶[V] Y) ◁ eHomWhiskerLeft V Y g ≫ eComp V X Y Z'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ hComp (hComp η θ) κ = eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ hComp (hComp η θ) κ ≍ hComp η (hComp θ κ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b : CatEnrichedOrdinary C} {f g : a ⟶ b} (η : f ⟶ g), hComp (𝟙 (𝟙 a)) η = (eqToIso ⋯).hom ≫ η ≫ (eqToIso ⋯).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
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ (eHomWhiskerLeft V X α.hom ▷ Y ⟶[V] Z) ≫ (X ⟶[V] Y₁) ◁ eHomWhiskerRight V α.inv Z ≫ eComp V X Y₁ Z = eComp V X Y Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c d : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    hComp (𝟙 (f ≫ g)) η = (eqToIso ⋯).hom ≫ hComp (𝟙 f) (hComp (𝟙 g) η) ≫ (eqToIso ⋯).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 Y : Center C
U U' : C
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.fst ⊗ U) ◁ (Y.snd.β U').hom ≫ (X.snd.β U).hom ▷ (U' ⊗ Y.fst)) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst) =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      ((α_ 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' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          U ◁
              ((α_ 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 U' (X.fst ⊗ Y.fst)).inv

Tactic:
whisker_exchange

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.snd.β U).hom ▷ (Y.fst ⊗ U') ≫ (U ⊗ X.fst) ◁ (Y.snd.β U').hom) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst) =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      ((α_ 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' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          U ◁
              ((α_ 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 U' (X.fst ⊗ Y.fst)).inv
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b : CatEnrichedOrdinary C} {f g : a ⟶ b} (η : f ⟶ g), hComp η (𝟙 (𝟙 b)) = (eqToIso ⋯).hom ≫ η ≫ (eqToIso ⋯).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c d : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    hComp η (𝟙 (g ≫ h)) = (eqToIso ⋯).inv ≫ hComp (hComp η (𝟙 g)) (𝟙 h) ≫ (eqToIso ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c d : CatEnrichedOrdinary C} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    hComp (hComp (𝟙 f) η) (𝟙 h) = (eqToIso ⋯).hom ≫ hComp (𝟙 f) (hComp η (𝟙 h)) ≫ (eqToIso ⋯).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c d e : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
    hComp (eqToIso ⋯).hom (𝟙 i) ≫ (eqToIso ⋯).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (eqToIso ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c),
    (eqToIso ⋯).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = hComp (eqToIso ⋯).hom (𝟙 g)

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
W X Y Z : C
⊢ (α_ (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom ≫ (W ⟶[V] X) ◁ eComp V X Y Z ≫ eComp V W X Z =
    (eComp V W X Y ▷ Y ⟶[V] Z) ≫ eComp V W Y Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
a : F.HomObj G A
X Y : C
f : X ⟶ Y
⊢ ((F ⊗ A).map f ≫
      ↾fun x ↦
        match x with
        | (x, y) => (ConcreteCategory.hom (a.app Y y)) x) =
    (↾fun x ↦
        match x with
        | (x, y) => (ConcreteCategory.hom (a.app X y)) x) ≫
      G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
a : F ⊗ A ⟶ G
c✝ d✝ : C
φ : c✝ ⟶ d✝
y : A.obj c✝
⊢ (F.map φ ≫ ↾fun x ↦ (ConcreteCategory.hom (a.app d✝)) (x, (ConcreteCategory.hom (A.map φ)) y)) =
    (↾fun x ↦ (ConcreteCategory.hom (a.app c✝)) (x, y)) ≫ G.map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
x✝ : F.HomObj G A
⊢ (fun a ↦ { app := fun X y ↦ ↾fun x ↦ (ConcreteCategory.hom (a.app X)) (x, y), naturality := ⋯ })
      ((fun a ↦
          {
            app := fun X ↦
              ↾fun x ↦
                match x with
                | (x, y) => (ConcreteCategory.hom (a.app X y)) x,
            naturality := ⋯ })
        x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
x✝ : F ⊗ A ⟶ G
⊢ (fun a ↦
        {
          app := fun X ↦
            ↾fun x ↦
              match x with
              | (x, y) => (ConcreteCategory.hom (a.app X y)) x,
          naturality := ⋯ })
      ((fun a ↦ { app := fun X y ↦ ↾fun x ↦ (ConcreteCategory.hom (a.app X)) (x, y), naturality := ⋯ }) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type w
f g : F.HomObj G A
h : f = g
X : C
a : A.obj X
⊢ f.app X a = g.app X a

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
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ (λ_ (F.obj (X ⟶[V] Y))).inv ≫
      (ε F ≫ F.map (eId V X)) ▷ F.obj (X ⟶[V] Y) ≫ μ F (X ⟶[V] X) (X ⟶[V] Y) ≫ F.map (eComp V X X Y) =
    𝟙 (F.obj (X ⟶[V] Y))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : C ⥤ Type w
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
⊢ F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (f.app Δ')) ((ConcreteCategory.hom (A'.map φ)) a)) =
    x.app Δ ((ConcreteCategory.hom (f.app Δ)) a) ≫ G.map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : (C ⥤ Type w)ᵒᵖ
f : A ⟶ A'
x : F.HomObj G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ F.map φ ≫ x.app Y ((ConcreteCategory.hom (f.unop.app Y)) ((ConcreteCategory.hom ((Opposite.unop A').map φ)) a)) =
    x.app X ((ConcreteCategory.hom (f.unop.app X)) a) ≫ G.map φ

Tactic:
by

Goal state after: