-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
lemma fac (j : J) : lift s ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j

Proof state:
case h
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

Tactic:
have := s.w k.hom

Result:
case h
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
this : s.π.app ((Functor.fromPUnit j).obj k.left) ≫ (functorEnrichedHom V F₁ F₂).map k.hom = s.π.app ((𝟭 J).obj k.right)
⊢ (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

Proof state:
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 ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j

Tactic:
dsimp [coneFunctorEnrichedHom]

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

Proof state:
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

Result:
case h
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

Proof state:
case h
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
this :
  s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)) =
    s.π.app k.right
⊢ s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map k.hom).obj (Under.mk (𝟙 k.right))) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k

Tactic:
congr

Result:
case h.e_a.h.e_12.h
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
this :
  s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)) =
    s.π.app k.right
⊢ (Under.map k.hom).obj (Under.mk (𝟙 k.right)) = k

Proof state:
case h.e_a.h.e_12.h
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
this :
  s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)) =
    s.π.app k.right
⊢ { left := (Under.mk (𝟙 k.right)).left, right := k.right, hom := k.hom } = k

Tactic:
rfl

Result:
no goals

Proof state:
case h.e_a.h.e_12.h
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
this :
  s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)) =
    s.π.app k.right
⊢ (Under.map k.hom).obj (Under.mk (𝟙 k.right)) = k

Tactic:
simp [Under.map, Comma.mapLeft]

Result:
case h.e_a.h.e_12.h
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
this :
  s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)) =
    s.π.app k.right
⊢ { left := (Under.mk (𝟙 k.right)).left, right := k.right, hom := k.hom } = k