awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K L M N : Functor.{v, v', u, u'} C D
X : C
x : (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (K.functorHom L) (L.functorHom M)) (M.functorHom N)).obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
            (α_ (K.HomObj L (obj coyoneda (Opposite.op X))) (L.HomObj M (obj coyoneda (Opposite.op X)))
              (M.HomObj N (obj coyoneda (Opposite.op X))))) :
        (a :
            (K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗ L.HomObj M (coyoneda.obj (Opposite.op X))) ⊗
              M.HomObj N (coyoneda.obj (Opposite.op X))) →
          K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗
            L.HomObj M (coyoneda.obj (Opposite.op X)) ⊗ M.HomObj N (coyoneda.obj (Opposite.op X)))
      x =
    (x.1.1, x.1.2, x.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Functorial
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
⊢ map F.obj f = F.map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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₂
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)
⊢ 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) φ))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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₂
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:
simp [lan]

Premises used: CategoryTheory.Functor.lan
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
dsimp : (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)
⊢ (obj L.lan F).IsLeftKanExtension (NatTrans.app L.lanUnit F)

Tactic:
dsimp [lan, lanUnit]

Premises used: CategoryTheory.Functor.lan, CategoryTheory.Functor.lanUnit
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
⊢ (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_3 : L.HasPointwiseLeftKanExtension F
inst_4 : L.HasLeftKanExtension F
X : D
f : CostructuredArrow L X
⊢ CategoryStruct.comp (Y := colimit (proj L X ⋙ F)) (colimit.ι (proj L X ⋙ F) f)
      (Iso.inv (L.leftKanExtensionObjIsoColimit F X)) =
    NatTrans.app (L.leftKanExtensionUnit F) f.left ≫ (L.leftKanExtension F).map f.hom

Tactic:
simp [leftKanExtensionObjIsoColimit]

Premises used: CategoryTheory.Functor.leftKanExtensionObjIsoColimit
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_3 : L.HasPointwiseLeftKanExtension F
X : D
f : CostructuredArrow L X
⊢ Eq (α := F.obj f.left ⟶ colimit (proj L X ⋙ F))
    (NatTrans.app (L.leftKanExtensionUnit F) f.left ≫
      (L.leftKanExtension F).map f.hom ≫ Iso.hom (L.leftKanExtensionObjIsoColimit F X))
    (colimit.ι (proj L X ⋙ F) f)

Tactic:
LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom (F := F)
    (isPointwiseLeftKanExtensionLeftKanExtensionUnit L F X) f

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom, CategoryTheory.Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_3 : L.HasPointwiseLeftKanExtension F
X : C
⊢ Eq (α := F.obj X ⟶ colimit (J := CostructuredArrow L (L.obj X)) (proj L (L.obj X) ⋙ F))
    (CategoryStruct.comp (Y := (L ⋙ L.leftKanExtension F).obj X) (NatTrans.app (L.leftKanExtensionUnit F) X)
      (Iso.hom (L.leftKanExtensionObjIsoColimit F (L.obj X))))
    (colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X))))

Tactic:
simpa using leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom L F
    (L.obj X) (CostructuredArrow.mk (𝟙 _))

Premises used: CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom, CategoryTheory.CategoryStruct.id, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_3 : L.HasPointwiseLeftKanExtension F
X Y : D
f : X ⟶ Y
⊢ HasColimit (((functor L).map f).toFunctor ⋙ Grothendieck.ι (functor L) Y ⋙ grothendieckProj L ⋙ F)

Tactic:
hasColimit_of_iso (isoWhiskerRight (mapCompιCompGrothendieckProj L f) F)

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_3 : L.HasPointwiseLeftKanExtension F
inst_4 : L.HasLeftKanExtension F
this : ∀ (X : D), HasColimit (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) := ⋯
X Y : D
f : X ⟶ Y
⊢ ∀ (j : (↑((functor L).obj X) : Type (max u_1 v_2))),
    colimit.ι (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) j ≫
        (fiberwiseColimit (grothendieckProj L ⋙ F)).map f ≫
          Iso.hom
            ((fun (X : D) ↦
                (Iso.trans (Y := colimit (proj L X ⋙ F))
                    (HasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L X) F))
                    (Iso.symm (L.leftKanExtensionObjIsoColimit F X)) :
                  (fiberwiseColimit (grothendieckProj L ⋙ F)).obj X ≅ (L.leftKanExtension F).obj X))
              Y) =
      CategoryStruct.comp (Y := colimit (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F))
        (colimit.ι (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) j)
        (Iso.hom
            ((fun (X : D) ↦
                (Iso.trans (Y := colimit (proj L X ⋙ F))
                    (HasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L X) F))
                    (Iso.symm (L.leftKanExtensionObjIsoColimit F X)) :
                  (fiberwiseColimit (grothendieckProj L ⋙ F)).obj X ≅ (L.leftKanExtension F).obj X))
              X) ≫
          (L.leftKanExtension F).map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
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)
⊢ 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)
            α)))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
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)
⊢ 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:
dsimp [homEquivOfIsLeftKanExtension]

Premises used: CategoryTheory.Functor.homEquivOfIsLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
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)
⊢ 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:
rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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 ⟶ (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
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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 (α :=
    (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)
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)
⊢ 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:
dsimp at h ⊢
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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)
w₂ w₃ : f.app X ≫ α.app X = f.app X ≫ α.app 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)

Tactic:
rw [← h, assoc, descOfIsLeftKanExtension_fac_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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₂
dsimp :
  NatTrans.app L.lanUnit F ≫ L.whiskerLeft β ≫ L.whiskerLeft f =
    (NatTrans.app L.lanUnit F ≫ L.whiskerLeft β) ≫ L.whiskerLeft f
⊢ 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₂)

Tactic:
dsimp [homEquivOfIsLeftKanExtension]

Premises used: CategoryTheory.Functor.homEquivOfIsLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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₂
rw rw₁ :
  NatTrans.app L.lanUnit F ≫ L.whiskerLeft β ≫ L.whiskerLeft f =
    NatTrans.app L.lanUnit F ≫ L.whiskerLeft β ≫ L.whiskerLeft f
⊢ NatTrans.app L.lanUnit F ≫ L.whiskerLeft β ≫ L.whiskerLeft f =
    (NatTrans.app L.lanUnit F ≫ L.whiskerLeft β) ≫ L.whiskerLeft f

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
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)
⊢ 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

Tactic:
ext F : 2
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
w : NatTrans.app L.lanUnit F ≫ 𝟙 (L ⋙ obj L.lan F) = NatTrans.app L.lanUnit 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)
    (NatTrans.app (Adjunction.unit (L.lanAdjunction H)) F) (NatTrans.app L.lanUnit F)

Tactic:
dsimp [lanAdjunction, homEquivOfIsLeftKanExtension]

Premises used: CategoryTheory.Functor.homEquivOfIsLeftKanExtension, CategoryTheory.Functor.lanAdjunction
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
⊢ NatTrans.app L.lanUnit F ≫ 𝟙 (L ⋙ obj L.lan F) = NatTrans.app L.lanUnit F

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
G : Functor.{v_2, v_3, u_2, u_3} D H
⊢ NatTrans.app (Adjunction.counit (L.lanAdjunction H)) G =
    (obj L.lan (L ⋙ G)).descOfIsLeftKanExtension (NatTrans.app L.lanUnit (L ⋙ G)) G (𝟙 (L ⋙ G))

Tactic:
rfl

Premises used: CategoryTheory.Functor.descOfIsLeftKanExtension, CategoryTheory.StructuredArrow.IsUniversal.desc, CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
G : Functor.{v_2, v_3, u_2, u_3} D H
⊢ CategoryStruct.comp (Y := obj (L.lan ⋙ obj (whiskeringLeft C D H) L) (L ⋙ G)) (NatTrans.app L.lanUnit (L ⋙ G))
      (L.whiskerLeft (NatTrans.app (Adjunction.counit (L.lanAdjunction H)) G)) =
    𝟙 (L ⋙ G)

Tactic:
simp [lanAdjunction_counit_app]

Premises used: CategoryTheory.Functor.lanAdjunction_counit_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
G : Functor.{v_2, v_3, u_2, u_3} D H
X : C
⊢ CategoryStruct.comp (Y := (obj (L.lan ⋙ obj (whiskeringLeft C D H) L) (L ⋙ G)).obj X)
      (NatTrans.app (NatTrans.app L.lanUnit (L ⋙ G)) X)
      (NatTrans.app (NatTrans.app (Adjunction.counit (L.lanAdjunction H)) G) (L.obj X)) =
    𝟙 ((obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) (L ⋙ G)).obj X)

Tactic:
congr_app (L.lanUnit_app_whiskerLeft_lanAdjunction_counit_app G) X

Premises used: CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
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
G : Functor.{v_2, v_3, u_2, u_3} D H
⊢ CategoryStruct.comp (Y := L ⋙ obj L.lan (L ⋙ G)) (NatTrans.app L.lanUnit (L ⋙ G))
      (L.whiskerLeft (NatTrans.app (Adjunction.counit (L.lanAdjunction H)) G)) =
    𝟙 (L ⋙ G)

Tactic:
simp