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
E E' : L.RightExtension F
Y : D
⊢ Subsingleton (E.IsPointwiseRightKanExtensionAt Y)

Tactic:
inferInstanceAs (Subsingleton (IsLimit _))

Premises used: _private.0.CategoryTheory.Functor.RightExtension.instSubsingletonIsPointwiseRightKanExtensionAt._proof_1
-- 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
E : L.RightExtension F
Y : D
h : E.IsPointwiseRightKanExtensionAt Y
⊢ L.HasPointwiseRightKanExtensionAt F Y

Tactic:
⟨_, h⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- 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
E : L.RightExtension F
X : C
h : E.IsPointwiseRightKanExtensionAt (L.obj X)
inst_3 : L.Full
inst_4 : L.Faithful
⊢ IsIso ((CostructuredArrow.hom E).app X)

Tactic:
simpa using h.isIso_π_app_of_isInitial _ StructuredArrow.mkIdInitial

Premises used: CategoryTheory.StructuredArrow.mkIdInitial, CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial
-- 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
E E' : L.RightExtension F
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseRightKanExtensionAt Y
⊢ (fun (h : E.IsPointwiseRightKanExtensionAt Y') ↦ E.isPointwiseRightKanExtensionAtOfIso' h e.symm)
      ((fun (h : E.IsPointwiseRightKanExtensionAt Y) ↦ E.isPointwiseRightKanExtensionAtOfIso' h e) h) =
    h

Tactic:
subsingleton
-- 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
E E' : L.RightExtension F
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseRightKanExtensionAt Y'
⊢ (fun (h : E.IsPointwiseRightKanExtensionAt Y) ↦ E.isPointwiseRightKanExtensionAtOfIso' h e)
      ((fun (h : E.IsPointwiseRightKanExtensionAt Y') ↦ E.isPointwiseRightKanExtensionAtOfIso' h e.symm) h) =
    h

Tactic:
subsingleton
-- 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
E : L.RightExtension F
Y : D
h : E.IsPointwiseRightKanExtensionAt Y
T : H
f g : T ⟶ (CostructuredArrow.left E).obj Y
hfg :
  ∀ ⦃X : C⦄ (φ : Y ⟶ L.obj X),
    f ≫ (CostructuredArrow.left E).map φ ≫ (CostructuredArrow.hom E).app X =
      g ≫ (CostructuredArrow.left E).map φ ≫ (CostructuredArrow.hom E).app X
⊢ f = g

Tactic:
h.hom_ext (fun j ↦ hfg j.hom)

Premises used: CategoryTheory.StructuredArrow.hom, CategoryTheory.Limits.IsLimit.hom_ext
-- 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
E : L.RightExtension F
Y : D
h : E.IsPointwiseRightKanExtensionAt Y
inst_3 : HasLimit (StructuredArrow.proj Y L ⋙ F)
g : StructuredArrow Y L
⊢ CategoryStruct.comp (Y := limit (StructuredArrow.proj Y L ⋙ F)) (Iso.hom h.isoLimit)
      (limit.π (StructuredArrow.proj Y L ⋙ F) g) =
    (CostructuredArrow.left E).map g.hom ≫ (CostructuredArrow.hom E).app g.right

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.limit
-- 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
E : L.RightExtension F
Y : D
h : E.IsPointwiseRightKanExtensionAt Y
inst_3 : HasLimit (StructuredArrow.proj Y L ⋙ F)
g : StructuredArrow Y L
⊢ Eq (α := limit (StructuredArrow.proj Y L ⋙ F) ⟶ F.obj g.right)
    (Iso.inv h.isoLimit ≫ (CostructuredArrow.left E).map g.hom ≫ (CostructuredArrow.hom E).app g.right)
    (limit.π (StructuredArrow.proj Y L ⋙ F) g)

Tactic:
simpa using h.conePointUniqueUpToIso_inv_comp (limit.isLimit _) g

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_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
E E' : L.RightExtension F
e : E ≅ E'
h : E.IsPointwiseRightKanExtension
⊢ (fun (h : E'.IsPointwiseRightKanExtension) (Y : D) ↦
        (((isPointwiseRightKanExtensionAtEquivOfIso e Y).symm :
              (a : E'.IsPointwiseRightKanExtensionAt Y) → E.IsPointwiseRightKanExtensionAt Y)
            (h Y) :
          E.IsPointwiseRightKanExtensionAt Y))
      ((fun (h : E.IsPointwiseRightKanExtension) (Y : D) ↦
          ((isPointwiseRightKanExtensionAtEquivOfIso e Y :
                (a : E.IsPointwiseRightKanExtensionAt Y) → E'.IsPointwiseRightKanExtensionAt Y)
              (h Y) :
            E'.IsPointwiseRightKanExtensionAt Y))
        h) =
    h

Tactic:
simp
-- 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
E E' : L.RightExtension F
e : E ≅ E'
h : E'.IsPointwiseRightKanExtension
⊢ (fun (h : E.IsPointwiseRightKanExtension) (Y : D) ↦
        ((isPointwiseRightKanExtensionAtEquivOfIso e Y :
              (a : E.IsPointwiseRightKanExtensionAt Y) → E'.IsPointwiseRightKanExtensionAt Y)
            (h Y) :
          E'.IsPointwiseRightKanExtensionAt Y))
      ((fun (h : E'.IsPointwiseRightKanExtension) (Y : D) ↦
          (((isPointwiseRightKanExtensionAtEquivOfIso e Y).symm :
                (a : E'.IsPointwiseRightKanExtensionAt Y) → E.IsPointwiseRightKanExtensionAt Y)
              (h Y) :
            E.IsPointwiseRightKanExtensionAt Y))
        h) =
    h

Tactic:
simp
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
⊢ L.HasPointwiseRightKanExtension F

Tactic:
fun Y => (h Y).hasPointwiseRightKanExtensionAt

Premises used: CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt
-- 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
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : StructuredArrow Y₂ L
rw :
  (CostructuredArrow.left G).map φ ≫ (G.coneAt Y₂).π.app X =
    ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app X
⊢ ((CostructuredArrow.left G).map φ ≫ (h Y₂).lift (G.coneAt Y₂)) ≫ (E.coneAt Y₂).π.app X =
    ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app X

Tactic:
rw [assoc, (h Y₂).fac (coneAt G Y₂) X]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.RightExtension.coneAt, CategoryTheory.Limits.IsLimit.fac
-- 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
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : StructuredArrow Y₂ L
⊢ (CostructuredArrow.left G).map φ ≫ (G.coneAt Y₂).π.app X =
    ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app X

Tactic:
simpa using ((h Y₁).fac (coneAt G Y₁) ((StructuredArrow.map φ).obj X)).symm

Premises used: CategoryTheory.StructuredArrow.map, Eq.symm, CategoryTheory.Functor.RightExtension.coneAt, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.fac
-- 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
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
w :
  ∀ (X : C),
    NatTrans.app
        (map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
          CostructuredArrow.hom E)
        X =
      (CostructuredArrow.hom G).app X
⊢ map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
      CostructuredArrow.hom E =
    CostructuredArrow.hom G

Tactic:
ext X
-- 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
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
X : C
⊢ NatTrans.app
      (map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
        CostructuredArrow.hom E)
      X =
    (CostructuredArrow.hom G).app X

Tactic:
simpa using (h (L.obj X)).fac (RightExtension.coneAt G _) (StructuredArrow.mk (𝟙 _))

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.StructuredArrow.mk, CategoryTheory.Functor.RightExtension.coneAt, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.fac
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
h₁ : ∀ (Y : D), f₁.left.app Y = f₂.left.app Y
⊢ f₁ = f₂

Tactic:
ext Y
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
h₁ : ∀ (j : StructuredArrow Y L), f₁.left.app Y ≫ (E.coneAt Y).π.app j = f₂.left.app Y ≫ (E.coneAt Y).π.app j
⊢ f₁.left.app Y = f₂.left.app Y

Tactic:
apply (h Y).hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
⊢ Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
    ((map (obj (whiskeringLeft C D H) L) f₁.left ≫ CostructuredArrow.hom E).app X.right)
    ((CostructuredArrow.hom G).app X.right)

Tactic:
have eq₁ := congr_app (CostructuredArrow.w f₁) X.right
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ :
  Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
    ((map (obj (whiskeringLeft C D H) L) f₁.left ≫ CostructuredArrow.hom E).app X.right)
    ((CostructuredArrow.hom G).app X.right)
⊢ Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
    ((map (obj (whiskeringLeft C D H) L) f₂.left ≫ CostructuredArrow.hom E).app X.right)
    ((CostructuredArrow.hom G).app X.right)

Tactic:
have eq₂ := congr_app (CostructuredArrow.w f₂) X.right
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ :
  Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
    ((map (obj (whiskeringLeft C D H) L) f₁.left ≫ CostructuredArrow.hom E).app X.right)
    ((CostructuredArrow.hom G).app X.right)
eq₂ :
  Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
    ((map (obj (whiskeringLeft C D H) L) f₂.left ≫ CostructuredArrow.hom E).app X.right)
    ((CostructuredArrow.hom G).app X.right)
h₁ :
  f₁.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right =
    f₂.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

Tactic:
dsimp at eq₁ eq₂ ⊢
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ :
  Eq (α := G.left.obj (L.obj X.right) ⟶ F.obj X.right)
    (f₁.left.app (L.obj X.right) ≫ (CostructuredArrow.hom E).app X.right) ((CostructuredArrow.hom G).app X.right)
eq₂ :
  Eq (α := G.left.obj (L.obj X.right) ⟶ F.obj X.right)
    (f₂.left.app (L.obj X.right) ≫ (CostructuredArrow.hom E).app X.right) ((CostructuredArrow.hom G).app X.right)
⊢ f₁.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right =
    f₂.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right

Tactic:
simp only [← NatTrans.naturality_assoc, eq₁, eq₂]

Premises used: CategoryTheory.NatTrans.naturality_assoc
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
⊢ L.HasRightKanExtension F

Tactic:
have := h.isRightKanExtension
  HasRightKanExtension.mk E.left E.hom

Premises used: CategoryTheory.Functor.HasRightKanExtension.mk, CategoryTheory.CostructuredArrow.hom, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isRightKanExtension, CategoryTheory.CostructuredArrow.left
-- 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
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
inst_3 : L.Full
inst_4 : L.Faithful
⊢ IsIso (CostructuredArrow.hom E)

Tactic:
have := fun X => (h (L.obj X)).isIso_hom_app
  NatIso.isIso_of_isIso_app ..

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app, CategoryTheory.CostructuredArrow.hom, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app, CategoryTheory.Functor.obj
-- 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₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : CostructuredArrow L Y₁
φ : g₁ ⟶ g₂
⊢ Eq (α :=
    (CostructuredArrow.proj L Y₁ ⋙ F).obj g₁ ⟶
      obj (obj (const (CostructuredArrow L Y₁)) (colimit (CostructuredArrow.proj L Y₂ ⋙ F))) g₂)
    ((CostructuredArrow.proj L Y₁ ⋙ F).map φ ≫
      colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) (obj (CostructuredArrow.map f) g₂))
    (colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) (obj (CostructuredArrow.map f) g₁) ≫
      map (obj (const (CostructuredArrow L Y₁)) (colimit (CostructuredArrow.proj L Y₂ ⋙ F))) φ)

Tactic:
simpa using colimit.w (CostructuredArrow.proj L Y₂ ⋙ F)
              ((CostructuredArrow.map f).map φ)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map, CategoryTheory.Limits.colimit.w, CategoryTheory.CostructuredArrow.map, 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
Y : D
j : CostructuredArrow L Y
dsimp :
  CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y ⋙ F)) (colimit.ι (CostructuredArrow.proj L Y ⋙ F) j)
      (colimit.desc (CostructuredArrow.proj L Y ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y ⋙ F),
          ι :=
            {
              app := fun (g : CostructuredArrow L Y) ↦
                colimit.ι (CostructuredArrow.proj L Y ⋙ F) (obj (CostructuredArrow.map (𝟙 Y)) g),
              naturality := ⋯ } }) =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L Y ⋙ F))
⊢ CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y ⋙ F)) (colimit.ι (CostructuredArrow.proj L Y ⋙ F) j)
      (colimit.desc (CostructuredArrow.proj L Y ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y ⋙ F),
          ι :=
            {
              app := fun (g : CostructuredArrow L Y) ↦
                colimit.ι (CostructuredArrow.proj L Y ⋙ F) (obj (CostructuredArrow.map (𝟙 Y)) g),
              naturality := ⋯ } }) =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L Y ⋙ F))

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
Y : D
j : CostructuredArrow L Y
simp :
  Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y ⋙ F) (obj (CostructuredArrow.map (𝟙 Y)) j))
    (colimit.ι (CostructuredArrow.proj L Y ⋙ F) j)
⊢ CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y ⋙ F)) (colimit.ι (CostructuredArrow.proj L Y ⋙ F) j)
      (colimit.desc (CostructuredArrow.proj L Y ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y ⋙ F),
          ι :=
            {
              app := fun (g : CostructuredArrow L Y) ↦
                colimit.ι (CostructuredArrow.proj L Y ⋙ F) (obj (CostructuredArrow.map (𝟙 Y)) g),
              naturality := ⋯ } }) =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L Y ⋙ F))

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

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.colimit.ι_desc
-- 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 : D
j : CostructuredArrow L Y
h : obj (CostructuredArrow.map (𝟙 Y)) j = j
⊢ Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y ⋙ F) (obj (CostructuredArrow.map (𝟙 Y)) j))
    (colimit.ι (CostructuredArrow.proj L Y ⋙ 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.HasPointwiseLeftKanExtension F
Y : D
j : CostructuredArrow L Y
⊢ obj (CostructuredArrow.map (𝟙 Y)) j = j

Tactic:
apply CostructuredArrow.map_id

Premises used: CategoryTheory.CostructuredArrow.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.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
h : obj (CostructuredArrow.map (f ≫ f')) j = obj (CostructuredArrow.map f') (obj (CostructuredArrow.map f) j)
⊢ Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map (f ≫ f')) j) :
      (CostructuredArrow.proj L Y₃ ⋙ F).obj (obj (CostructuredArrow.map (f ≫ f')) j) ⟶
        colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map f') (obj (CostructuredArrow.map f) j)))

Tactic:
congr 1