English
A simp lemma expressing equality of a large uncurry₃ composition of functors with the corresponding iso in Lifting₃.
Русский
Лемма-упрощение, выражающая равенство большой композиции uncurry₃ функторов и соответствующего изоморфизма в Lifting₃.
LaTeX
$$$\text{lift₃NatTrans}(...)=...$$$
Lean4
@[simp]
theorem lift₃NatTrans_app_app_app (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
(((lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) =
(((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃ ≫
((τ.app X₁).app X₂).app X₃ ≫ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃ :=
by
dsimp [lift₃NatTrans, fullyFaithfulUncurry₃, Equivalence.fullyFaithfulFunctor]
simp only [currying₃_unitIso_hom_app_app_app_app, Functor.id_obj, currying₃_unitIso_inv_app_app_app_app,
Functor.comp_obj, Category.comp_id, Category.id_comp]
exact liftNatTrans_app _ _ _ _ (uncurry₃.obj F₁') (uncurry₃.obj F₂') (uncurry₃.map τ) ⟨X₁, X₂, X₃⟩
