mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
L✝ : C ⥤ D
H : Type u_3
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : ∀ (F : C ⥤ H), L✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ limMap (L.ran.map f) ≫ limit.π (L.ran.obj Y✝) (L.obj i) ≫ (L.ranCounit.app Y✝).app i =
    limit.π (L.ran.obj X✝) (L.obj i) ≫ (L.ranCounit.app X✝).app i ≫ f.app i

Tactic:
limMap_π_assoc

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
L✝ : C ⥤ D
H : Type u_3
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : ∀ (F : C ⥤ H), L✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ limit.π (L.ran.obj X✝) (L.obj i) ≫ (L.ran.map f).app (L.obj i) ≫ (L.ranCounit.app Y✝).app i =
    limit.π (L.ran.obj X✝) (L.obj i) ≫ (L.ranCounit.app X✝).app i ≫ f.app i
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ F'.IsLeftKanExtension α → F''.IsLeftKanExtension α'

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ F''.IsLeftKanExtension α' → F'.IsLeftKanExtension α

Tactic:
·

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ F'.IsLeftKanExtension α → F''.IsLeftKanExtension α'
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ F''.IsLeftKanExtension α' → F'.IsLeftKanExtension α

Tactic:
·

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ F''.IsLeftKanExtension α' → F'.IsLeftKanExtension α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α' → IsIso φ

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ IsIso φ → F''.IsLeftKanExtension α'

Tactic:
·

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α' → IsIso φ
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ IsIso φ → F''.IsLeftKanExtension α'

Tactic:
·

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ IsIso φ → F''.IsLeftKanExtension α'
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) := ⋯
⊢ F'.IsLeftKanExtension α → (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) := ⋯
⊢ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α

Tactic:
·

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) := ⋯
⊢ F'.IsLeftKanExtension α → (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) := ⋯
⊢ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α

Tactic:
·

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) := ⋯
⊢ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((ConcreteCategory.hom ((restrictedYonedaObj η).map (eqToHom ⋯))) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((ConcreteCategory.hom ((restrictedYonedaObj η).map (eqToHom ⋯))) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((ConcreteCategory.hom ((restrictedYonedaObj η).map (eqToHom ⋯))) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) := ⋯
⊢ F'.IsRightKanExtension α → (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) := ⋯
⊢ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α

Tactic:
·

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) := ⋯
⊢ F'.IsRightKanExtension α → (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) := ⋯
⊢ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α

Tactic:
·

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) := ⋯
⊢ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension α → F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)

pp: case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α

Tactic:
·

Goal state after:
case mp
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension α → F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α

Tactic:
·

Goal state after:
case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ (X : C ⥤ D) →
    (prod.functor.obj F ⋙ (evaluation C D).obj k).obj X ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj X

pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ Iso.hom (?m.163 Y) =
      Iso.hom (?m.163 X) ≫ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f

Tactic:
·

Goal state after:
C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ (X : C ⥤ D) →
    (prod.functor.obj F ⋙ (evaluation C D).obj k).obj X ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj X
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F Y)).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F X)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f

Tactic:
·

Goal state after:
C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F Y)).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F X)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) := ⋯
⊢ F'.IsRightKanExtension α → F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)

pp: case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) := ⋯
⊢ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α) → F'.IsRightKanExtension α

Tactic:
·

Goal state after:
case mp
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) := ⋯
⊢ F'.IsRightKanExtension α → F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) := ⋯
⊢ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α) → F'.IsRightKanExtension α

Tactic:
·

Goal state after:
case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) := ⋯
⊢ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α) → F'.IsRightKanExtension α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) := ⋯
⊢ F₁'.IsLeftKanExtension α₁ → F₂'.IsLeftKanExtension α₂

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) := ⋯
⊢ F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁

Tactic:
·

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) := ⋯
⊢ F₁'.IsLeftKanExtension α₁ → F₂'.IsLeftKanExtension α₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) := ⋯
⊢ F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁

Tactic:
·

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) := ⋯
⊢ F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁