-- Mathlib/CategoryTheory/Localization/Bifunctor.lean
theorem lift₂NatTrans_app_app (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂) :
    ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) =
      ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫ (τ.app X₁).app X₂ ≫
        ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst✝¹⁰ : Category.{u_8, u_1} C₁
inst✝⁹ : Category.{u_9, u_2} C₂
inst✝⁸ : Category.{u_11, u_3} D₁
inst✝⁷ : Category.{u_10, u_4} D₂
inst✝⁶ : Category.{u_7, u_5} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F₁) (uncurry.obj F₂) (uncurry.obj F₁') (uncurry.obj F₂')
          (uncurry.map τ)).app
      (L₁.obj X₁, L₂.obj X₂) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂

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

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst✝¹⁰ : Category.{u_8, u_1} C₁
inst✝⁹ : Category.{u_9, u_2} C₂
inst✝⁸ : Category.{u_11, u_3} D₁
inst✝⁷ : Category.{u_10, u_4} D₂
inst✝⁶ : Category.{u_7, u_5} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂

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

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst✝¹⁰ : Category.{u_8, u_1} C₁
inst✝⁹ : Category.{u_9, u_2} C₂
inst✝⁸ : Category.{u_11, u_3} D₁
inst✝⁷ : Category.{u_10, u_4} D₂
inst✝⁶ : Category.{u_7, u_5} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ 𝟙 ((F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) ≫
      (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F₁) (uncurry.obj F₂) (uncurry.obj F₁') (uncurry.obj F₂')
              (uncurry.map τ)).app
          (L₁.obj X₁, L₂.obj X₂) ≫
        𝟙 ((F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst✝¹⁰ : Category.{u_8, u_1} C₁
inst✝⁹ : Category.{u_9, u_2} C₂
inst✝⁸ : Category.{u_11, u_3} D₁
inst✝⁷ : Category.{u_10, u_4} D₂
inst✝⁶ : Category.{u_7, u_5} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ 𝟙 ((F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) ≫
      (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F₁) (uncurry.obj F₂) (uncurry.obj F₁') (uncurry.obj F₂')
              (uncurry.map τ)).app
          (L₁.obj X₁, L₂.obj X₂) ≫
        𝟙 ((F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂)) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂

Tactic:
simp only [currying_unitIso_hom_app_app_app, currying_unitIso_inv_app_app_app, comp_id, id_comp]

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst✝¹⁰ : Category.{u_8, u_1} C₁
inst✝⁹ : Category.{u_9, u_2} C₂
inst✝⁸ : Category.{u_11, u_3} D₁
inst✝⁷ : Category.{u_10, u_4} D₂
inst✝⁶ : Category.{u_7, u_5} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F₁) (uncurry.obj F₂) (uncurry.obj F₁') (uncurry.obj F₂')
          (uncurry.map τ)).app
      (L₁.obj X₁, L₂.obj X₂) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂