-- Mathlib/CategoryTheory/Localization/Trifunctor.lean
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₃

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
inst✝¹⁴ : Category.{u_18, u_1} C₁
inst✝¹³ : Category.{u_19, u_2} C₂
inst✝¹² : Category.{u_20, u_3} C₃
inst✝¹¹ : Category.{u_17, u_6} D₁
inst✝¹⁰ : Category.{u_16, u_7} D₂
inst✝⁹ : Category.{u_15, u_8} D₃
inst✝⁸ : Category.{u_14, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((currying₃.unitIso.hom.app F₁').app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) ≫
      (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (uncurry₃.obj F₁) (uncurry₃.obj F₂) (uncurry₃.obj F₁')
              (uncurry₃.obj F₂') (uncurry₃.map τ)).app
          (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃) ≫
        (((currying₃.unitIso.inv.app 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₃

Tactic:
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]

Result:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
inst✝¹⁴ : Category.{u_18, u_1} C₁
inst✝¹³ : Category.{u_19, u_2} C₂
inst✝¹² : Category.{u_20, u_3} C₃
inst✝¹¹ : Category.{u_17, u_6} D₁
inst✝¹⁰ : Category.{u_16, u_7} D₂
inst✝⁹ : Category.{u_15, u_8} D₃
inst✝⁸ : Category.{u_14, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (uncurry₃.obj F₁) (uncurry₃.obj F₂) (uncurry₃.obj F₁')
          (uncurry₃.obj F₂') (uncurry₃.map τ)).app
      (L₁.obj X₁, L₂.obj X₂, 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₃

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
inst✝¹⁴ : Category.{u_18, u_1} C₁
inst✝¹³ : Category.{u_19, u_2} C₂
inst✝¹² : Category.{u_20, u_3} C₃
inst✝¹¹ : Category.{u_17, u_6} D₁
inst✝¹⁰ : Category.{u_16, u_7} D₂
inst✝⁹ : Category.{u_15, u_8} D₃
inst✝⁸ : Category.{u_14, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (uncurry₃.obj F₁) (uncurry₃.obj F₂) (uncurry₃.obj F₁')
          (uncurry₃.obj F₂') (uncurry₃.map τ)).app
      (L₁.obj X₁, L₂.obj X₂, 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₃

Tactic:
exact liftNatTrans_app _ _ _ _ (uncurry₃.obj F₁') (uncurry₃.obj F₂') (uncurry₃.map τ) ⟨X₁, X₂, X₃⟩

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
inst✝¹⁴ : Category.{u_18, u_1} C₁
inst✝¹³ : Category.{u_19, u_2} C₂
inst✝¹² : Category.{u_20, u_3} C₃
inst✝¹¹ : Category.{u_17, u_6} D₁
inst✝¹⁰ : Category.{u_16, u_7} D₂
inst✝⁹ : Category.{u_15, u_8} D₃
inst✝⁸ : Category.{u_14, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
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₃

Tactic:
dsimp [lift₃NatTrans, fullyFaithfulUncurry₃, Equivalence.fullyFaithfulFunctor]

Result:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
inst✝¹⁴ : Category.{u_18, u_1} C₁
inst✝¹³ : Category.{u_19, u_2} C₂
inst✝¹² : Category.{u_20, u_3} C₃
inst✝¹¹ : Category.{u_17, u_6} D₁
inst✝¹⁰ : Category.{u_16, u_7} D₂
inst✝⁹ : Category.{u_15, u_8} D₃
inst✝⁸ : Category.{u_14, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((currying₃.unitIso.hom.app F₁').app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) ≫
      (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (uncurry₃.obj F₁) (uncurry₃.obj F₂) (uncurry₃.obj F₁')
              (uncurry₃.obj F₂') (uncurry₃.map τ)).app
          (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃) ≫
        (((currying₃.unitIso.inv.app 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₃