mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
⊢ φ₁ = φ₂

Tactic:
let adj := mapPullbackAdj g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
⊢ φ₁ = φ₂
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
⊢ lift a b h ≫ fst f g = a

Tactic:
let adj := mapPullbackAdj g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
adj : map g ⊣ pullback g := mapPullbackAdj g
⊢ lift a b h ≫ fst f g = a
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F
i j : J
f : i ⟶ j
⊢ π F i ≫ (F.obj (op i)).map f = π F j ≫ (F.map f.op).app j

Tactic:
by
  apply Wedge.condition

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
C : Type u'
inst✝² : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasEnd F
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (F'.obj (op j)).map φ
⊢ π F j ≫ (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = π F j' ≫ (f.app (op j')).app j' ≫ (F'.map φ.op).app j'

Tactic:
reassoc_of% end_.condition F φ

Goal state after:
J : Type u
inst✝³ : Category.{v, u} J
C : Type u'
inst✝² : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasEnd F
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (F'.obj (op j)).map φ
⊢ π F j' ≫ (F.map φ.op).app j' ≫ (f.app (op j)).app j' = π F j' ≫ (f.app (op j')).app j' ≫ (F'.map φ.op).app j'
Module: Mathlib.CategoryTheory.Enriched.HomCongr

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 X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (eHomEquiv V) f ▷ 𝟙_ V ≫
        eHomWhiskerRight V α.inv Y ▷ 𝟙_ V ≫
          eHomWhiskerLeft V X₁ β.hom ▷ 𝟙_ V ≫
            (X₁ ⟶[V] Y₁) ◁ (eHomEquiv V) g ≫
              (X₁ ⟶[V] Y₁) ◁ eHomWhiskerRight V β.inv Z ≫ (X₁ ⟶[V] Y₁) ◁ eHomWhiskerLeft V Y₁ γ.hom ≫ eComp V X₁ Y₁ Z₁

Tactic:
← whisker_exchange_assoc,

Goal state after:
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 X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (eHomEquiv V) f ▷ 𝟙_ V ≫
        eHomWhiskerRight V α.inv Y ▷ 𝟙_ V ≫
          (X₁ ⟶[V] Y) ◁ (eHomEquiv V) g ≫
            (eHomWhiskerLeft V X₁ β.hom ▷ Y ⟶[V] Z) ≫
              (X₁ ⟶[V] Y₁) ◁ eHomWhiskerRight V β.inv Z ≫ (X₁ ⟶[V] Y₁) ◁ eHomWhiskerLeft V Y₁ γ.hom ≫ eComp V X₁ Y₁ Z₁
Module: Mathlib.CategoryTheory.Enriched.HomCongr

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 X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (eHomEquiv V) f ▷ 𝟙_ V ≫
        eHomWhiskerRight V α.inv Y ▷ 𝟙_ V ≫
          (X₁ ⟶[V] Y) ◁ (eHomEquiv V) g ≫
            (eHomWhiskerLeft V X₁ β.hom ▷ Y ⟶[V] Z) ≫
              (X₁ ⟶[V] Y₁) ◁ eHomWhiskerRight V β.inv Z ≫ (X₁ ⟶[V] Y₁) ◁ eHomWhiskerLeft V Y₁ γ.hom ≫ eComp V X₁ Y₁ Z₁

Tactic:
← whisker_exchange_assoc,

Goal state after:
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 X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (eHomEquiv V) f ▷ 𝟙_ V ≫
        (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
          (eHomWhiskerRight V α.inv Y ▷ Y ⟶[V] Z) ≫
            (eHomWhiskerLeft V X₁ β.hom ▷ Y ⟶[V] Z) ≫
              (X₁ ⟶[V] Y₁) ◁ eHomWhiskerRight V β.inv Z ≫ (X₁ ⟶[V] Y₁) ◁ eHomWhiskerLeft V Y₁ γ.hom ≫ eComp V X₁ Y₁ Z₁
Module: Mathlib.CategoryTheory.EquivalenceRelation

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

Tactic:
by simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

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

Tactic:
by simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

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

Tactic:
by simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

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

Tactic:
by simp [← F.map_comp]

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

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ (ρ_ (𝟙_ V)).inv ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop

Tactic:
← leftUnitor_inv_braiding_assoc

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ (λ_ (𝟙_ V)).inv ≫
      (β_ (𝟙_ V) (𝟙_ V)).hom ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop
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₂) j ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
      (λ_ ((F₁.obj j ⟶[V] F₂.obj j) ⊗ F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        (eHomEquiv V) (F₁.map f) ▷ ((F₁.obj j ⟶[V] F₂.obj j) ⊗ F₂.obj j ⟶[V] F₃.obj j) ≫
          (F₁.obj i ⟶[V] F₁.obj j) ◁ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₃.obj j)

Tactic:
← whisker_exchange_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₂) j ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
      (λ_ ((F₁.obj j ⟶[V] F₂.obj j) ⊗ F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        𝟙_ V ◁ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ≫
          ((eHomEquiv V) (F₁.map f) ▷ 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: case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ map p f φ ⋯ (map p g ψ ⋯ τ) ≫ φ ≫ ψ = τ

Tactic:
rw [← assoc, fac, fac]

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

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
⊢ ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (F₃.obj i)) ≫
      ((diagram V F₁ F₃).obj (Opposite.op i)).map f =
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)) ≫
      ((diagram V F₁ F₃).map f.op).app j

Tactic:
by
    dsimp
    trans (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      (ρ_ _).inv ▷ _ ≫ (_ ◁ (eHomEquiv V (F₂.map f))) ▷ _ ≫ eComp V _ (F₂.obj i) _ ▷ _ ≫
        eComp V _ (F₂.obj j) _
    · have := end_.condition (diagram V F₂ F₃) f
      dsimp [eHomWhiskerLeft, eHomWhiskerRight] at this ⊢
      conv_lhs => rw [assoc, tensorHom_def_assoc]
      conv_rhs =>
        rw [tensorHom_def_assoc, whisker_assoc_assoc, e_assoc,
          triangle_assoc_comp_right_inv_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          ← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          assoc, assoc, ← this, MonoidalCategory.whiskerLeft_comp_assoc,
          MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
          ← e_assoc, whiskerLeft_rightUnitor_inv_assoc, associator_inv_naturality_right_assoc,
          Iso.hom_inv_id_assoc, whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc,
          Iso.inv_hom_id_assoc]
    · have := end_.condition (diagram V F₁ F₂) f
      dsimp [eHomWhiskerLeft, eHomWhiskerRight] at this ⊢
      conv_lhs =>
        rw [tensorHom_def'_assoc, ← comp_whiskerRight_assoc,
          ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc,
          assoc, assoc, this, comp_whiskerRight_assoc, comp_whiskerRight_assoc,
          comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc,
          ← associator_inv_naturality_left_assoc, ← e_assoc',
          Iso.inv_hom_id_assoc, ← whisker_exchange_assoc, id_whiskerLeft_assoc,
          Iso.inv_hom_id_assoc]
      conv_rhs => rw [assoc, tensorHom_def'_assoc]

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

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      eId V (F₁.obj j) ▷ enrichedHom V F₁ F₂ ≫
        ((diagram V F₁ F₁).obj (Opposite.op j)).obj j ◁ end_.π (diagram V F₁ F₂) j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
← whisker_exchange_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
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      𝟙_ V ◁ end_.π (diagram V F₁ F₂) j ≫
        eId V (F₁.obj j) ▷ ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) 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
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₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ▷ enrichedHom V F₃ F₄ ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷ enrichedHom V F₃ F₄ ≫
        ((diagram V F₁ F₃).obj (Opposite.op j)).obj j ◁ end_.π (diagram V F₃ F₄) j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)

Tactic:
← whisker_exchange_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
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₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ▷ enrichedHom V F₃ F₄ ≫
      (((diagram V F₁ F₂).obj (Opposite.op j)).obj j ⊗ ((diagram V F₂ F₃).obj (Opposite.op j)).obj j) ◁
          end_.π (diagram V F₃ F₄) j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
            ((diagram V F₃ F₄).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (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
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₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ▷ enrichedHom V F₃ F₄ ≫
      (((diagram V F₁ F₂).obj (Opposite.op j)).obj j ⊗ ((diagram V F₂ F₃).obj (Opposite.op j)).obj j) ◁
          end_.π (diagram V F₃ F₄) j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
            ((diagram V F₃ F₄).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)

Tactic:
← whisker_exchange_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
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₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    (enrichedHom V F₁ F₂ ⊗ enrichedHom V F₂ F₃) ◁ end_.π (diagram V F₃ F₄) j ≫
      (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ▷ ((diagram V F₃ F₄).obj (Opposite.op j)).obj j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
            ((diagram V F₃ F₄).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j)
Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit

Goal state before:
pp: K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
this : Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨X, y, -⟩ := Types.jointly_surjective' (this.map (h (F.op ⋙ coyoneda)).some).some

Goal state after:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
this : Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))
X : K
y : (limit (F.op ⋙ coyoneda)).obj X
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
⊢ lift s ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) = s.π.app j

Tactic:
ext k

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
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
k : Under j
⊢ (lift s ≫ precompEnrichedHom V F₁ F₂ (Under.forget j)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
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✝² : HasFunctorEnrichedHom V F₁ F₂
inst✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
⊢ (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))) ≫
      enrichedComp V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃) =
    enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))

Tactic:
ext k

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✝² : HasFunctorEnrichedHom V F₁ F₂
inst✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
k : Under j'
⊢ ((precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
          precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))) ≫
        enrichedComp V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)) ≫
      end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k =
    (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))) ≫
      end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ (homEquiv V) (f ≫ g) ≫ precompEnrichedHom V F₁ F₃ (Under.forget j) =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗ₘ
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)

Tactic:
ext k

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
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ ((homEquiv V) (f ≫ g) ≫ precompEnrichedHom V F₁ F₃ (Under.forget j)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k =
    ((λ_ (𝟙_ V)).inv ≫
        ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗ₘ
            (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
          enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k