awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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
⊢ m =
    (fun (y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C))) ↦
        StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ⋯)
      y
have 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) sorry)
          y))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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
have refine : CostructuredArrow.IsUniversal (RightExtension.mk F₁ α.hom)
Tactic: refine ⟨⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₀
⊢ CostructuredArrow.IsUniversal (RightExtension.mk F₁ α.hom)
have apply : CostructuredArrow.IsUniversal
  ((RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom))
Tactic: apply RightExtension.isUniversalPostcomp₁Equiv
    (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₀
⊢ CostructuredArrow.IsUniversal
    ((RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom))
have 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) sorry)
      X
Tactic: refine IsTerminal.ofUniqueHom
    (fun y ↦ CostructuredArrow.homMk <| y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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)
⊢ m =
    (fun (y : CostructuredArrow (obj (whiskeringLeft C C H) (𝟭 C)) F₀) ↦
        CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯)
      y
have 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) sorry)
          y))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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
⊢ G.isDenseAt Y
have rw : F.isDenseAt Y
Tactic: rw [← Functor.congr_isDenseAt e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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
have refine : (G ⋙ F).IsDense → F.IsDense
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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
have refine : (F ⋙ G).IsDense → F.IsDense
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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
have refine : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map ((F.denseAt Y).desc c) = f
Tactic: refine ⟨(F.denseAt Y).desc c, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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 := ⋯ } }
⊢ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map ((F.denseAt Y).desc c) = f
have 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))) }
Tactic: ext ⟨X⟩ ⟨x⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (hypothesis)
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))
⊢ 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))) }
have this : 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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 := ⋯ }
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)
have w : ∀ (X : C) (x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) } =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) }
Tactic: ext ⟨X⟩ ⟨x⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (hypothesis)
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 := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) } =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) }
have this : (CostructuredArrow.proj F Y ⋙ F).map α ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
Tactic: have := s.w α
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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 := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : (CostructuredArrow.proj F Y ⋙ F).map α ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) } =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) }
have w : { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } = { down := x ≫ s.ι.app j : ULift.{w, v₂} (F.obj X ⟶ s.pt) }
Tactic: dsimp [uliftYoneda, φ, α] at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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 := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : F.map (F.preimage x) ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } = { down := x ≫ s.ι.app j : ULift.{w, v₂} (F.obj X ⟶ s.pt) }
have w : ULift.down.{w, v₂} { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } =
  ULift.down.{w, v₂} { down := x ≫ s.ι.app j : ULift.{w, v₂} (F.obj X ⟶ s.pt) }
Tactic: apply ULift.down_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (hypothesis)
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 := ⋯ }
⊢ F.isDenseAt Y
have 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)
Tactic: have hφ (s) (j) : (restrictedULiftYoneda F).map j.hom ≫ φ s =
        (restrictedULiftYoneda F).map (s.ι.app j) := by
      ext ⟨X⟩ ⟨x⟩
      let α : .mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x)
      have := s.w α
      dsimp [uliftYoneda, φ, α] at this ⊢
      apply ULift.down_injective
      simpa using this.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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
⊢ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map m =
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (h.preimage (φ s))
have w : ∀ (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: ext ⟨_⟩ ⟨_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.DenseAt (goal)
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.isDenseAt = G.isDenseAt
have h : ∀ (X : D), F.isDenseAt X ↔ G.isDenseAt X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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₂
have suffices : ∀ ⦃Y₁ Y₂ : D⦄ (x : 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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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₁
⊢ L.HasPointwiseLeftKanExtensionAt F Y₂
have change : HasColimit (Equivalence.functor (CostructuredArrow.mapIso e.symm) ⋙ CostructuredArrow.proj L Y₁ ⋙ F)
Tactic: change HasColimit ((CostructuredArrow.mapIso e.symm).functor ⋙ CostructuredArrow.proj L Y₁ ⋙ F)