awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
⊢ (fun (f : F ⟶ G) ↦
        { app := fun (x : C) ↦ ↾fun (x_1 : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) x) ↦ HomObj.ofNatTrans f,
          naturality := ⋯ : NatTrans ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) (F.functorHom G) })
      ((fun (f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G) ↦
          {
            app := fun (X : C) ↦
              HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                    (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                      (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                  PUnit.unit)
                X (𝟙 (Opposite.unop (Opposite.op X))),
            naturality := ⋯ : NatTrans F G })
        f) =
    f
have w : ∀ (X : C) (a : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) X) (Y : C) (φ : X ⟶ Y),
  HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (f : F ⟶ G) ↦
                {
                  app := fun (x : C) ↦
                    ↾fun (x_1 : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) x) ↦ HomObj.ofNatTrans f,
                  naturality := sorry : NatTrans ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) (F.functorHom G) })
              ((fun (f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G) ↦
                  {
                    app := fun (X : C) ↦
                      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                            (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                          PUnit.unit)
                        X (𝟙 (Opposite.unop (Opposite.op X))),
                    naturality := sorry : NatTrans F G })
                f))
            X))
        a)
      Y φ =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun a).app Y φ
Tactic: ext X a Y φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
φ : F₁ ⟶ F₂
⊢ Eq (α := obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₁ ⟶ obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F₂)
    (map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) φ ≫ L.leftKanExtensionUnit F₂)
    (CategoryStruct.comp (Y := obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F₁) (L.leftKanExtensionUnit F₁)
      (map (L.lan ⋙ obj (whiskeringLeft C D H) L) φ))
have w : ∀ (x : C),
  Eq (α :=
    (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₁).obj x ⟶ (obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F₂).obj x)
    (NatTrans.app (map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) φ ≫ L.leftKanExtensionUnit F₂) x)
    (NatTrans.app
      (CategoryStruct.comp (Y := obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F₁) (L.leftKanExtensionUnit F₁)
        (map (L.lan ⋙ obj (whiskeringLeft C D H) L) φ))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ (obj L.lan F).IsLeftKanExtension (NatTrans.app L.lanUnit F)
have dsimp : (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)
Tactic: dsimp [lan, lanUnit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
G : Functor.{v_2, v_3, u_2, u_3} D H
f : F₁ ⟶ F₂
α : F₂ ⟶ obj (obj (whiskeringLeft C D H) L) G
⊢ Eq (α := obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₁ ⟶ L ⋙ G)
    (CategoryStruct.comp (Y := L ⋙ obj L.lan F₁) (NatTrans.app L.lanUnit F₁)
      (L.whiskerLeft
        ((((obj L.lan F₁).homEquivOfIsLeftKanExtension (NatTrans.app L.lanUnit F₁) G).symm :
            (a : F₁ ⟶ ((whiskeringLeft C D H).obj L).obj G) → L.lan.obj F₁ ⟶ G)
          (f ≫ α))))
    (CategoryStruct.comp (Y := L ⋙ obj L.lan F₁) (NatTrans.app L.lanUnit F₁)
      (L.whiskerLeft
        (map L.lan f ≫
          (((obj L.lan F₂).homEquivOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G).symm :
              (a : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G) → L.lan.obj F₂ ⟶ G)
            α)))
have w : ∀ (X : C),
  Eq (α := (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₁).obj X ⟶ (L ⋙ G).obj X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.lan F₁) (NatTrans.app L.lanUnit F₁)
        (L.whiskerLeft
          ((((obj L.lan F₁).homEquivOfIsLeftKanExtension (NatTrans.app L.lanUnit F₁) G).symm :
              (a : F₁ ⟶ ((whiskeringLeft C D H).obj L).obj G) → L.lan.obj F₁ ⟶ G)
            (f ≫ α))))
      X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.lan F₁) (NatTrans.app L.lanUnit F₁)
        (L.whiskerLeft
          (map L.lan f ≫
            (((obj L.lan F₂).homEquivOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G).symm :
                (a : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G) → L.lan.obj F₂ ⟶ G)
              α)))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
G : Functor.{v_2, v_3, u_2, u_3} D H
f : F₁ ⟶ F₂
α : F₂ ⟶ obj (obj (whiskeringLeft C D H) L) G
X : C
⊢ Eq (α := (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₁).obj X ⟶ (L ⋙ G).obj X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.lan F₁) (NatTrans.app L.lanUnit F₁)
        (L.whiskerLeft
          ((((obj L.lan F₁).homEquivOfIsLeftKanExtension (NatTrans.app L.lanUnit F₁) G).symm :
              (a : F₁ ⟶ ((whiskeringLeft C D H).obj L).obj G) → L.lan.obj F₁ ⟶ G)
            (f ≫ α))))
      X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.lan F₁) (NatTrans.app L.lanUnit F₁)
        (L.whiskerLeft
          (map L.lan f ≫
            (((obj L.lan F₂).homEquivOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G).symm :
                (a : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G) → L.lan.obj F₂ ⟶ G)
              α)))
      X)
have w : NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫
    ((obj L.lan F₁).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₁) G (f ≫ α)).app (L.obj X) =
  NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫
    NatTrans.app (map L.lan f) (L.obj X) ≫
      ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
Tactic: dsimp [homEquivOfIsLeftKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
G : Functor.{v_2, v_3, u_2, u_3} D H
f : F₁ ⟶ F₂
α : F₂ ⟶ obj (obj (whiskeringLeft C D H) L) G
X : C
⊢ NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫
      ((obj L.lan F₁).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₁) G (f ≫ α)).app (L.obj X) =
    NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫
      NatTrans.app (map L.lan f) (L.obj X) ≫
        ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
have w : f.app X ≫ α.app X =
  (NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫ NatTrans.app (map L.lan f) (L.obj X)) ≫
    ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
Tactic: rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
G : Functor.{v_2, v_3, u_2, u_3} D H
f : F₁ ⟶ F₂
α : F₂ ⟶ obj (obj (whiskeringLeft C D H) L) G
X : C
⊢ f.app X ≫ α.app X =
    (NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫ NatTrans.app (map L.lan f) (L.obj X)) ≫
      ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
have h : Eq (α := (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₁).obj X ⟶ (obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F₂).obj X)
  (NatTrans.app (map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) f ≫ NatTrans.app L.lanUnit F₂) X)
  (NatTrans.app (NatTrans.app L.lanUnit F₁ ≫ map (L.lan ⋙ obj (whiskeringLeft C D H) L) f) X)
Tactic: have h := congr_app (L.lanUnit.naturality f) X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
G : Functor.{v_2, v_3, u_2, u_3} D H
f : F₁ ⟶ F₂
α : F₂ ⟶ obj (obj (whiskeringLeft C D H) L) G
X : C
h :
  Eq (α := F₁.obj X ⟶ (obj L.lan F₂).obj (L.obj X)) (f.app X ≫ NatTrans.app (NatTrans.app L.lanUnit F₂) X)
    (NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫ NatTrans.app (map L.lan f) (L.obj X))
⊢ f.app X ≫ α.app X =
    (NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫ NatTrans.app (map L.lan f) (L.obj X)) ≫
      ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
have w : f.app X ≫ α.app X =
  (f.app X ≫ NatTrans.app (NatTrans.app L.lanUnit F₂) X) ≫
    ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
Tactic: rw [← h, assoc, descOfIsLeftKanExtension_fac_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
G : Functor.{v_2, v_3, u_2, u_3} D H
f : F₁ ⟶ F₂
α : F₂ ⟶ obj (obj (whiskeringLeft C D H) L) G
X : C
h :
  Eq (α := F₁.obj X ⟶ (obj L.lan F₂).obj (L.obj X)) (f.app X ≫ NatTrans.app (NatTrans.app L.lanUnit F₂) X)
    (NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫ NatTrans.app (map L.lan f) (L.obj X))
w :
  f.app X ≫ α.app X =
    (f.app X ≫ NatTrans.app (NatTrans.app L.lanUnit F₂) X) ≫
      ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
⊢ f.app X ≫ α.app X =
    (NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫ NatTrans.app (map L.lan f) (L.obj X)) ≫
      ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
have w₁ : f.app X ≫ α.app X =
  f.app X ≫
    NatTrans.app (NatTrans.app L.lanUnit F₂) X ≫
      ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
Tactic: rw [← h, assoc, descOfIsLeftKanExtension_fac_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
G : Functor.{v_2, v_3, u_2, u_3} D H
f : F₁ ⟶ F₂
α : F₂ ⟶ obj (obj (whiskeringLeft C D H) L) G
X : C
h :
  Eq (α := F₁.obj X ⟶ (obj L.lan F₂).obj (L.obj X)) (f.app X ≫ NatTrans.app (NatTrans.app L.lanUnit F₂) X)
    (NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫ NatTrans.app (map L.lan f) (L.obj X))
w :
  f.app X ≫ α.app X =
    (f.app X ≫ NatTrans.app (NatTrans.app L.lanUnit F₂) X) ≫
      ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
w₁ :
  f.app X ≫ α.app X =
    f.app X ≫
      NatTrans.app (NatTrans.app L.lanUnit F₂) X ≫
        ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
⊢ f.app X ≫ α.app X =
    (NatTrans.app (NatTrans.app L.lanUnit F₁) X ≫ NatTrans.app (map L.lan f) (L.obj X)) ≫
      ((obj L.lan F₂).descOfIsLeftKanExtension (NatTrans.app L.lanUnit F₂) G α).app (L.obj X)
have w₂ : f.app X ≫ α.app X = f.app X ≫ α.app X
Tactic: rw [← h, assoc, descOfIsLeftKanExtension_fac_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
G₁ G₂ : Functor.{v_2, v_3, u_2, u_3} D H
β : obj L.lan F ⟶ G₁
f : G₁ ⟶ G₂
⊢ Eq (α := F ⟶ obj (obj (whiskeringLeft C D H) L) G₂)
    (((obj L.lan F).homEquivOfIsLeftKanExtension (NatTrans.app L.lanUnit F) G₂ :
          (a : L.lan.obj F ⟶ G₂) → F ⟶ ((whiskeringLeft C D H).obj L).obj G₂)
        (β ≫ f) :
      F ⟶ obj (obj (whiskeringLeft C D H) L) G₂)
    (((obj L.lan F).homEquivOfIsLeftKanExtension (NatTrans.app L.lanUnit F) G₁ :
            (a : L.lan.obj F ⟶ G₁) → F ⟶ ((whiskeringLeft C D H).obj L).obj G₁)
          β ≫
        map (obj (whiskeringLeft C D H) L) f :
      F ⟶ obj (obj (whiskeringLeft C D H) L) G₂)
have dsimp : NatTrans.app L.lanUnit F ≫ L.whiskerLeft β ≫ L.whiskerLeft f =
  (NatTrans.app L.lanUnit F ≫ L.whiskerLeft β) ≫ L.whiskerLeft f
Tactic: dsimp [homEquivOfIsLeftKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
G₁ G₂ : Functor.{v_2, v_3, u_2, u_3} D H
β : obj L.lan F ⟶ G₁
f : G₁ ⟶ G₂
⊢ NatTrans.app L.lanUnit F ≫ L.whiskerLeft β ≫ L.whiskerLeft f =
    (NatTrans.app L.lanUnit F ≫ L.whiskerLeft β) ≫ L.whiskerLeft f
have rw : NatTrans.app L.lanUnit F ≫ L.whiskerLeft β ≫ L.whiskerLeft f =
  NatTrans.app L.lanUnit F ≫ L.whiskerLeft β ≫ L.whiskerLeft f
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_1, v_3, u_1, u_3} C H ⥤ Functor.{v_1, v_3, u_1, u_3} C H)
      (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) (L.lan ⋙ obj (whiskeringLeft C D H) L))
    (Adjunction.unit (L.lanAdjunction H)) L.lanUnit
have w : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H),
  Eq (α := obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F ⟶ obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F)
    (NatTrans.app (Adjunction.unit (L.lanAdjunction H)) F) (NatTrans.app L.lanUnit F)
Tactic: ext F : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ Eq (α := obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F ⟶ obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F)
    (NatTrans.app (Adjunction.unit (L.lanAdjunction H)) F) (NatTrans.app L.lanUnit F)
have w : NatTrans.app L.lanUnit F ≫ 𝟙 (L ⋙ obj L.lan F) = NatTrans.app L.lanUnit F
Tactic: dsimp [lanAdjunction, homEquivOfIsLeftKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_5 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} D H
X Y : Functor.{v_1, v_3, u_1, u_3} C H
f : X ⟶ Y
i : C
⊢ Eq (α := X.obj i ⟶ obj (L.lan ⋙ colim) Y)
    (CategoryStruct.comp (Y := colimit X) (colimit.ι X i)
      (map colim f ≫
        Iso.hom
          ((fun (G : Functor.{v_1, v_3, u_1, u_3} C H) ↦
              (Iso.symm ((obj L.lan G).colimitIsoOfIsLeftKanExtension (NatTrans.app L.lanUnit G)) :
                colimit (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G) ≅ colimit (obj L.lan G)))
            Y)))
    (CategoryStruct.comp (Y := colimit X) (colimit.ι X i)
      (Iso.hom
          ((fun (G : Functor.{v_1, v_3, u_1, u_3} C H) ↦
              (Iso.symm ((obj L.lan G).colimitIsoOfIsLeftKanExtension (NatTrans.app L.lanUnit G)) :
                colimit (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G) ≅ colimit (obj L.lan G)))
            X) ≫
        map (L.lan ⋙ colim) f))
have dsimp : Eq (α := X.obj i ⟶ colimit (obj L.lan Y))
  (CategoryStruct.comp (Y := colimit X) (colimit.ι X i)
    (CategoryStruct.comp (Y := colimit Y) (colimMap f)
      (Iso.inv ((obj L.lan Y).colimitIsoOfIsLeftKanExtension (NatTrans.app L.lanUnit Y)))))
  (CategoryStruct.comp (Y := colimit X) (colimit.ι X i)
    (CategoryStruct.comp (Y := colimit (obj L.lan X))
      (Iso.inv ((obj L.lan X).colimitIsoOfIsLeftKanExtension (NatTrans.app L.lanUnit X))) (colimMap (map L.lan f))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_5 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} D H
X Y : Functor.{v_1, v_3, u_1, u_3} C H
f : X ⟶ Y
i : C
⊢ Eq (α := X.obj i ⟶ colimit (obj L.lan Y))
    (CategoryStruct.comp (Y := colimit X) (colimit.ι X i)
      (CategoryStruct.comp (Y := colimit Y) (colimMap f)
        (Iso.inv ((obj L.lan Y).colimitIsoOfIsLeftKanExtension (NatTrans.app L.lanUnit Y)))))
    (CategoryStruct.comp (Y := colimit X) (colimit.ι X i)
      (CategoryStruct.comp (Y := colimit (obj L.lan X))
        (Iso.inv ((obj L.lan X).colimitIsoOfIsLeftKanExtension (NatTrans.app L.lanUnit X))) (colimMap (map L.lan f))))
have rw : Eq (α := X.obj i ⟶ colimit (obj L.lan Y))
  ((f.app i ≫ NatTrans.app (NatTrans.app L.lanUnit Y) i) ≫ colimit.ι (obj L.lan Y) (L.obj i))
  ((NatTrans.app (NatTrans.app L.lanUnit X) i ≫ NatTrans.app (map L.lan f) (L.obj i)) ≫
    colimit.ι (obj L.lan Y) (L.obj i))
Tactic: rw [ι_colimMap_assoc, ι_colimitIsoOfIsLeftKanExtension_inv,
        ι_colimitIsoOfIsLeftKanExtension_inv_assoc, ι_colimMap, ← assoc, ← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_5 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} D H
X Y : Functor.{v_1, v_3, u_1, u_3} C H
f : X ⟶ Y
i : C
⊢ Eq (α := X.obj i ⟶ colimit (obj L.lan Y))
    ((f.app i ≫ NatTrans.app (NatTrans.app L.lanUnit Y) i) ≫ colimit.ι (obj L.lan Y) (L.obj i))
    ((NatTrans.app (NatTrans.app L.lanUnit X) i ≫ NatTrans.app (map L.lan f) (L.obj i)) ≫
      colimit.ι (obj L.lan Y) (L.obj i))
have e_a : Eq (α := X.obj i ⟶ (L ⋙ obj L.lan Y).obj i) (f.app i ≫ NatTrans.app (NatTrans.app L.lanUnit Y) i)
  (NatTrans.app (NatTrans.app L.lanUnit X) i ≫ NatTrans.app (map L.lan f) (L.obj i))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
G : Functor.{v_1, v_3, u_1, u_3} C H
inst_3 : L.HasPointwiseLeftKanExtension G
inst_4 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} D H
inst_5 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} C H
X : C
⊢ Eq (α := G.obj X ⟶ colimit (CostructuredArrow.grothendieckProj L ⋙ G))
    (CategoryStruct.comp (Y := colimit G) (colimit.ι G X : G.obj X ⟶ colimit G)
        (Iso.hom (L.colimitIsoColimitGrothendieck G) : colimit G ⟶ colimit (CostructuredArrow.grothendieckProj L ⋙ G)) :
      G.obj X ⟶ colimit (CostructuredArrow.grothendieckProj L ⋙ G))
    (colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
        { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) } :
      (CostructuredArrow.grothendieckProj L ⋙ G).obj
          { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) :
            Grothendieck (CostructuredArrow.functor L) } ⟶
        colimit (CostructuredArrow.grothendieckProj L ⋙ G))
have rw : Eq (α := G.obj X ⟶ colimit G) (colimit.ι G X)
  (CategoryStruct.comp (Y := colimit (CostructuredArrow.grothendieckProj L ⋙ G))
    (colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
        { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) } :
      (CostructuredArrow.grothendieckProj L ⋙ G).obj
          { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) :
            Grothendieck (CostructuredArrow.functor L) } ⟶
        colimit (CostructuredArrow.grothendieckProj L ⋙ G))
    (Iso.inv (L.colimitIsoColimitGrothendieck G) : colimit (CostructuredArrow.grothendieckProj L ⋙ G) ⟶ colimit G))
Tactic: rw [← Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : L.Full
inst_4 : L.Faithful
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_5 : L.HasPointwiseLeftKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasLeftKanExtension F
⊢ IsIso (Y := obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app (Adjunction.unit (L.lanAdjunction H)) F)
have rw : IsIso (Y := obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app L.lanUnit F)
Tactic: rw [lanAdjunction_unit]