Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
eq :
  uliftYonedaEquiv.symm (unop x).snd ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      F.op.whiskerLeft (F.op.lan.map (uliftYonedaEquiv.symm (unop x).snd))
eq₁ :
  (hom
        (((StructuredArrow.Hom.right f).app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).app
          (op (F.obj (unop (unop x).fst)))))
      ((hom
          (((compULiftYonedaIsoULiftYonedaCompLan F).hom.app (unop (unop x).fst)).app (op (F.obj (unop (unop x).fst)))))
        { down := 𝟙 (F.obj (unop (unop x).fst)) }) =
    (hom (((StructuredArrow.hom Φ).app (unop (unop x).fst)).app (op (F.obj (unop (unop x).fst)))))
      { down := 𝟙 (F.obj (unop (unop x).fst)) }
eq₂ :
  (hom
        (((StructuredArrow.Hom.right g).app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).app
          (op (F.obj (unop (unop x).fst)))))
      ((hom
          (((compULiftYonedaIsoULiftYonedaCompLan F).hom.app (unop (unop x).fst)).app (op (F.obj (unop (unop x).fst)))))
        { down := 𝟙 (F.obj (unop (unop x).fst)) }) =
    (hom (((StructuredArrow.hom Φ).app (unop (unop x).fst)).app (op (F.obj (unop (unop x).fst)))))
      { down := 𝟙 (F.obj (unop (unop x).fst)) }
⊢ F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      F.op.whiskerLeft (F.op.lan.map (uliftYonedaEquiv.symm (unop x).snd) ≫ (StructuredArrow.Hom.right f).app P) =
    F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      F.op.whiskerLeft (F.op.lan.map (uliftYonedaEquiv.symm (unop x).snd) ≫ (StructuredArrow.Hom.right g).app P)

Tactic:
congr 2

Goal state after:
case e_a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
eq :
  uliftYonedaEquiv.symm (unop x).snd ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      F.op.whiskerLeft (F.op.lan.map (uliftYonedaEquiv.symm (unop x).snd))
eq₁ :
  (hom
        (((StructuredArrow.Hom.right f).app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).app
          (op (F.obj (unop (unop x).fst)))))
      ((hom
          (((compULiftYonedaIsoULiftYonedaCompLan F).hom.app (unop (unop x).fst)).app (op (F.obj (unop (unop x).fst)))))
        { down := 𝟙 (F.obj (unop (unop x).fst)) }) =
    (hom (((StructuredArrow.hom Φ).app (unop (unop x).fst)).app (op (F.obj (unop (unop x).fst)))))
      { down := 𝟙 (F.obj (unop (unop x).fst)) }
eq₂ :
  (hom
        (((StructuredArrow.Hom.right g).app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).app
          (op (F.obj (unop (unop x).fst)))))
      ((hom
          (((compULiftYonedaIsoULiftYonedaCompLan F).hom.app (unop (unop x).fst)).app (op (F.obj (unop (unop x).fst)))))
        { down := 𝟙 (F.obj (unop (unop x).fst)) }) =
    (hom (((StructuredArrow.hom Φ).app (unop (unop x).fst)).app (op (F.obj (unop (unop x).fst)))))
      { down := 𝟙 (F.obj (unop (unop x).fst)) }
⊢ F.op.lan.map (uliftYonedaEquiv.symm (unop x).snd) ≫ (StructuredArrow.Hom.right f).app P =
    F.op.lan.map (uliftYonedaEquiv.symm (unop x).snd) ≫ (StructuredArrow.Hom.right g).app P