-- Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@[simp]
lemma pointwiseRightKanExtension_lift_app (G : D ⥤ H) (α : L ⋙ G ⟶ F) (Y : D) :
    ((pointwiseRightKanExtension L F).liftOfIsRightKanExtension
      (pointwiseRightKanExtensionCounit L F) G α |>.app Y) =
        limit.lift _ (structuredArrowMapCone 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.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)

Tactic:
let β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y ↦ limit.lift _ (structuredArrowMapCone 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.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y => limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone 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.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y => limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ whiskerLeft L
        ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α) ≫
      L.pointwiseRightKanExtensionCounit F =
    whiskerLeft L β ≫ L.pointwiseRightKanExtensionCounit F

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.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y => limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
h : (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)

Tactic:
exact NatTrans.congr_app h Y

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.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y => limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β

Tactic:
apply hom_ext_of_isRightKanExtension (α := pointwiseRightKanExtensionCounit 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.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y => limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ whiskerLeft L
        ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α) ≫
      L.pointwiseRightKanExtensionCounit F =
    whiskerLeft L β ≫ L.pointwiseRightKanExtensionCounit F

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.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y => limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)

Tactic:
have h : (pointwiseRightKanExtension L F).liftOfIsRightKanExtension
    (pointwiseRightKanExtensionCounit L F) G α = β := by
  apply hom_ext_of_isRightKanExtension (α := pointwiseRightKanExtensionCounit 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.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y => limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
h : (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)