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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseLeftKanExtensionAt F Y
rw : (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj Y)
⊢ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
rw [← hasPointwiseLeftKanExtensionAt_iff_of_natIso F eL,
    hasPointwiseLeftKanExtensionAt_iff_of_iso _ F e.symm]

Premises used: CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_natIso, CategoryTheory.Iso.symm, CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L Y ⥤ CostructuredArrow (L ⋙ E.functor) (E.functor.obj Y) := CostructuredArrow.post L E.functor Y
⊢ HasColimit (Φ.asEquivalence.functor ⋙ CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F)

Tactic:
have : HasColimit ((asEquivalence Φ).functor ⋙
    CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F) :=
    (inferInstance : HasPointwiseLeftKanExtensionAt L F Y)
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L Y ⥤ CostructuredArrow (L ⋙ E.functor) (E.functor.obj Y) := CostructuredArrow.post L E.functor Y
this : HasColimit (Φ.asEquivalence.functor ⋙ CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F)
⊢ (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj Y)

Tactic:
hasColimit_of_equivalence_comp (asEquivalence Φ)

Premises used: CategoryTheory.Limits.hasColimit_of_equivalence_comp, CategoryTheory.Functor.asEquivalence
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L Y ⥤ CostructuredArrow (L ⋙ E.functor) (E.functor.obj Y) := CostructuredArrow.post L E.functor Y
this : HasColimit (Φ.asEquivalence.functor ⋙ CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F)
⊢ (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj Y)

Tactic:
exact hasColimit_of_equivalence_comp (asEquivalence Φ)

Premises used: CategoryTheory.Limits.hasColimit_of_equivalence_comp, CategoryTheory.Functor.asEquivalence
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
mp : L.HasPointwiseLeftKanExtensionAt F Y → L'.HasPointwiseLeftKanExtensionAt F Y'
mpr : L'.HasPointwiseLeftKanExtensionAt F Y' → L.HasPointwiseLeftKanExtensionAt F Y
⊢ L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
constructor
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
h : L.HasPointwiseLeftKanExtensionAt F Y
⊢ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
hasPointwiseLeftKanExtensionAt_of_equivalence L L' F E eL Y Y' e

Premises used: CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_of_equivalence
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
h : L.HasPointwiseLeftKanExtensionAt F Y
⊢ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
exact hasPointwiseLeftKanExtensionAt_of_equivalence L L' F E eL Y Y' e

Premises used: CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_of_equivalence
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
h : L'.HasPointwiseLeftKanExtensionAt F Y'
⊢ L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
hasPointwiseLeftKanExtensionAt_of_equivalence L' L F E.symm
      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.associator, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_of_equivalence, CategoryTheory.Equivalence.inverse
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseRightKanExtensionAt F Y
rw : (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)
⊢ L'.HasPointwiseRightKanExtensionAt F Y'

Tactic:
rw [← hasPointwiseRightKanExtensionAt_iff_of_natIso F eL,
    hasPointwiseRightKanExtensionAt_iff_of_iso _ F e.symm]

Premises used: CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_natIso, CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_iso, CategoryTheory.Iso.symm
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L ⥤ StructuredArrow (E.functor.obj Y) (L ⋙ E.functor) := StructuredArrow.post Y L E.functor
⊢ HasLimit (Φ.asEquivalence.functor ⋙ StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F)

Tactic:
have : HasLimit ((asEquivalence Φ).functor ⋙
    StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F) :=
    (inferInstance : HasPointwiseRightKanExtensionAt L F Y)
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L ⥤ StructuredArrow (E.functor.obj Y) (L ⋙ E.functor) := StructuredArrow.post Y L E.functor
this : HasLimit (Φ.asEquivalence.functor ⋙ StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F)
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)

Tactic:
hasLimit_of_equivalence_comp (asEquivalence Φ)

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Limits.hasLimit_of_equivalence_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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L ⥤ StructuredArrow (E.functor.obj Y) (L ⋙ E.functor) := StructuredArrow.post Y L E.functor
this : HasLimit (Φ.asEquivalence.functor ⋙ StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F)
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)

Tactic:
exact hasLimit_of_equivalence_comp (asEquivalence Φ)

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Limits.hasLimit_of_equivalence_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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
mp : L.HasPointwiseRightKanExtensionAt F Y → L'.HasPointwiseRightKanExtensionAt F Y'
mpr : L'.HasPointwiseRightKanExtensionAt F Y' → L.HasPointwiseRightKanExtensionAt F Y
⊢ L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y'

Tactic:
constructor
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
h : L.HasPointwiseRightKanExtensionAt F Y
⊢ L'.HasPointwiseRightKanExtensionAt F Y'

Tactic:
hasPointwiseRightKanExtensionAt_of_equivalence L L' F E eL Y Y' e

Premises used: CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_of_equivalence
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
h : L.HasPointwiseRightKanExtensionAt F Y
⊢ L'.HasPointwiseRightKanExtensionAt F Y'

Tactic:
exact hasPointwiseRightKanExtensionAt_of_equivalence L L' F E eL Y Y' e

Premises used: CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_of_equivalence
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
h : L'.HasPointwiseRightKanExtensionAt F Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y

Tactic:
hasPointwiseRightKanExtensionAt_of_equivalence L' L F E.symm
      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.associator, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Equivalence.inverse
-- 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 : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
h : L'.HasPointwiseRightKanExtensionAt F Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y

Tactic:
exact hasPointwiseRightKanExtensionAt_of_equivalence L' L F E.symm
      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.associator, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Equivalence.inverse
-- 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 : L.LeftExtension F
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
dsimp :
  F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫ 𝟙 ((StructuredArrow.right E).obj Y)
⊢ (CostructuredArrow.proj L Y ⋙ F).map φ ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫
      map (obj (const (CostructuredArrow L Y)) ((StructuredArrow.right E).obj Y)) φ

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
E : L.LeftExtension F
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
rw :
  F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map (L.map φ.left ≫ g₂.hom)) ≫
      𝟙 ((StructuredArrow.right E).obj Y)
⊢ F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫ 𝟙 ((StructuredArrow.right E).obj Y)

Tactic:
rw [← CostructuredArrow.w φ]

Premises used: CategoryTheory.CostructuredArrow.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
E : L.LeftExtension F
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map (L.map φ.left ≫ g₂.hom)) ≫
      𝟙 ((StructuredArrow.right E).obj Y)

Tactic:
simp only [NatTrans.naturality_assoc, Functor.comp_map,
          Functor.map_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc
-- 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_1 : L.LeftExtension F
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
dsimp :
  ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
    (StructuredArrow.hom E').app G.left ≫ (StructuredArrow.right E').map G.hom
⊢ (E.coconeAt Y).ι.app G ≫ (StructuredArrow.Hom.right φ).app Y = (E'.coconeAt Y).ι.app G

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
E_1 : L.LeftExtension F
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
rw :
  ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
    (StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right φ)).app G.left ≫
      (StructuredArrow.right E').map G.hom
⊢ ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
    (StructuredArrow.hom E').app G.left ≫ (StructuredArrow.right E').map G.hom

Tactic:
rw [← StructuredArrow.w φ]

Premises used: CategoryTheory.StructuredArrow.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
E_1 : L.LeftExtension F
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
⊢ ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
    (StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right φ)).app G.left ≫
      (StructuredArrow.right E').map G.hom

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 : L.LeftExtension F
Y : D
⊢ Subsingleton (E.IsPointwiseLeftKanExtensionAt Y)

Tactic:
inferInstanceAs (Subsingleton (IsColimit _))

Premises used: _private.0.CategoryTheory.Functor.LeftExtension.instSubsingletonIsPointwiseLeftKanExtensionAt._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.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
⊢ L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
⟨_, h⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.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.LeftExtension F
X : C
h : E.IsPointwiseLeftKanExtensionAt (L.obj X)
inst_3 : L.Full
inst_4 : L.Faithful
⊢ IsIso ((StructuredArrow.hom E).app X)

Tactic:
simpa using h.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal

Premises used: CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal, CategoryTheory.CostructuredArrow.mkIdTerminal
-- 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 : L.LeftExtension F
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseLeftKanExtensionAt Y
⊢ (fun (h : E.IsPointwiseLeftKanExtensionAt Y') ↦ E.isPointwiseLeftKanExtensionAtOfIso' h e.symm)
      ((fun (h : E.IsPointwiseLeftKanExtensionAt Y) ↦ E.isPointwiseLeftKanExtensionAtOfIso' 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 : L.LeftExtension F
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseLeftKanExtensionAt Y'
⊢ (fun (h : E.IsPointwiseLeftKanExtensionAt Y) ↦ E.isPointwiseLeftKanExtensionAtOfIso' h e)
      ((fun (h : E.IsPointwiseLeftKanExtensionAt Y') ↦ E.isPointwiseLeftKanExtensionAtOfIso' h e.symm) h) =
    h

Tactic:
subsingleton