awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : F₀ ≅ L.functor ⋙ F₁
refine :
  ∀ (Y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C)))
    (m : (LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom) ⟶ Y),
    m =
      (fun (y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C))) ↦
          StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ⋯)
        Y
⊢ StructuredArrow.IsUniversal
    ((LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom))

Tactic:
refine IsInitial.ofUniqueHom
    (fun y ↦ StructuredArrow.homMk <| α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ?_

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Limits.IsInitial.ofUniqueHom, CategoryTheory.StructuredArrow.hom, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : F₀ ≅ L.functor ⋙ F₁
y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C))
m : (LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom) ⟶ y
h :
  ∀ (x : C),
    (StructuredArrow.Hom.right m).app x =
      NatTrans.app
        (StructuredArrow.Hom.right
          ((fun (y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C))) ↦
              StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ⋯)
            y))
        x
⊢ m =
    (fun (y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C))) ↦
        StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ⋯)
      y

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : F₀ ≅ L.functor ⋙ F₁
y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C))
m : (LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom) ⟶ y
x : C
⊢ (StructuredArrow.Hom.right m).app x =
    NatTrans.app
      (StructuredArrow.Hom.right
        ((fun (y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C))) ↦
            StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ⋯)
          y))
      x

Tactic:
simpa using α.inv.app x ≫= congr_app m.w x

Premises used: CategoryTheory.congr_app, CategoryTheory.Iso.inv, CategoryTheory.StructuredArrow.Hom.w, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L_1 : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
α : F₀ ⟶ L ⋙ F₁
inst_5 : L.IsEquivalence
inst_6 : IsIso α
⊢ F₁.IsLeftKanExtension α

Tactic:
inferInstanceAs <|
    F₁.IsLeftKanExtension (asIso α : F₀ ≅ (asEquivalence L).functor ⋙ F₁).hom

Premises used: _private.0.CategoryTheory.Functor.isLeftKanExtensionAlongEquivalence'._proof_1
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : L.functor ⋙ F₁ ≅ F₀
⊢ F₁.IsRightKanExtension α.hom

Tactic:
⟨⟨?_⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.IsRightKanExtension.mk
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : L.functor ⋙ F₁ ≅ F₀
refine : CostructuredArrow.IsUniversal (RightExtension.mk F₁ α.hom)
⊢ F₁.IsRightKanExtension α.hom

Tactic:
refine ⟨⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : L.functor ⋙ F₁ ≅ F₀
apply :
  CostructuredArrow.IsUniversal
    ((RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom))
⊢ CostructuredArrow.IsUniversal (RightExtension.mk F₁ α.hom)

Tactic:
apply RightExtension.isUniversalPostcomp₁Equiv
    (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.RightExtension.isUniversalPostcomp₁Equiv, CategoryTheory.Functor.leftUnitor, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : L.functor ⋙ F₁ ≅ F₀
refine :
  ∀ (X : CostructuredArrow (obj (whiskeringLeft C C H) (𝟭 C)) F₀)
    (m : X ⟶ (RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom)),
    m =
      (fun (y : CostructuredArrow (obj (whiskeringLeft C C H) (𝟭 C)) F₀) ↦
          CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯)
        X
⊢ CostructuredArrow.IsUniversal
    ((RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom))

Tactic:
refine IsTerminal.ofUniqueHom
    (fun y ↦ CostructuredArrow.homMk <| y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ?_

Premises used: CategoryTheory.Limits.IsTerminal.ofUniqueHom, CategoryTheory.CostructuredArrow.hom, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : L.functor ⋙ F₁ ≅ F₀
y : CostructuredArrow (obj (whiskeringLeft C C H) (𝟭 C)) F₀
m : y ⟶ (RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom)
h :
  ∀ (x : C),
    m.left.app x =
      NatTrans.app
        (CommaMorphism.left
          ((fun (y : CostructuredArrow (obj (whiskeringLeft C C H) (𝟭 C)) F₀) ↦
              CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯)
            y))
        x
⊢ m =
    (fun (y : CostructuredArrow (obj (whiskeringLeft C C H) (𝟭 C)) F₀) ↦
        CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯)
      y

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : L.functor ⋙ F₁ ≅ F₀
y : CostructuredArrow (obj (whiskeringLeft C C H) (𝟭 C)) F₀
m : y ⟶ (RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom)
x : C
⊢ m.left.app x =
    NatTrans.app
      (CommaMorphism.left
        ((fun (y : CostructuredArrow (obj (whiskeringLeft C C H) (𝟭 C)) F₀) ↦
            CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯)
          y))
      x

Tactic:
simpa using congr_app m.w x =≫ α.inv.app x

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.congr_app, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L_1 : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
α : L ⋙ F₁ ⟶ F₀
inst_5 : L.IsEquivalence
inst_6 : IsIso α
⊢ F₁.IsRightKanExtension α

Tactic:
inferInstanceAs <|
    F₁.IsRightKanExtension (asIso α : (asEquivalence L).functor ⋙ F₁ ≅ F₀).hom

Premises used: _private.0.CategoryTheory.Functor.isRightKanExtensionAlongEquivalence'._proof_1
-- 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
⊢ F.IsDense ↔ Nonempty (LeftExtension.mk (𝟭 D) F.rightUnitor.inv).IsPointwiseLeftKanExtension

Tactic:
⟨fun _ ↦ ⟨fun _ ↦ F.denseAt _⟩, fun ⟨h⟩ ↦ ⟨fun _ ↦ ⟨h _⟩⟩⟩

Premises used: CategoryTheory.Functor.IsDense.mk, _private.0.CategoryTheory.Functor.isDense_iff_nonempty_isPointwiseLeftKanExtension.match_1, Nonempty.intro, CategoryTheory.Functor.IsDense, Iff.intro, CategoryTheory.Functor.denseAt
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
⊢ IsLeftKanExtension (𝟭 D) F.rightUnitor.inv

Tactic:
((Functor.isDense_iff_nonempty_isPointwiseLeftKanExtension F).mp ‹_›).some.isLeftKanExtension

Premises used: CategoryTheory.Functor.isDense_iff_nonempty_isPointwiseLeftKanExtension, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.Functor.id, Nonempty.some, Iff.mp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
⊢ F.HasPointwiseLeftKanExtension F

Tactic:
fun X ↦ (Functor.IsDense.isDenseAt F X).some.hasPointwiseLeftKanExtensionAt

Premises used: CategoryTheory.Functor.DenseAt.hasPointwiseLeftKanExtensionAt, Nonempty.some, CategoryTheory.Functor.IsDense.isDenseAt
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
inst_2 : F.IsDense
Y : D
rw : F.isDenseAt Y
⊢ G.isDenseAt Y

Tactic:
rw [← Functor.congr_isDenseAt e]

Premises used: CategoryTheory.Functor.congr_isDenseAt
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
inst_2 : F.IsDense
Y : D
⊢ F.isDenseAt Y

Tactic:
⟨F.denseAt Y⟩

Premises used: CategoryTheory.Functor.isDenseAt, Nonempty.intro, CategoryTheory.Functor.denseAt
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
inst_2 : F.IsDense
Y : D
⊢ F.isDenseAt Y

Tactic:
exact ⟨F.denseAt Y⟩
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
⊢ F.IsDense ↔ G.IsDense

Tactic:
⟨fun _ ↦ of_iso e, fun _ ↦ of_iso e.symm⟩

Premises used: CategoryTheory.Functor.IsDense.of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁, u₃, u₁} C' C
inst_3 : G.IsEquivalence
⊢ (G ⋙ F).IsDense ↔ F.IsDense

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁, u₃, u₁} C' C
inst_3 : G.IsEquivalence
refine : (G ⋙ F).IsDense → F.IsDense
⊢ (G ⋙ F).IsDense ↔ F.IsDense

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁, u₃, u₁} C' C
inst_3 : G.IsEquivalence
h : (G ⋙ F).IsDense
e : G.inv ⋙ G ⋙ F ≅ F := (G.inv.associator G F).symm ≪≫ isoWhiskerRight G.asEquivalence.counitIso F ≪≫ F.leftUnitor
⊢ F.IsDense

Tactic:
of_iso e

Premises used: CategoryTheory.Functor.IsDense.of_iso
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁, u₃, u₁} C' C
inst_3 : G.IsEquivalence
h : (G ⋙ F).IsDense
e : G.inv ⋙ G ⋙ F ≅ F := (G.inv.associator G F).symm ≪≫ isoWhiskerRight G.asEquivalence.counitIso F ≪≫ F.leftUnitor
⊢ F.IsDense

Tactic:
exact of_iso e

Premises used: CategoryTheory.Functor.IsDense.of_iso
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D C'
inst_3 : G.IsEquivalence
⊢ (F ⋙ G).IsDense ↔ F.IsDense

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D C'
inst_3 : G.IsEquivalence
refine : (F ⋙ G).IsDense → F.IsDense
⊢ (F ⋙ G).IsDense ↔ F.IsDense

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D C'
inst_3 : G.IsEquivalence
h : (F ⋙ G).IsDense
e : (F ⋙ G) ⋙ G.inv ≅ F := F.associator G G.inv ≪≫ F.isoWhiskerLeft G.asEquivalence.unitIso.symm ≪≫ F.rightUnitor
⊢ F.IsDense

Tactic:
of_iso e

Premises used: CategoryTheory.Functor.IsDense.of_iso
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D C'
inst_3 : G.IsEquivalence
h : (F ⋙ G).IsDense
e : (F ⋙ G) ⋙ G.inv ≅ F := F.associator G G.inv ≪≫ F.isoWhiskerLeft G.asEquivalence.unitIso.symm ≪≫ F.rightUnitor
⊢ F.IsDense

Tactic:
exact of_iso e

Premises used: CategoryTheory.Functor.IsDense.of_iso
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
X_1 Y : D
a₁ a₂ : X_1 ⟶ Y
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map a₁ = (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map a₂
X : C
p : F.obj X ⟶ X_1
⊢ (StructuredArrow.hom (LeftExtension.mk (𝟭 D) F.rightUnitor.inv)).app X ≫
      (StructuredArrow.right (LeftExtension.mk (𝟭 D) F.rightUnitor.inv)).map p ≫ a₁ =
    (StructuredArrow.hom (LeftExtension.mk (𝟭 D) F.rightUnitor.inv)).app X ≫
      (StructuredArrow.right (LeftExtension.mk (𝟭 D) F.rightUnitor.inv)).map p ≫ a₂

Tactic:
simpa using ULift.up_injective (ConcreteCategory.congr_hom (CC := fun X ↦ X)
        (NatTrans.congr_app h (op X)) (ULift.up p))

Premises used: ULift.up_injective, CategoryTheory.NatTrans.congr_app, Opposite.op, CategoryTheory.ConcreteCategory.congr_hom, ULift.up
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
Y Z : D
f : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Z
g₁ g₂ : CostructuredArrow F Y
φ : g₁ ⟶ g₂
⊢ Eq (α := (CostructuredArrow.proj F Y ⋙ F).obj g₁ ⟶ obj (obj (const (CostructuredArrow F Y)) Z) g₂)
    ((CostructuredArrow.proj F Y ⋙ F).map φ ≫
      ULift.down.{w, v₂}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op g₂.left)) :
            (a : (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Y).obj (op g₂.left))) →
              (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Z).obj (op g₂.left)))
          { down := g₂.hom }))
    (ULift.down.{w, v₂}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op g₁.left)) :
            (a : (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Y).obj (op g₁.left))) →
              (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Z).obj (op g₁.left)))
          { down := g₁.hom }) ≫
      map (obj (const (CostructuredArrow F Y)) Z) φ)

Tactic:
simpa [uliftFunctor, uliftYoneda,
                restrictedULiftYoneda, ← ULift.down_inj] using
                ((f.naturality_apply φ.left.op) (ULift.up g₂.hom)).symm

Premises used: CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, ULift.down_inj, CategoryTheory.CostructuredArrow.hom, CategoryTheory.uliftFunctor, CategoryTheory.Presheaf.restrictedULiftYoneda, CategoryTheory.CommaMorphism.left, ULift.up, Eq.symm, CategoryTheory.uliftYoneda
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
Y Z : D
f : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Z
c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
  { pt := Z,
    ι :=
      {
        app := fun (g : CostructuredArrow F Y) ↦
          ULift.down.{w, v₂}
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op g.left)) :
                (a : (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Y).obj (op g.left))) →
                  (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Z).obj (op g.left)))
              { down := g.hom }),
        naturality := ⋯ } }
⊢ ∃ (a : Y ⟶ Z), (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map a = f

Tactic:
⟨(F.denseAt Y).desc c, ?_⟩

Premises used: CategoryTheory.Limits.IsColimit.desc, Exists.intro, CategoryTheory.Functor.denseAt
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
Y Z : D
f : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Z
c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
  { pt := Z,
    ι :=
      {
        app := fun (g : CostructuredArrow F Y) ↦
          ULift.down.{w, v₂}
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op g.left)) :
                (a : (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Y).obj (op g.left))) →
                  (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Z).obj (op g.left)))
              { down := g.hom }),
        naturality := ⋯ } }
refine : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map ((F.denseAt Y).desc c) = f
⊢ ∃ (a : Y ⟶ Z), (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map a = f

Tactic:
refine ⟨(F.denseAt Y).desc c, ?_⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
Y Z : D
f : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Z
c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
  { pt := Z,
    ι :=
      {
        app := fun (g : CostructuredArrow F Y) ↦
          ULift.down.{w, v₂}
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op g.left)) :
                (a : (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Y).obj (op g.left))) →
                  (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Z).obj (op g.left)))
              { down := g.hom }),
        naturality := ⋯ } }
w :
  ∀ (X : C) (x : obj (obj yoneda Y) (F.op.obj (op X))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map ((F.denseAt Y).desc c)).app (op X)))
        { down := x : ULift.{w, v₂} (obj (obj yoneda Y) (F.op.obj (op X))) } =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)))
        { down := x : ULift.{w, v₂} (obj (obj yoneda Y) (F.op.obj (op X))) }
⊢ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map ((F.denseAt Y).desc c) = f

Tactic:
ext ⟨X⟩ ⟨x⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
Y Z : D
f : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Z
c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
  { pt := Z,
    ι :=
      {
        app := fun (g : CostructuredArrow F Y) ↦
          ULift.down.{w, v₂}
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op g.left)) :
                (a : (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Y).obj (op g.left))) →
                  (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Z).obj (op g.left)))
              { down := g.hom }),
        naturality := ⋯ } }
X : C
x : obj (obj yoneda Y) (F.op.obj (op X))
⊢ Eq (α := (CostructuredArrow.proj F Y ⋙ F).obj (CostructuredArrow.mk x) ⟶ c.pt)
    (((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).ι.app (CostructuredArrow.mk x) ≫ (F.denseAt Y).desc c)
    (c.ι.app (CostructuredArrow.mk x))

Tactic:
have := (F.denseAt Y).fac c (.mk x)