awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Functor.{v_2, v_3, u_2, u_3} D H
α : F ⟶ L ⋙ G
⊢ CategoryStruct.comp (Y := L ⋙ obj L.lan F) (NatTrans.app L.lanUnit F)
      (L.whiskerLeft
        ((Equiv.symm (Adjunction.homEquiv (L.lanAdjunction H) F G) :
            (a : F ⟶ ((whiskeringLeft C D H).obj L).obj G) → L.lan.obj F ⟶ G)
          α)) =
    α

Tactic:
simp [lanAdjunction]

Premises used: 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
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
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))))
⊢ 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))

Tactic:
dsimp
-- 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
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
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))
⊢ 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:
rw [ι_colimMap_assoc, ι_colimitIsoOfIsLeftKanExtension_inv,
        ι_colimitIsoOfIsLeftKanExtension_inv_assoc, ι_colimMap, ← assoc, ← assoc]

Premises used: CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv_assoc, CategoryTheory.Category.assoc, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv, CategoryTheory.Limits.ι_colimMap_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
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
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))
⊢ 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:
congr 1
-- 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
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 ⟶ (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_app (L.lanUnit.naturality f) i

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.lanUnit, 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
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 ⟶ (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:
exact congr_app (L.lanUnit.naturality f) i

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.lanUnit, 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
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
⊢ HasColimit (CostructuredArrow.grothendieckProj L ⋙ G)

Tactic:
hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit _

Premises used: CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit
-- 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
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 : Grothendieck (CostructuredArrow.functor L)
⊢ Eq (α := (CostructuredArrow.grothendieckProj L ⋙ G).obj X ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.grothendieckProj L ⋙ G))
        (colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X :
          (CostructuredArrow.grothendieckProj L ⋙ G).obj X ⟶ colimit (CostructuredArrow.grothendieckProj L ⋙ G))
        (Iso.inv (L.colimitIsoColimitGrothendieck G) : colimit (CostructuredArrow.grothendieckProj L ⋙ G) ⟶ colimit G) :
      (CostructuredArrow.grothendieckProj L ⋙ G).obj X ⟶ colimit G)
    (colimit.ι G (obj (CostructuredArrow.proj L X.base) X.fiber) :
      G.obj (obj (CostructuredArrow.proj L X.base) X.fiber) ⟶ colimit G)

Tactic:
simp [colimitIsoColimitGrothendieck]

Premises used: CategoryTheory.Functor.colimitIsoColimitGrothendieck
-- 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
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
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))
⊢ 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))

Tactic:
rw [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- 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
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 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:
(ι_colimitIsoColimitGrothendieck_inv L G ⟨L.obj X, .mk (𝟙 _)⟩).symm

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Grothendieck.mk, CategoryTheory.CostructuredArrow.mk, Eq.symm, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, 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
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 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:
exact (ι_colimitIsoColimitGrothendieck_inv L G ⟨L.obj X, .mk (𝟙 _)⟩).symm

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Grothendieck.mk, CategoryTheory.CostructuredArrow.mk, Eq.symm, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, 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
inst_3 : L.Full
inst_4 : L.Faithful
F : Functor.{v_1, v_3, u_1, u_3} C H
X : C
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).obj X) (NatTrans.app (NatTrans.app L.lanUnit F) X)

Tactic:
(isPointwiseLeftKanExtensionLeftKanExtensionUnit L F (L.obj X)).isIso_hom_app

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app, CategoryTheory.Functor.obj, 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
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 L.lanUnit F)

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_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 : L.Full
inst_4 : L.Faithful
inst_5 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasPointwiseLeftKanExtension F
⊢ IsIso (C := Functor.{v_1, v_3, u_1, u_3} C H ⥤ Functor.{v_1, v_3, u_1, u_3} C H) (Y :=
    L.lan ⋙ obj (whiskeringLeft C D H) L) L.lanUnit

Tactic:
apply NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_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 : 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
rw : IsIso (Y := obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app L.lanUnit F)
⊢ IsIso (Y := obj (L.lan ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app (Adjunction.unit (L.lanAdjunction H)) F)

Tactic:
rw [lanAdjunction_unit]

Premises used: CategoryTheory.Functor.lanAdjunction_unit
-- 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 : 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 L.lanUnit 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
inst_3 : L.Full
inst_4 : L.Faithful
inst_5 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasPointwiseLeftKanExtension F
⊢ IsIso (C := Functor.{v_1, v_3, u_1, u_3} C H ⥤ Functor.{v_1, v_3, u_1, u_3} C H) (Y :=
    L.lan ⋙ obj (whiskeringLeft C D H) L) (Adjunction.unit (L.lanAdjunction H))

Tactic:
apply NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_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.HasRightKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
φ : F₁ ⟶ F₂
w :
  ∀ (x : C),
    Eq (α :=
      (obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F₁).obj x ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₂).obj x)
      (NatTrans.app (map (L.ran ⋙ obj (whiskeringLeft C D H) L) φ ≫ L.rightKanExtensionCounit F₂) x)
      (NatTrans.app (L.rightKanExtensionCounit F₁ ≫ map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) φ) x)
⊢ Eq (α := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F₁ ⟶ obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₂)
    (map (L.ran ⋙ obj (whiskeringLeft C D H) L) φ ≫ L.rightKanExtensionCounit F₂)
    (L.rightKanExtensionCounit F₁ ≫ map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) φ)

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.HasRightKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
φ : F₁ ⟶ F₂
x : C
⊢ Eq (α :=
    (obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F₁).obj x ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₂).obj x)
    (NatTrans.app (map (L.ran ⋙ obj (whiskeringLeft C D H) L) φ ≫ L.rightKanExtensionCounit F₂) x)
    (NatTrans.app (L.rightKanExtensionCounit F₁ ≫ map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) φ) x)

Tactic:
simp [ran]

Premises used: CategoryTheory.Functor.ran
-- 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.HasRightKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
dsimp : (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)
⊢ (obj L.ran F).IsRightKanExtension (NatTrans.app L.ranCounit F)

Tactic:
dsimp [ran, ranCounit]

Premises used: CategoryTheory.Functor.ran, CategoryTheory.Functor.ranCounit
-- 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.HasRightKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit 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
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_4 : L.HasPointwiseRightKanExtension F
X : D
f : StructuredArrow X L
⊢ CategoryStruct.comp (Y := limit (StructuredArrow.proj X L ⋙ F)) (Iso.hom (L.ranObjObjIsoLimit F X))
      (limit.π (StructuredArrow.proj X L ⋙ F) f) =
    (obj L.ran F).map f.hom ≫ NatTrans.app (NatTrans.app L.ranCounit F) f.right

Tactic:
simp [ranObjObjIsoLimit, ran, ranCounit]

Premises used: CategoryTheory.Functor.ranObjObjIsoLimit, CategoryTheory.Functor.ran, CategoryTheory.Functor.ranCounit
-- 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.HasRightKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_4 : L.HasPointwiseRightKanExtension F
X : D
f : StructuredArrow X L
⊢ Eq (α := limit (StructuredArrow.proj X L ⋙ F) ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F).obj f.right)
    (Iso.inv (L.ranObjObjIsoLimit F X) ≫ (obj L.ran F).map f.hom ≫ NatTrans.app (NatTrans.app L.ranCounit F) f.right)
    (limit.π (StructuredArrow.proj X L ⋙ F) f)

Tactic:
RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π (F := F)
    (isPointwiseRightKanExtensionRanCounit L F X) f

Premises used: CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π
-- 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.HasRightKanExtension F
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D H
G : Functor.{v_1, v_3, u_1, u_3} C H
β : F₁ ⟶ F₂
f : F₂ ⟶ obj L.ran G
dsimp :
  (L.whiskerLeft β ≫ L.whiskerLeft f) ≫ NatTrans.app L.ranCounit G =
    L.whiskerLeft β ≫ L.whiskerLeft f ≫ NatTrans.app L.ranCounit G
⊢ Eq (α := obj (obj (whiskeringLeft C D H) L) F₁ ⟶ G)
    ((((obj L.ran G).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G) F₁).symm.symm :
          (a : F₁ ⟶ L.ran.obj G) → ((whiskeringLeft C D H).obj L).obj F₁ ⟶ G)
        (β ≫ f) :
      obj (obj (whiskeringLeft C D H) L) F₁ ⟶ G)
    (map (obj (whiskeringLeft C D H) L) β ≫
        (((obj L.ran G).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G) F₂).symm.symm :
            (a : F₂ ⟶ L.ran.obj G) → ((whiskeringLeft C D H).obj L).obj F₂ ⟶ G)
          f :
      obj (obj (whiskeringLeft C D H) L) F₁ ⟶ G)

Tactic:
dsimp [homEquivOfIsRightKanExtension]

Premises used: CategoryTheory.Functor.homEquivOfIsRightKanExtension
-- 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.HasRightKanExtension F
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D H
G : Functor.{v_1, v_3, u_1, u_3} C H
β : F₁ ⟶ F₂
f : F₂ ⟶ obj L.ran G
rw rw₁ :
  L.whiskerLeft β ≫ L.whiskerLeft f ≫ NatTrans.app L.ranCounit G =
    L.whiskerLeft β ≫ L.whiskerLeft f ≫ NatTrans.app L.ranCounit G
⊢ (L.whiskerLeft β ≫ L.whiskerLeft f) ≫ NatTrans.app L.ranCounit G =
    L.whiskerLeft β ≫ L.whiskerLeft f ≫ NatTrans.app L.ranCounit G

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc