Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
eq₁ :
  (hom
        (((yoneda.obj (F.obj Y) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))
              (F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := F.map f } =
    (hom ((F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁})).app (op X))) { down := f }
eq₃ :
  (hom ((F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁})).app (op X))) { down := 𝟙 X ≫ f } =
    (hom ((F.op.lan.map (Functor.whiskerRight (yoneda.map f) uliftFunctor.{max w v₂, v₁})).app (op (F.obj X))))
      ((hom ((F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁})).app (op X))) { down := 𝟙 X })
eq₂ :
  (hom
        (((yoneda.obj (F.obj X) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))
              (F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := 𝟙 (F.obj X) } =
    (hom ((F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁})).app (op X))) { down := 𝟙 X }
⊢ (hom
        (((yoneda.obj (F.obj Y) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁}))
              (𝟙 (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁}) ≫
                F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := 𝟙 (F.obj X) ≫ F.map f } =
    (hom ((F.op.lan.map (Functor.whiskerRight (yoneda.map f) uliftFunctor.{max w v₂, v₁})).app (op (F.obj X))))
      ((hom
          (((yoneda.obj (F.obj X) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
                { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
                (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁}))
                (𝟙 (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁}) ≫
                  F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))).app
            (op (F.obj X))))
        { down := 𝟙 (F.obj X) })

Tactic:
simp only [id_comp] at eq₃

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
eq₁ :
  (hom
        (((yoneda.obj (F.obj Y) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))
              (F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := F.map f } =
    (hom ((F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁})).app (op X))) { down := f }
eq₂ :
  (hom
        (((yoneda.obj (F.obj X) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))
              (F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := 𝟙 (F.obj X) } =
    (hom ((F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁})).app (op X))) { down := 𝟙 X }
eq₃ :
  (hom ((F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁})).app (op X))) { down := f } =
    (hom ((F.op.lan.map (Functor.whiskerRight (yoneda.map f) uliftFunctor.{max w v₂, v₁})).app (op (F.obj X))))
      ((hom ((F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁})).app (op X))) { down := 𝟙 X })
⊢ (hom
        (((yoneda.obj (F.obj Y) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁}))
              (𝟙 (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁}) ≫
                F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := 𝟙 (F.obj X) ≫ F.map f } =
    (hom ((F.op.lan.map (Functor.whiskerRight (yoneda.map f) uliftFunctor.{max w v₂, v₁})).app (op (F.obj X))))
      ((hom
          (((yoneda.obj (F.obj X) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
                { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
                (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁}))
                (𝟙 (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁}) ≫
                  F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))).app
            (op (F.obj X))))
        { down := 𝟙 (F.obj X) })