-- Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@[simp]
lemma pointwiseLeftKanExtension_desc_app (G : D ⥤ H) (α :  F ⟶ L ⋙ G) (Y : D) :
    ((pointwiseLeftKanExtension L F).descOfIsLeftKanExtension (pointwiseLeftKanExtensionUnit L F)
      G α |>.app Y) = colimit.desc _ (costructuredArrowMapCocone L F G α Y)

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y => colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Tactic:
have h : (pointwiseLeftKanExtension L F).descOfIsLeftKanExtension
    (pointwiseLeftKanExtensionUnit L F) G α = β := by
  apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)
  aesop

Result:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y => colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
h : (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α = β
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Tactic:
let β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y ↦ colimit.desc _ (costructuredArrowMapCocone L F G α Y) }

Result:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y => colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Proof state:
case hγ
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y => colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ L.pointwiseLeftKanExtensionUnit F ≫
      whiskerLeft L ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α) =
    L.pointwiseLeftKanExtensionUnit F ≫ whiskerLeft L β

Tactic:
aesop

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y => colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α = β

Tactic:
apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)

Result:
case hγ
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y => colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ L.pointwiseLeftKanExtensionUnit F ≫
      whiskerLeft L ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α) =
    L.pointwiseLeftKanExtensionUnit F ≫ whiskerLeft L β

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y => colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
h : (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α = β
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Tactic:
exact NatTrans.congr_app h Y

Result:
no goals