enrichedComp — Mathlib

Lean4
/-- The composition for the `V`-enrichment of the category `J ⥤ C`. -/
noncomputable def enrichedComp : enrichedHom V F₁ F₂ ⊗ enrichedHom V F₂ F₃ ⟶ enrichedHom V F₁ F₃ :=
  end_.lift (fun j ↦ (end_.π _ j ⊗ₘ end_.π _ j) ≫ eComp V _ _ _)
    (fun i j f ↦ 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])
Похожие утверждения