awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
hφ :
  ∀ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) (j : CostructuredArrow F Y),
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s =
      (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
m : ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt ⟶ s.pt
hm : ∀ (j : CostructuredArrow F Y), ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).ι.app j ≫ m = s.ι.app j
unop : C
down : obj (obj yoneda ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt) (F.op.obj (op unop))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map m).app (op unop)))
      { down := down :
        ULift.{w, v₂}
          (obj (obj yoneda ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt) (F.op.obj (op unop))) } =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (h.preimage (φ s))).app (op unop)))
      { down := down :
        ULift.{w, v₂}
          (obj (obj yoneda ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt) (F.op.obj (op unop))) }

Tactic:
simp [φ, ← hm]
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
hφ :
  ∀ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) (j : CostructuredArrow F Y),
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s =
      (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)
⊢ F.isDenseAt Y

Tactic:
exact
      ⟨{desc s := (h.preimage (φ s))
        fac s j := h.map_injective (by simp [hφ])
        uniq s m hm := h.map_injective (by
          ext ⟨_⟩ ⟨_⟩
          simp [φ, ← hm]) }⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
⊢ F.IsDense ↔ Nonempty (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful

Tactic:
⟨fun _ ↦ ⟨FullyFaithful.ofFullyFaithful _⟩,
    fun ⟨h⟩ ↦ IsDense.of_fullyFaithful_restrictedULiftYoneda h⟩

Premises used: _private.0.CategoryTheory.Functor.isDense_iff_fullyFaithful_restrictedULiftYoneda.match_1, Nonempty.intro, CategoryTheory.Presheaf.restrictedULiftYoneda, CategoryTheory.Functor.IsDense, Iff.intro, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful, CategoryTheory.Functor.IsDense.of_fullyFaithful_restrictedULiftYoneda
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsDense
Y : D
⊢ ∀ (j : ShrinkHoms.{max (max u₁ v₁) v₂} (Shrink.{max (max u₁ v₁) v₂, max u₁ v₂} (CostructuredArrow F Y))),
    ofObj.{v₂, u₂, u₁} F.obj
      (obj
        (Equivalence.functor
            (Equivalence.trans
              (Equivalence.symm
                (ShrinkHoms.equivalence (Shrink.{max (max u₁ v₁) v₂, max u₁ v₂} (CostructuredArrow F Y))))
              (Equivalence.symm (Shrink.equivalence (CostructuredArrow F Y)))) ⋙
          CostructuredArrow.proj F Y ⋙ F)
        j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsDense
⊢ CategoryStruct.comp (Y := F ⋙ F.leftKanExtension F) (F.leftKanExtensionUnit F : F ⟶ F ⋙ F.leftKanExtension F)
      (F.whiskerLeft (Iso.hom (leftKanExtensionIso F)) : F ⋙ F.leftKanExtension F ⟶ F ⋙ 𝟭 D) =
    F.rightUnitor.inv

Tactic:
simp [Functor.IsDense.leftKanExtensionIso]

Premises used: CategoryTheory.Functor.IsDense.leftKanExtensionIso
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsDense
X : C
⊢ CategoryStruct.comp (Y := (F ⋙ F.leftKanExtension F).obj X)
      (NatTrans.app (F.leftKanExtensionUnit F) X : F.obj X ⟶ (F ⋙ F.leftKanExtension F).obj X)
      (NatTrans.app (Iso.hom (leftKanExtensionIso F)) (F.obj X) :
        (F.leftKanExtension F).obj (F.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) (F.obj X)) =
    F.rightUnitor.inv.app X

Tactic:
congr($(Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom _).app _)

Premises used: congrArg, id, CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
Y : D
hY : F.DenseAt Y
G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
⊢ (Cocone.precompose
          (Iso.symm
                (associator (Equivalence.functor (CostructuredArrow.mapNatIso e.symm)) (CostructuredArrow.proj F Y)
                  F) ≪≫
              (Equivalence.functor (CostructuredArrow.mapNatIso e.symm) ⋙ CostructuredArrow.proj F Y).isoWhiskerLeft
                e).inv).obj
      (Cocone.whisker (Equivalence.functor (CostructuredArrow.mapNatIso e.symm))
        ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y)) ≅
    (LeftExtension.mk (𝟭 D) G.rightUnitor.inv).coconeAt Y

Tactic:
exact Cocone.ext (Iso.refl _)

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
Y : D
hf : F.DenseAt Y
⊢ F.HasPointwiseLeftKanExtensionAt F Y

Tactic:
⟨_, hf⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ F.isDenseAt = (LeftExtension.mk (𝟭 D) F.rightUnitor.inv).isPointwiseLeftKanExtensionAt

Tactic:
rfl

Premises used: CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAt, CategoryTheory.Functor.isDenseAt, rfl
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : D
⊢ F.isDenseAt X ↔ Nonempty (IsColimit ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt X))

Tactic:
.rfl

Premises used: Iff.rfl, CategoryTheory.Functor.isDenseAt, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
Y : D
hY : F.DenseAt Y
⊢ (LeftExtension.mk (𝟭 D) F.rightUnitor.inv).isPointwiseLeftKanExtensionAt.IsClosedUnderIsomorphisms

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
h : ∀ (X : D), F.isDenseAt X ↔ G.isDenseAt X
⊢ F.isDenseAt = G.isDenseAt

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
X : D
⊢ F.isDenseAt X ↔ G.isDenseAt X

Tactic:
⟨fun ⟨h⟩ ↦ ⟨h.ofNatIso e⟩, fun ⟨h⟩ ↦ ⟨h.ofNatIso e.symm⟩⟩

Premises used: CategoryTheory.Functor.isDenseAt, Nonempty.intro, _private.0.CategoryTheory.Functor.congr_isDenseAt.match_1, CategoryTheory.Functor.DenseAt.ofNatIso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
X : D
⊢ F.isDenseAt X ↔ G.isDenseAt X

Tactic:
exact ⟨fun ⟨h⟩ ↦ ⟨h.ofNatIso e⟩, fun ⟨h⟩ ↦ ⟨h.ofNatIso e.symm⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
Y : D
C' : Type u_1
inst_2 : Category.{v_1, u_1} C'
G : Functor.{v_1, v₁, u_1, u₁} C' C
inst_3 : (CostructuredArrow.pre G F Y).Final
⊢ (G ⋙ F).isDenseAt Y ↔ F.isDenseAt Y

Tactic:
(DenseAt.precompEquivOfFinal G).nonempty_congr

Premises used: CategoryTheory.Functor.isDenseAt, Equiv.nonempty_congr, CategoryTheory.Functor.DenseAt.precompEquivOfFinal
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
Y : D
C' : Type u_1
inst_2 : Category.{v_1, u_1} C'
G : Functor.{v_1, v₁, u_1, u₁} C' C
inst_3 : (CostructuredArrow.pre G F Y).Final
hY : F.isDenseAt Y
⊢ (G ⋙ F).isDenseAt Y

Tactic:
(iff_of_final G).mpr hY

Premises used: Iff.mpr, CategoryTheory.Functor.IsDenseAt.iff_of_final
-- 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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
revert : ∀ {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂), L.HasPointwiseLeftKanExtensionAt F Y₁ ↔ L.HasPointwiseLeftKanExtensionAt F Y₂
⊢ L.HasPointwiseLeftKanExtensionAt F Y₁ ↔ L.HasPointwiseLeftKanExtensionAt F Y₂

Tactic:
revert Y₁ Y₂ e
-- 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
suffices : ∀ ⦃Y₁ Y₂ : D⦄ (x : Y₁ ≅ Y₂) [L.HasPointwiseLeftKanExtensionAt F Y₁], L.HasPointwiseLeftKanExtensionAt F Y₂
⊢ ∀ {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂), L.HasPointwiseLeftKanExtensionAt F Y₁ ↔ L.HasPointwiseLeftKanExtensionAt F Y₂

Tactic:
suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseLeftKanExtensionAt L F Y₁],
      HasPointwiseLeftKanExtensionAt L F Y₂ from
    fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩
-- 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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
_ : ∀ [L.HasPointwiseLeftKanExtensionAt F Y₁], L.HasPointwiseLeftKanExtensionAt F Y₂
⊢ ∀ [L.HasPointwiseLeftKanExtensionAt F Y₁], L.HasPointwiseLeftKanExtensionAt F Y₂

Tactic:
_
-- 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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst_3 : L.HasPointwiseLeftKanExtensionAt F Y₁
change : HasColimit (Equivalence.functor (CostructuredArrow.mapIso e.symm) ⋙ CostructuredArrow.proj L Y₁ ⋙ F)
⊢ L.HasPointwiseLeftKanExtensionAt F Y₂

Tactic:
change HasColimit ((CostructuredArrow.mapIso e.symm).functor ⋙ CostructuredArrow.proj L Y₁ ⋙ F)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.Iso.symm, CategoryTheory.Limits.HasColimit, CategoryTheory.CostructuredArrow.mapIso, CategoryTheory.CostructuredArrow.proj
-- 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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst_3 : L.HasPointwiseLeftKanExtensionAt F Y₁
⊢ HasColimit (Equivalence.functor (CostructuredArrow.mapIso e.symm) ⋙ CostructuredArrow.proj L Y₁ ⋙ F)

Tactic:
infer_instance
-- 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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
revert : ∀ {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂), L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂
⊢ L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
revert Y₁ Y₂ e
-- 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
suffices : ∀ ⦃Y₁ Y₂ : D⦄ (x : Y₁ ≅ Y₂) [L.HasPointwiseRightKanExtensionAt F Y₁], L.HasPointwiseRightKanExtensionAt F Y₂
⊢ ∀ {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂), L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseRightKanExtensionAt L F Y₁],
      HasPointwiseRightKanExtensionAt L F Y₂ from
    fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩
-- 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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
_ : ∀ [L.HasPointwiseRightKanExtensionAt F Y₁], L.HasPointwiseRightKanExtensionAt F Y₂
⊢ ∀ [L.HasPointwiseRightKanExtensionAt F Y₁], L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
_
-- 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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst_3 : L.HasPointwiseRightKanExtensionAt F Y₁
change : HasLimit (Equivalence.functor (StructuredArrow.mapIso e.symm) ⋙ StructuredArrow.proj Y₁ L ⋙ F)
⊢ L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
change HasLimit ((StructuredArrow.mapIso e.symm).functor ⋙ StructuredArrow.proj Y₁ L ⋙ F)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.HasLimit, CategoryTheory.Equivalence.functor, CategoryTheory.StructuredArrow.mapIso, CategoryTheory.Iso.symm, CategoryTheory.StructuredArrow.proj
-- 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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst_3 : L.HasPointwiseRightKanExtensionAt F Y₁
⊢ HasLimit (Equivalence.functor (StructuredArrow.mapIso e.symm) ⋙ StructuredArrow.proj Y₁ L ⋙ F)

Tactic:
infer_instance
-- 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
L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
Y : D
revert :
  ∀ {L L' : Functor.{v_1, v_2, u_1, u_2} C D} (e : L ≅ L'),
    L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y
⊢ L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y

Tactic:
revert L L' e
-- 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
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
suffices :
  ∀ ⦃L L' : Functor.{v_1, v_2, u_1, u_2} C D⦄ (x : L ≅ L') [L.HasPointwiseLeftKanExtensionAt F Y],
    L'.HasPointwiseLeftKanExtensionAt F Y
⊢ ∀ {L L' : Functor.{v_1, v_2, u_1, u_2} C D} (e : L ≅ L'),
    L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y

Tactic:
suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseLeftKanExtensionAt L F Y],
      HasPointwiseLeftKanExtensionAt L' F Y from
    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
-- 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
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
L L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
_ : ∀ [L.HasPointwiseLeftKanExtensionAt F Y], L'.HasPointwiseLeftKanExtensionAt F Y
⊢ ∀ [L.HasPointwiseLeftKanExtensionAt F Y], L'.HasPointwiseLeftKanExtensionAt F Y

Tactic:
_
-- 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
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
L L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
inst_3 : L.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L' Y ≌ CostructuredArrow L Y := Comma.mapLeftIso (fromPUnit Y) e.symm
e' : CostructuredArrow.proj L' Y ⋙ F ≅ Φ.functor ⋙ CostructuredArrow.proj L Y ⋙ F :=
  Iso.refl (CostructuredArrow.proj L' Y ⋙ F)
⊢ L'.HasPointwiseLeftKanExtensionAt F Y

Tactic:
hasColimit_of_iso e'

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- 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
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
L L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
inst_3 : L.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L' Y ≌ CostructuredArrow L Y := Comma.mapLeftIso (fromPUnit Y) e.symm
e' : CostructuredArrow.proj L' Y ⋙ F ≅ Φ.functor ⋙ CostructuredArrow.proj L Y ⋙ F :=
  Iso.refl (CostructuredArrow.proj L' Y ⋙ F)
⊢ L'.HasPointwiseLeftKanExtensionAt F Y

Tactic:
exact hasColimit_of_iso e'

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- 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
L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
Y : D
revert :
  ∀ {L L' : Functor.{v_1, v_2, u_1, u_2} C D} (e : L ≅ L'),
    L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y
⊢ L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
revert L L' e
-- 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
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
suffices :
  ∀ ⦃L L' : Functor.{v_1, v_2, u_1, u_2} C D⦄ (x : L ≅ L') [L.HasPointwiseRightKanExtensionAt F Y],
    L'.HasPointwiseRightKanExtensionAt F Y
⊢ ∀ {L L' : Functor.{v_1, v_2, u_1, u_2} C D} (e : L ≅ L'),
    L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseRightKanExtensionAt L F Y],
      HasPointwiseRightKanExtensionAt L' F Y from
    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
-- 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
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
L L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
_ : ∀ [L.HasPointwiseRightKanExtensionAt F Y], L'.HasPointwiseRightKanExtensionAt F Y
⊢ ∀ [L.HasPointwiseRightKanExtensionAt F Y], L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
_
-- 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
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
L L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
inst_3 : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso (fromPUnit Y) e.symm
e' : StructuredArrow.proj Y L' ⋙ F ≅ Φ.functor ⋙ StructuredArrow.proj Y L ⋙ F :=
  Iso.refl (StructuredArrow.proj Y L' ⋙ F)
⊢ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
hasLimit_of_iso e'.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm
-- 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
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
L L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
inst_3 : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso (fromPUnit Y) e.symm
e' : StructuredArrow.proj Y L' ⋙ F ≅ Φ.functor ⋙ StructuredArrow.proj Y L ⋙ F :=
  Iso.refl (StructuredArrow.proj Y L' ⋙ F)
⊢ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
exact hasLimit_of_iso e'.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm