awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ obj (CostructuredArrow.map (f ≫ f')) j = obj (CostructuredArrow.map f') (obj (CostructuredArrow.map f) j)

Tactic:
apply CostructuredArrow.map_comp

Premises used: CategoryTheory.CostructuredArrow.map_comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
simp :
  Eq (α := F.obj X₁ ⟶ colimit (J := CostructuredArrow L (L.obj X₂)) (CostructuredArrow.proj L (L.obj X₂) ⋙ F))
    (F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))))
    (colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁) ≫ L.map f)))
⊢ F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) =
    colimit.ι (CostructuredArrow.proj L (L.obj X₁) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁))) ≫
      (L ⋙ L.pointwiseLeftKanExtension F).map f

Tactic:
simp only [comp_obj, pointwiseLeftKanExtension_obj, comp_map,
      pointwiseLeftKanExtension_map, colimit.ι_desc, CostructuredArrow.map_mk]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.pointwiseLeftKanExtension_obj, CategoryTheory.Functor.pointwiseLeftKanExtension_map, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.CostructuredArrow.map_mk, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
rw :
  Eq (α := F.obj X₁ ⟶ colimit (J := CostructuredArrow L (L.obj X₂)) (CostructuredArrow.proj L (L.obj X₂) ⋙ F))
    (F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))))
    (colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f)))
⊢ Eq (α := F.obj X₁ ⟶ colimit (J := CostructuredArrow L (L.obj X₂)) (CostructuredArrow.proj L (L.obj X₂) ⋙ F))
    (F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))))
    (colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁) ≫ L.map f)))

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : CostructuredArrow.mk (L.map f) ⟶ CostructuredArrow.mk (𝟙 (L.obj X₂)) := CostructuredArrow.homMk f ⋯
⊢ Eq (α := F.obj X₁ ⟶ colimit (J := CostructuredArrow L (L.obj X₂)) (CostructuredArrow.proj L (L.obj X₂) ⋙ F))
    (F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))))
    (colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f)))

Tactic:
colimit.w (CostructuredArrow.proj L (L.obj X₂) ⋙ F) φ

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.w, CategoryTheory.Functor.obj, CategoryTheory.CostructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : CostructuredArrow.mk (L.map f) ⟶ CostructuredArrow.mk (𝟙 (L.obj X₂)) := CostructuredArrow.homMk f ⋯
⊢ Eq (α := F.obj X₁ ⟶ colimit (J := CostructuredArrow L (L.obj X₂)) (CostructuredArrow.proj L (L.obj X₂) ⋙ F))
    (F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))))
    (colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f)))

Tactic:
exact colimit.w (CostructuredArrow.proj L (L.obj X₂) ⋙ F) φ

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.w, CategoryTheory.Functor.obj, CategoryTheory.CostructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
dsimp :
  colimit.ι (CostructuredArrow.proj L X ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L X ⋙ F)) =
    CategoryStruct.comp (Y :=
      colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F))
      (colimit.ι (CostructuredArrow.proj L (L.obj j.left) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left))) :
        obj (CostructuredArrow.proj L (L.obj j.left) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left))) ⟶
          colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F))
      (colimit.desc (CostructuredArrow.proj L (L.obj j.left) ⋙ F)
          { pt := colimit (CostructuredArrow.proj L X ⋙ F),
            ι :=
              {
                app := fun (g : CostructuredArrow L (L.obj j.left)) ↦
                  colimit.ι (CostructuredArrow.proj L X ⋙ F) (obj (CostructuredArrow.map j.hom) g),
                naturality := ⋯ } } :
        colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F) ⟶
          Cocone.pt (J := CostructuredArrow L (L.obj j.left)) (F := CostructuredArrow.proj L (L.obj j.left) ⋙ F)
            { pt := colimit (CostructuredArrow.proj L X ⋙ F),
              ι :=
                {
                  app := fun (g : CostructuredArrow L (L.obj j.left)) ↦
                    colimit.ι (CostructuredArrow.proj L X ⋙ F) (obj (CostructuredArrow.map j.hom) g),
                  naturality := ⋯ } })
⊢ (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).ι.app j ≫
      Iso.hom (Iso.refl (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).pt) =
    ((LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F)).coconeAt X).ι.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
simp :
  Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L X ⋙ F)) (colimit.ι (CostructuredArrow.proj L X ⋙ F) j)
    (colimit.ι (CostructuredArrow.proj L X ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)))
⊢ colimit.ι (CostructuredArrow.proj L X ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L X ⋙ F)) =
    CategoryStruct.comp (Y :=
      colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F))
      (colimit.ι (CostructuredArrow.proj L (L.obj j.left) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left))) :
        obj (CostructuredArrow.proj L (L.obj j.left) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left))) ⟶
          colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F))
      (colimit.desc (CostructuredArrow.proj L (L.obj j.left) ⋙ F)
          { pt := colimit (CostructuredArrow.proj L X ⋙ F),
            ι :=
              {
                app := fun (g : CostructuredArrow L (L.obj j.left)) ↦
                  colimit.ι (CostructuredArrow.proj L X ⋙ F) (obj (CostructuredArrow.map j.hom) g),
                naturality := ⋯ } } :
        colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F) ⟶
          Cocone.pt (J := CostructuredArrow L (L.obj j.left)) (F := CostructuredArrow.proj L (L.obj j.left) ⋙ F)
            { pt := colimit (CostructuredArrow.proj L X ⋙ F),
              ι :=
                {
                  app := fun (g : CostructuredArrow L (L.obj j.left)) ↦
                    colimit.ι (CostructuredArrow.proj L X ⋙ F) (obj (CostructuredArrow.map j.hom) g),
                  naturality := ⋯ } })

Tactic:
simp only [comp_id, colimit.ι_desc, CostructuredArrow.map_mk]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.CostructuredArrow.map_mk
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
h : j = CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)
⊢ Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L X ⋙ F)) (colimit.ι (CostructuredArrow.proj L X ⋙ F) j)
    (colimit.ι (CostructuredArrow.proj L X ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
h : j = CostructuredArrow.mk j.hom
h₁ h₂ : j = j
⊢ j = CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)

Tactic:
rw [id_comp, ← CostructuredArrow.eq_mk]

Premises used: CategoryTheory.CostructuredArrow.eq_mk, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
⊢ L.HasLeftKanExtension F

Tactic:
HasLeftKanExtension.mk _ (pointwiseLeftKanExtensionUnit L F)

Premises used: CategoryTheory.Functor.pointwiseLeftKanExtensionUnit, CategoryTheory.Functor.HasLeftKanExtension.mk
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : F ⟶ L ⋙ G
Y : D
⊢ ∀ ⦃X Y_1 : CostructuredArrow L Y⦄ (f : X ⟶ Y_1),
    (CostructuredArrow.proj L Y ⋙ F).map f ≫ α.app Y_1.left ≫ G.map Y_1.hom =
      (α.app X.left ≫ G.map X.hom) ≫ map (obj (const (CostructuredArrow L Y)) (G.obj Y)) f

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseLeftKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun (Y : D) ↦ colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
hγ :
  L.pointwiseLeftKanExtensionUnit F ≫
      L.whiskerLeft ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α) =
    L.pointwiseLeftKanExtensionUnit F ≫ L.whiskerLeft β
⊢ (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α = β

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

Premises used: CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.Functor.pointwiseLeftKanExtensionUnit
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseLeftKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun (Y : D) ↦ colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ L.pointwiseLeftKanExtensionUnit F ≫
      L.whiskerLeft ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α) =
    L.pointwiseLeftKanExtensionUnit F ≫ L.whiskerLeft β

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseLeftKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun (Y : D) ↦ colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α = β

Tactic:
have h : (pointwiseLeftKanExtension L F).descOfIsLeftKanExtension
      (pointwiseLeftKanExtensionUnit L F) G α = β := by
    apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)
    aesop
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseLeftKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun (Y : D) ↦ 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:
NatTrans.congr_app h Y

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Limits.colimit.desc
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseLeftKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun (Y : D) ↦ 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

Premises used: CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : StructuredArrow Y₂ L
φ : g₁ ⟶ g₂
⊢ Eq.{v_4 + 1} (α :=
    obj (obj (const (StructuredArrow Y₂ L)) (limit (StructuredArrow.proj Y₁ L ⋙ F))) g₁ ⟶
      (StructuredArrow.proj Y₂ L ⋙ F).obj g₂)
    (map (obj (const (StructuredArrow Y₂ L)) (limit (StructuredArrow.proj Y₁ L ⋙ F))) φ ≫
      limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) g₂))
    (limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) g₁) ≫ (StructuredArrow.proj Y₂ L ⋙ F).map φ)

Tactic:
simpa using (limit.w (StructuredArrow.proj Y₁ L ⋙ F)
              ((StructuredArrow.map f).map φ)).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.StructuredArrow.map, CategoryTheory.Functor.map, Eq.symm, CategoryTheory.StructuredArrow.proj, CategoryTheory.Limits.limit.w
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
dsimp :
  CategoryStruct.comp (Y := limit (StructuredArrow.proj Y L ⋙ F))
      (limit.lift (StructuredArrow.proj Y L ⋙ F)
        { pt := limit (StructuredArrow.proj Y L ⋙ F),
          π :=
            {
              app := fun (g : StructuredArrow Y L) ↦
                limit.π (StructuredArrow.proj Y L ⋙ F) (obj (StructuredArrow.map (𝟙 Y)) g),
              naturality := ⋯ } })
      (limit.π (StructuredArrow.proj Y L ⋙ F) j) =
    𝟙 (limit (StructuredArrow.proj Y L ⋙ F)) ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j
⊢ CategoryStruct.comp (Y := limit (StructuredArrow.proj Y L ⋙ F))
      (limit.lift (StructuredArrow.proj Y L ⋙ F)
        { pt := limit (StructuredArrow.proj Y L ⋙ F),
          π :=
            {
              app := fun (g : StructuredArrow Y L) ↦
                limit.π (StructuredArrow.proj Y L ⋙ F) (obj (StructuredArrow.map (𝟙 Y)) g),
              naturality := ⋯ } })
      (limit.π (StructuredArrow.proj Y L ⋙ F) j) =
    𝟙 (limit (StructuredArrow.proj Y L ⋙ F)) ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
simp :
  Eq (α := limit (StructuredArrow.proj Y L ⋙ F) ⟶ F.obj j.right)
    (limit.π (StructuredArrow.proj Y L ⋙ F) (obj (StructuredArrow.map (𝟙 Y)) j))
    (limit.π (StructuredArrow.proj Y L ⋙ F) j)
⊢ CategoryStruct.comp (Y := limit (StructuredArrow.proj Y L ⋙ F))
      (limit.lift (StructuredArrow.proj Y L ⋙ F)
        { pt := limit (StructuredArrow.proj Y L ⋙ F),
          π :=
            {
              app := fun (g : StructuredArrow Y L) ↦
                limit.π (StructuredArrow.proj Y L ⋙ F) (obj (StructuredArrow.map (𝟙 Y)) g),
              naturality := ⋯ } })
      (limit.π (StructuredArrow.proj Y L ⋙ F) j) =
    𝟙 (limit (StructuredArrow.proj Y L ⋙ F)) ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j

Tactic:
simp only [limit.lift_π, id_comp]

Premises used: CategoryTheory.Limits.limit.lift_π, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
h : obj (StructuredArrow.map (𝟙 Y)) j = j
⊢ Eq (α := limit (StructuredArrow.proj Y L ⋙ F) ⟶ F.obj j.right)
    (limit.π (StructuredArrow.proj Y L ⋙ F) (obj (StructuredArrow.map (𝟙 Y)) j))
    (limit.π (StructuredArrow.proj Y L ⋙ F) j)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
⊢ obj (StructuredArrow.map (𝟙 Y)) j = j

Tactic:
apply StructuredArrow.map_id

Premises used: CategoryTheory.StructuredArrow.map_id
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : StructuredArrow Y₃ L
h : obj (StructuredArrow.map (f ≫ f')) j = obj (StructuredArrow.map f) (obj (StructuredArrow.map f') j)
⊢ Eq (α := limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶ F.obj j.right)
    (limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map (f ≫ f')) j) :
      limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶
        (StructuredArrow.proj Y₁ L ⋙ F).obj (obj (StructuredArrow.map (f ≫ f')) j))
    (limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) (obj (StructuredArrow.map f') j)))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : StructuredArrow Y₃ L
⊢ obj (StructuredArrow.map (f ≫ f')) j = obj (StructuredArrow.map f) (obj (StructuredArrow.map f') j)

Tactic:
apply StructuredArrow.map_comp

Premises used: CategoryTheory.StructuredArrow.map_comp