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.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
w :
  ∀ (X : C),
    Eq (α := (L ⋙ F).obj X ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂).obj X)
      (NatTrans.app
        (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
          (L.whiskerLeft
            ((((obj L.ran G₂).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F).symm :
                (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₂) → F ⟶ L.ran.obj G₂)
              (β ≫ f)))
          (NatTrans.app L.ranCounit G₂))
        X)
      (NatTrans.app
        (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
          (L.whiskerLeft
            ((((obj L.ran G₁).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F).symm :
                  (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁) → F ⟶ L.ran.obj G₁)
                β ≫
              map L.ran f))
          (NatTrans.app L.ranCounit G₂))
        X)
⊢ Eq (α := L ⋙ F ⟶ obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂)
    (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
      (L.whiskerLeft
        ((((obj L.ran G₂).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F).symm :
            (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₂) → F ⟶ L.ran.obj G₂)
          (β ≫ f)))
      (NatTrans.app L.ranCounit G₂))
    (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
      (L.whiskerLeft
        ((((obj L.ran G₁).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F).symm :
              (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁) → F ⟶ L.ran.obj G₁)
            β ≫
          map L.ran f))
      (NatTrans.app L.ranCounit 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.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
w :
  ((obj L.ran G₂).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F (β ≫ f)).app (L.obj X) ≫
      NatTrans.app (NatTrans.app L.ranCounit G₂) X =
    (((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
        NatTrans.app (map L.ran f) (L.obj X)) ≫
      NatTrans.app (NatTrans.app L.ranCounit G₂) X
⊢ Eq (α := (L ⋙ F).obj X ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂).obj X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
        (L.whiskerLeft
          ((((obj L.ran G₂).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F).symm :
              (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₂) → F ⟶ L.ran.obj G₂)
            (β ≫ f)))
        (NatTrans.app L.ranCounit G₂))
      X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
        (L.whiskerLeft
          ((((obj L.ran G₁).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F).symm :
                (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁) → F ⟶ L.ran.obj G₁)
              β ≫
            map L.ran f))
        (NatTrans.app L.ranCounit G₂))
      X)

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 : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
w :
  β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X
⊢ ((obj L.ran G₂).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F (β ≫ f)).app (L.obj X) ≫
      NatTrans.app (NatTrans.app L.ranCounit G₂) X =
    (((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
        NatTrans.app (map L.ran f) (L.obj X)) ≫
      NatTrans.app (NatTrans.app L.ranCounit G₂) X

Tactic:
rw [liftOfIsRightKanExtension_fac_app, NatTrans.comp_app, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app, CategoryTheory.NatTrans.comp_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 : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
⊢ Eq (α :=
    (obj (L.ran ⋙ obj (whiskeringLeft C D H) L) G₁).obj X ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂).obj X)
    (NatTrans.app (map (L.ran ⋙ obj (whiskeringLeft C D H) L) f ≫ NatTrans.app L.ranCounit G₂) X)
    (NatTrans.app (NatTrans.app L.ranCounit G₁ ≫ map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) f) X)

Tactic:
have h := congr_app (L.ranCounit.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.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
h :
  Eq (α :=
    (obj (L.ran ⋙ obj (whiskeringLeft C D H) L) G₁).obj X ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂).obj X)
    (NatTrans.app (map (L.ran ⋙ obj (whiskeringLeft C D H) L) f ≫ NatTrans.app L.ranCounit G₂) X)
    (NatTrans.app (NatTrans.app L.ranCounit G₁ ≫ map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) f) X)
w :
  β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X
⊢ β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) 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.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
h :
  Eq (α := (obj L.ran G₁).obj (L.obj X) ⟶ G₂.obj X)
    (NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X)
    (NatTrans.app (NatTrans.app L.ranCounit G₁) X ≫ f.app X)
w :
  β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (NatTrans.app L.ranCounit G₁) X ≫ f.app X
w₁ w₂ : β.app X ≫ f.app X = β.app X ≫ f.app X
⊢ β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X

Tactic:
rw [h, liftOfIsRightKanExtension_fac_app_assoc]

Premises used: CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app_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.HasRightKanExtension F
w :
  ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H),
    Eq (α := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F ⟶ obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F)
      (NatTrans.app (Adjunction.counit (L.ranAdjunction H)) F) (NatTrans.app L.ranCounit 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)
      (L.ran ⋙ obj (whiskeringLeft C D H) L) (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)))
    (Adjunction.counit (L.ranAdjunction H)) L.ranCounit

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.HasRightKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
w : 𝟙 (L ⋙ obj L.ran F) ≫ NatTrans.app L.ranCounit F = NatTrans.app L.ranCounit F
⊢ Eq (α := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F ⟶ obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F)
    (NatTrans.app (Adjunction.counit (L.ranAdjunction H)) F) (NatTrans.app L.ranCounit F)

Tactic:
dsimp [ranAdjunction, homEquivOfIsRightKanExtension]

Premises used: CategoryTheory.Functor.ranAdjunction, 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 : Functor.{v_1, v_3, u_1, u_3} C H
⊢ 𝟙 (L ⋙ obj L.ran F) ≫ NatTrans.app L.ranCounit F = NatTrans.app L.ranCounit 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.HasRightKanExtension F
G : Functor.{v_2, v_3, u_2, u_3} D H
⊢ NatTrans.app (Adjunction.unit (L.ranAdjunction H)) G =
    (obj L.ran (L ⋙ G)).liftOfIsRightKanExtension (NatTrans.app L.ranCounit (L ⋙ G)) G (𝟙 (L ⋙ G))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.CostructuredArrow.IsUniversal.lift, rfl, CategoryTheory.Functor.liftOfIsRightKanExtension
-- 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
G : Functor.{v_2, v_3, u_2, u_3} D H
⊢ CategoryStruct.comp (Y := L ⋙ obj (obj (whiskeringLeft C D H) L ⋙ L.ran) G)
      (L.whiskerLeft (NatTrans.app (Adjunction.unit (L.ranAdjunction H)) G)) (NatTrans.app L.ranCounit (L ⋙ G)) =
    𝟙 (L ⋙ G)

Tactic:
simp [ranAdjunction_unit_app]

Premises used: CategoryTheory.Functor.ranAdjunction_unit_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
G : Functor.{v_2, v_3, u_2, u_3} D H
X : C
⊢ CategoryStruct.comp (Y := (obj (obj (whiskeringLeft C D H) L ⋙ L.ran) G).obj (L.obj X))
      (NatTrans.app (NatTrans.app (Adjunction.unit (L.ranAdjunction H)) G) (L.obj X))
      (NatTrans.app (NatTrans.app L.ranCounit (L ⋙ G)) X) =
    𝟙 ((obj (𝟭 (Functor.{v_2, v_3, u_2, u_3} D H)) G).obj (L.obj X))

Tactic:
congr_app (L.ranCounit_app_whiskerLeft_ranAdjunction_unit_app G) X

Premises used: CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_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.HasRightKanExtension F
G : Functor.{v_2, v_3, u_2, u_3} D H
⊢ CategoryStruct.comp (Y := L ⋙ obj L.ran (L ⋙ G))
      (L.whiskerLeft (NatTrans.app (Adjunction.unit (L.ranAdjunction H)) G)) (NatTrans.app L.ranCounit (L ⋙ G)) =
    𝟙 (L ⋙ G)

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.HasRightKanExtension 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
α : L ⋙ G ⟶ F
⊢ CategoryStruct.comp (Y := L ⋙ obj L.ran F)
      (L.whiskerLeft
        ((Adjunction.homEquiv (L.ranAdjunction H) G F :
            (a : ((whiskeringLeft C D H).obj L).obj G ⟶ F) → G ⟶ L.ran.obj F)
          α))
      (NatTrans.app L.ranCounit F) =
    α

Tactic:
simp [ranAdjunction]

Premises used: CategoryTheory.Functor.ranAdjunction
-- 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_1 : 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_1.HasRightKanExtension F
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : ∀ (G : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension G
inst_5 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_6 : HasLimitsOfShape.{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 (α := limit (obj L.ran X) ⟶ Y.obj i)
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := limit (obj L.ran Y)) (limMap (map L.ran f))
        (Iso.hom ((obj L.ran Y).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit Y))))
      (limit.π Y i))
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := limit X)
        (Iso.hom ((obj L.ran X).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit X))) (limMap f))
      (limit.π Y i))
⊢ Eq (α := obj (L.ran ⋙ lim) X ⟶ Y.obj i)
    (CategoryStruct.comp (Y := limit Y)
      (map (L.ran ⋙ lim) f ≫
        Iso.hom
          ((fun (G : Functor.{v_1, v_3, u_1, u_3} C H) ↦
              ((obj L.ran G).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit G) :
                limit (obj L.ran G) ≅ limit (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G)))
            Y))
      (limit.π Y i))
    (CategoryStruct.comp (Y := limit Y)
      (Iso.hom
            ((fun (G : Functor.{v_1, v_3, u_1, u_3} C H) ↦
                ((obj L.ran G).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit G) :
                  limit (obj L.ran G) ≅ limit (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G)))
              X) ≫
          map lim f :
        obj (L.ran ⋙ lim) X ⟶ obj lim Y)
      (limit.π Y i))

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_1 : 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_1.HasRightKanExtension F
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : ∀ (G : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension G
inst_5 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_6 : HasLimitsOfShape.{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 (α := limit (obj L.ran X) ⟶ Y.obj i)
    (limit.π (obj L.ran X) (L.obj i) ≫
      NatTrans.app (map L.ran f) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit Y) i)
    (limit.π (obj L.ran X) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit X) i ≫ f.app i)
⊢ Eq (α := limit (obj L.ran X) ⟶ Y.obj i)
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := limit (obj L.ran Y)) (limMap (map L.ran f))
        (Iso.hom ((obj L.ran Y).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit Y))))
      (limit.π Y i))
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := limit X)
        (Iso.hom ((obj L.ran X).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit X))) (limMap f))
      (limit.π Y i))

Tactic:
rw [assoc, assoc, limMap_π, limitIsoOfIsRightKanExtension_hom_π_assoc,
        limitIsoOfIsRightKanExtension_hom_π, limMap_π_assoc]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Category.assoc, CategoryTheory.Limits.limMap_π_assoc, CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π_assoc, CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π
-- 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_1 : 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_1.HasRightKanExtension F
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : ∀ (G : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension G
inst_5 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_6 : HasLimitsOfShape.{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 (α := (obj L.ran X).obj (L.obj i) ⟶ Y.obj i)
    (NatTrans.app (map L.ran f) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit Y) i)
    (NatTrans.app (NatTrans.app L.ranCounit X) i ≫ f.app i)
⊢ Eq (α := limit (obj L.ran X) ⟶ Y.obj i)
    (limit.π (obj L.ran X) (L.obj i) ≫
      NatTrans.app (map L.ran f) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit Y) i)
    (limit.π (obj L.ran X) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit X) i ≫ f.app 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_1 : 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_1.HasRightKanExtension F
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : ∀ (G : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension G
inst_5 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_6 : HasLimitsOfShape.{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 (α := (obj L.ran X).obj (L.obj i) ⟶ Y.obj i)
    (NatTrans.app (map L.ran f) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit Y) i)
    (NatTrans.app (NatTrans.app L.ranCounit X) i ≫ f.app i)

Tactic:
congr_app (L.ranCounit.naturality f) i

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.ranCounit, 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_1 : 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_1.HasRightKanExtension F
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : ∀ (G : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension G
inst_5 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_6 : HasLimitsOfShape.{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 (α := (obj L.ran X).obj (L.obj i) ⟶ Y.obj i)
    (NatTrans.app (map L.ran f) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit Y) i)
    (NatTrans.app (NatTrans.app L.ranCounit X) i ≫ f.app i)

Tactic:
exact congr_app (L.ranCounit.naturality f) i

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.ranCounit, 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 : L.Full
inst_4 : L.Faithful
F : Functor.{v_1, v_3, u_1, u_3} C H
X : C
inst_5 : L.HasPointwiseRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
⊢ IsIso (X := (obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F).obj X) (NatTrans.app (NatTrans.app L.ranCounit F) X)

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

Premises used: CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app, 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
inst_5 : L.HasPointwiseRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
⊢ IsIso (X := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app L.ranCounit 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.HasPointwiseRightKanExtension 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) (X :=
    L.ran ⋙ obj (whiskeringLeft C D H) L) L.ranCounit

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.HasPointwiseRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
rw : IsIso (X := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app L.ranCounit F)
⊢ IsIso (X := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app (Adjunction.counit (L.ranAdjunction H)) F)

Tactic:
rw [ranAdjunction_counit]

Premises used: CategoryTheory.Functor.ranAdjunction_counit
-- 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.HasPointwiseRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
⊢ IsIso (X := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app L.ranCounit 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.HasPointwiseRightKanExtension 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) (X :=
    L.ran ⋙ obj (whiskeringLeft C D H) L) (Adjunction.counit (L.ranAdjunction H))

Tactic:
apply NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app