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

Goal state before:
pp: case e_f
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' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ≫ e₁.inv = (e₁.inv ⊗ₘ ε.inv) ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom) ≫ e₁.inv

Tactic:
assoc,

Goal state after:
case e_f
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' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ≫ e₁.inv = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ (L'.map (ρ_ X').hom ≫ e₁.hom) ≫ e₁.inv
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case e_f
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' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ≫ e₁.inv = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ (L'.map (ρ_ X').hom ≫ e₁.hom) ≫ e₁.inv

Tactic:
assoc,

Goal state after:
case e_f
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' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ≫ e₁.inv = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom ≫ e₁.inv
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case e_f
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' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ e₁.inv ▷ 𝟙_ (LocalizedMonoidal L W ε) ≫ L'.obj X' ◁ (ε' L W ε).inv ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom =
    (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom

Tactic:
← tensorHom_id,

Goal state after:
case e_f
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' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (e₁.inv ⊗ₘ 𝟙 (𝟙_ (LocalizedMonoidal L W ε))) ≫
      L'.obj X' ◁ (ε' L W ε).inv ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom =
    (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom
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₂
i j : J
f : i ⟶ j
| (ρ_ (𝟙_ V)).hom ≫
    (g ≫ end_.π (diagram V F₁ F₂) i) ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)

Tactic:
assoc,

Goal state after:
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₂
i j : J
f : i ⟶ j
| (ρ_ (𝟙_ V)).hom ≫
    g ≫
      end_.π (diagram V F₁ F₂) i ≫
        (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
          (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)
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' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  ((α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
        L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ L'.obj X' ◁ L'.map (λ_ Y').hom ≫ (μ L W ε X' Y').hom) ≫
      (μ L W ε X' Y').inv =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
assoc,

Goal state after:
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' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      (L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ L'.obj X' ◁ L'.map (λ_ Y').hom ≫ (μ L W ε X' Y').hom) ≫
        (μ L W ε X' Y').inv =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
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' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      (L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ L'.obj X' ◁ L'.map (λ_ Y').hom ≫ (μ L W ε X' Y').hom) ≫
        (μ L W ε X' Y').inv =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
assoc,

Goal state after:
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' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫
        (L'.obj X' ◁ L'.map (λ_ Y').hom ≫ (μ L W ε X' Y').hom) ≫ (μ L W ε X' Y').inv =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
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' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫
        (L'.obj X' ◁ L'.map (λ_ Y').hom ≫ (μ L W ε X' Y').hom) ≫ (μ L W ε X' Y').inv =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
assoc,

Goal state after:
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' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ L'.obj X' ◁ L'.map (λ_ Y').hom ≫ (μ L W ε X' Y').hom ≫ (μ L W ε X' Y').inv =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
    (ρ_ (F₁.obj i ⟶[V] F₃.obj i)).inv ≫
      (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)

Tactic:
assoc,

Goal state after:
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫
    eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
      (ρ_ (F₁.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁
        (((end_.π (diagram V F₂ F₃) j ≫ (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv) ≫
            (eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
          eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)) ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj j)

Tactic:
assoc,

Goal state after:
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁
        ((end_.π (diagram V F₂ F₃) j ≫ (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv) ≫
          ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)) ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj j)
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁
        ((end_.π (diagram V F₂ F₃) j ≫ (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv) ≫
          ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)) ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj j)

Tactic:
assoc,

Goal state after:
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁
        (end_.π (diagram V F₂ F₃) j ≫
          (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
            ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)) ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj j)
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    ((((end_.π (diagram V F₁ F₂) i ≫ (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv) ≫
            (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f)) ≫
          eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)) ▷
        F₂.obj j ⟶[V] F₃.obj j) ≫
      eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)

Tactic:
assoc,

Goal state after:
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    (((end_.π (diagram V F₁ F₂) i ≫ (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv) ≫
          (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)) ▷
        F₂.obj j ⟶[V] F₃.obj j) ≫
      eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    (((end_.π (diagram V F₁ F₂) i ≫ (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv) ≫
          (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)) ▷
        F₂.obj j ⟶[V] F₃.obj j) ≫
      eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)

Tactic:
assoc,

Goal state after:
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    ((end_.π (diagram V F₁ F₂) i ≫
          (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
            (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)) ▷
        F₂.obj j ⟶[V] F₃.obj j) ≫
      eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

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.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ f'' = (g' ≫ g) ≫ f

Tactic:
assoc,

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ f'' = g' ≫ g ≫ f
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
    (λ_ (F₁.obj j ⟶[V] F₃.obj j)).inv ≫
      ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₃.obj j)

Tactic:
assoc,

Goal state after:
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₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
    eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ≫
      (λ_ (F₁.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₃.obj j)