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.HasLeftKanExtension F
⊢ (L.lanAdjunction H).unit = L.lanUnit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
Z : H
φ : CostructuredArrow.proj L Y ⋙ F ⟶ (const (CostructuredArrow L Y)).obj Z
g : CostructuredArrow L Y
⊢ (StructuredArrow.hom E).app g.left ≫ (StructuredArrow.right E).map g.hom ≫ (IsColimit.homEquiv h).symm φ = φ.app g

Tactic:
by

Goal state after:
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.HasLeftKanExtension F
G : D ⥤ H
⊢ L.lanUnit.app (L ⋙ G) ≫ L.whiskerLeft ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
inst✝ : HasColimit (CostructuredArrow.proj L Y ⋙ F)
g : CostructuredArrow L Y
⊢ (StructuredArrow.hom E).app g.left ≫ (StructuredArrow.right E).map g.hom ≫ h.isoColimit.hom =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.LeftExtension F
e : E ≅ E'
h : E.IsPointwiseLeftKanExtension
⊢ (fun h Y ↦ (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y))
      ((fun h Y ↦ (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y)) h) =
    h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.LeftExtension F
e : E ≅ E'
h : E'.IsPointwiseLeftKanExtension
⊢ (fun h Y ↦ (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y))
      ((fun h Y ↦ (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y)) h) =
    h

Tactic:
by

Goal state after:
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.HasLeftKanExtension F
F : C ⥤ H
G : D ⥤ H
α : F ⟶ L ⋙ G
⊢ L.lanUnit.app F ≫ L.whiskerLeft (((L.lanAdjunction H).homEquiv F G).symm α) = α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (E.coconeAt Y₁).ι.app X ≫ (h Y₁).desc (G.coconeAt Y₁) ≫ (StructuredArrow.right G).map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
⊢ StructuredArrow.hom E ≫
      ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ } =
    StructuredArrow.hom G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : yoneda.obj X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ (ConcreteCategory.hom (μ.app (op X))) ((ConcreteCategory.hom (ε.app (op X))) u) = yonedaEquiv s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X Y : C
f : X ⟶ Y
s : yoneda.obj X ⟶ A
t : yoneda.obj Y ⟶ A
hst : yoneda.map f ≫ t = s
u : F.obj (op Y)
h : MakesOverArrow η t u
⊢ (ConcreteCategory.hom (η.app (op X))) ((ConcreteCategory.hom (F.map f.op)) u) = yonedaEquiv s

Tactic:
by

Goal state after:
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.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ colimit.ι X✝ i ≫ colim.map f ≫ ((L.lan.obj Y✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app Y✝)).symm.hom =
    colimit.ι X✝ i ≫ ((L.lan.obj X✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X✝)).symm.hom ≫ (L.lan ⋙ colim).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
f : X ⟶ Y
hf : yoneda.map f ≫ η = s
⊢ MakesOverArrow η s f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
f : X ⟶ Y
hf : yoneda.map f ≫ η = s
⊢ MakesOverArrow η s f

Tactic:
by
  simpa only [yonedaEquiv_yoneda_map f] using of_arrow hf

Goal state after:
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
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : Grothendieck (CostructuredArrow.functor L)
⊢ colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X ≫ (L.colimitIsoColimitGrothendieck G).inv =
    colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber)

Tactic:
by

Goal state after:
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
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : C
⊢ colimit.ι G X ≫ (L.colimitIsoColimitGrothendieck G).hom =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
      { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
p : OverArrows η s
⊢ yoneda.map p.val ≫ η = s

Tactic:
by

Goal state after:
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✝² : L.Full
inst✝¹ : L.Faithful
inst✝ : ∀ (F : C ⥤ H), L.HasPointwiseLeftKanExtension F
⊢ IsIso L.lanUnit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
s t : CostructuredArrow yoneda A
p : OverArrows s.hom t.hom
⊢ yoneda.map p.val ≫ s.hom = t.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    ((CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A).obj s).map f ≫
        (OverArrows.costructuredArrowIso s (unop Y)).hom =
      (OverArrows.costructuredArrowIso s (unop X)).hom ≫ (yoneda.obj s).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
⊢ ∀ {X Y : CostructuredArrow yoneda A} (f : X ⟶ Y),
    (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A).map f ≫
        (NatIso.ofComponents (fun x ↦ OverArrows.costructuredArrowIso Y (unop x)) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ OverArrows.costructuredArrowIso X (unop x)) ⋯).hom ≫ yoneda.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
⊢ f₁ = f₂

Tactic:
by

Goal state after:
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✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseLeftKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
⊢ IsIso ((L.lanAdjunction H).unit.app F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk g') = op (CostructuredArrow.mk g)

Tactic:
by

Goal state after:
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✝² : L.Full
inst✝¹ : L.Faithful
inst✝ : ∀ (F : C ⥤ H), L.HasPointwiseLeftKanExtension F
⊢ IsIso (L.lanAdjunction H).unit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ g')) = op (CostructuredArrow.mk (yoneda.map f ≫ g))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ (ConcreteCategory.hom (F.map (CostructuredArrow.mkPrecomp g f).op)) ((ConcreteCategory.hom (F.map (eqToHom ⋯))) x) =
    (ConcreteCategory.hom (F.map (eqToHom ⋯))) ((ConcreteCategory.hom (F.map (CostructuredArrow.mkPrecomp g' f).op)) x)

Tactic:
by

Goal state after:
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
F₁ F₂ : C ⥤ H
φ : F₁ ⟶ F₂
⊢ (L.ran ⋙ (whiskeringLeft C D H).obj L).map φ ≫ L.rightKanExtensionCounit F₂ =
    L.rightKanExtensionCounit F₁ ≫ (𝟭 (C ⥤ H)).map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ op (CostructuredArrow.mk s) = op (CostructuredArrow.mk (yonedaEquiv.symm (yonedaEquiv s)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
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
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
G : D ⥤ H
β : G ⟶ F'
⊢ L.whiskerLeft ((fun β ↦ F'.liftOfIsRightKanExtension α G β) ((fun β ↦ L.whiskerLeft β ≫ α) β)) ≫ α =
    L.whiskerLeft β ≫ α

Tactic:
by

Goal state after:
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
F : C ⥤ H
⊢ (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
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
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
G : D ⥤ H
⊢ Function.RightInverse (fun β ↦ F'.liftOfIsRightKanExtension α G β) fun β ↦ L.whiskerLeft β ≫ α

Tactic:
by

Goal state after:
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
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
f : StructuredArrow X L
⊢ (L.ranObjObjIsoLimit F X).hom ≫ limit.π (StructuredArrow.proj X L ⋙ F) f =
    (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ op (CostructuredArrow.mk s) = op (CostructuredArrow.mk (mk s x).fst)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p q : YonedaCollection F X
h : p.fst = q.fst
⊢ op (CostructuredArrow.mk q.fst) = op (CostructuredArrow.mk p.fst)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
⊢ ((const (StructuredArrow Y L)).obj ((CostructuredArrow.left E).obj Y)).map φ ≫
      (CostructuredArrow.left E).map g₂.hom ≫ (CostructuredArrow.hom E).app g₂.right =
    ((CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right) ≫
      (StructuredArrow.proj Y L ⋙ F).map φ

Tactic:
by

Goal state after:
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
F₁ F₂ : D ⥤ H
G : C ⥤ H
β : F₁ ⟶ F₂
f : F₂ ⟶ L.ran.obj G
⊢ ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F₁).symm.symm (β ≫ f) =
    ((whiskeringLeft C D H).obj L).map β ≫
      ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F₂).symm.symm f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = fst ⟨p, q'⟩
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) (snd ⟨p, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩.snd ≍ ⟨p, q'⟩.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p q : YonedaCollection F X
h : p.fst = q.fst
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) q.snd = p.snd
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E✝ E'✝ : L.RightExtension F
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
⊢ φ.left.app Y ≫ (E'.coneAt Y).π.app G = (E.coneAt Y).π.app G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).fst = p.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
X : C
h : E.IsPointwiseRightKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso ((CostructuredArrow.hom E).app X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).yonedaEquivFst = p.yonedaEquivFst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseRightKanExtensionAt Y
⊢ (fun h ↦ E.isPointwiseRightKanExtensionAtOfIso' h e.symm) ((fun h ↦ E.isPointwiseRightKanExtensionAtOfIso' h e) h) = h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseRightKanExtensionAt Y'
⊢ (fun h ↦ E.isPointwiseRightKanExtensionAtOfIso' h e) ((fun h ↦ E.isPointwiseRightKanExtensionAtOfIso' h e.symm) h) = h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk (map₁ η p).fst)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
Y : D
h : E.IsPointwiseRightKanExtensionAt Y
inst✝ : HasLimit (StructuredArrow.proj Y L ⋙ F)
g : StructuredArrow Y L
⊢ h.isoLimit.inv ≫ (CostructuredArrow.left E).map g.hom ≫ (CostructuredArrow.hom E).app g.right =
    limit.π (StructuredArrow.proj Y L ⋙ F) g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).snd =
    (ConcreteCategory.hom (G.map (eqToHom ⋯))) ((ConcreteCategory.hom (η.app (op (CostructuredArrow.mk p.fst)))) p.snd)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: 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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
e : E ≅ E'
h : E.IsPointwiseRightKanExtension
⊢ (fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y))
      ((fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y)) h) =
    h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).fst = yoneda.map f ≫ p.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).yonedaEquivFst = (ConcreteCategory.hom (A.map f.op)) p.yonedaEquivFst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
e : E ≅ E'
h : E'.IsPointwiseRightKanExtension
⊢ (fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y))
      ((fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y)) h) =
    h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
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
inst✝² : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝¹ : F'.IsRightKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : L ⋙ G' ⟶ G
inst✝ : G'.IsRightKanExtension β
⊢ L.whiskerLeft (G'.liftOfIsRightKanExtension β F' (α ≫ i.hom) ≫ F'.liftOfIsRightKanExtension α G' (β ≫ i.inv)) ≫ α =
    L.whiskerLeft (𝟙 F') ≫ α

Tactic:
by

Goal state after: