mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ p.fst)) = op (CostructuredArrow.mk (map₂ F f p).fst)

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 (F'.liftOfIsRightKanExtension α G' (β ≫ i.inv) ≫ G'.liftOfIsRightKanExtension β F' (α ≫ i.hom)) ≫ β =
    L.whiskerLeft (𝟙 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
p : YonedaCollection F Y
⊢ (map₂ F f p).snd = (ConcreteCategory.hom (F.map ((CostructuredArrow.mkPrecomp p.fst f).op ≫ eqToHom ⋯))) p.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
⊢ map₁ (𝟙 F) = id

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

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : F''.IsRightKanExtension α'
⊢ L.whiskerLeft φ ≫ α = L.whiskerLeft (F''.rightKanExtensionUnique α' F' α).hom ≫ α

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
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : StructuredArrow Y₂ L
⊢ ((CostructuredArrow.left G).map φ ≫ (h Y₂).lift (G.coneAt Y₂)) ≫ (E.coneAt Y₂).π.app X =
    ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app 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
⊢ (L.ranAdjunction H).counit = L.ranCounit

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
G : D ⥤ H
⊢ L.whiskerLeft ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ 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.HasRightKanExtension F
F : C ⥤ H
G : D ⥤ H
α : L ⋙ G ⟶ F
⊢ L.whiskerLeft (((L.ranAdjunction H).homEquiv G F) α) ≫ L.ranCounit.app F = α

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
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
⊢ ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
      CostructuredArrow.hom E =
    CostructuredArrow.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 : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
⊢ map₁ (η ≫ μ) = map₁ μ ∘ map₁ η

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α' ↔ IsIso φ

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
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
G : D ⥤ H
β : F' ⟶ G
⊢ α ≫ L.whiskerLeft ((fun β ↦ F'.descOfIsLeftKanExtension α G β) ((fun β ↦ α ≫ L.whiskerLeft β) β)) =
    α ≫ L.whiskerLeft β

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
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
G : D ⥤ H
⊢ Function.RightInverse (fun β ↦ F'.descOfIsLeftKanExtension α 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
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
⊢ ((L.ran ⋙ lim).map f ≫ ((L.ran.obj Y✝).limitIsoOfIsRightKanExtension (L.ranCounit.app Y✝)).hom) ≫ limit.π Y✝ i =
    (((L.ran.obj X✝).limitIsoOfIsRightKanExtension (L.ranCounit.app X✝)).hom ≫ lim.map f) ≫ limit.π Y✝ i

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.HasPointwiseRightKanExtension F
⊢ IsIso L.ranCounit

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
⊢ map₂ F (𝟙 X) = id

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.HasPointwiseRightKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ IsIso ((L.ranAdjunction H).counit.app 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
inst✝ : ∀ (F : C ⥤ H), L.HasPointwiseRightKanExtension F
⊢ IsIso (L.ranAdjunction H).counit

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

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
α : F ⟶ L ⋙ F'
inst✝¹ : F'.IsLeftKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : G ⟶ L ⋙ G'
inst✝ : G'.IsLeftKanExtension β
⊢ α ≫ L.whiskerLeft (F'.descOfIsLeftKanExtension α G' (i.hom ≫ β) ≫ G'.descOfIsLeftKanExtension β F' (i.inv ≫ α)) =
    α ≫ L.whiskerLeft (𝟙 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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
⊢ f₁ = 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
α : F ⟶ L ⋙ F'
inst✝¹ : F'.IsLeftKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : G ⟶ L ⋙ G'
inst✝ : G'.IsLeftKanExtension β
⊢ β ≫ L.whiskerLeft (G'.descOfIsLeftKanExtension β F' (i.inv ≫ α) ≫ F'.descOfIsLeftKanExtension α G' (i.hom ≫ β)) =
    β ≫ L.whiskerLeft (𝟙 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
inst✝ : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : CostructuredArrow L Y₁
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.proj L Y₁ ⋙ F).map φ ≫
      colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g₂) =
    colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g₁) ≫
      ((const (CostructuredArrow L Y₁)).obj (colimit (CostructuredArrow.proj L Y₂ ⋙ F))).map φ

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
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
a✝ : F''.IsLeftKanExtension α'
⊢ α ≫ L.whiskerLeft φ = α ≫ L.whiskerLeft (F'.leftKanExtensionUnique α F'' α').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 : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ map₂ F (f ≫ g) = map₂ F f ∘ map₂ 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
inst✝ : L.HasPointwiseLeftKanExtension F
Y : D
j : CostructuredArrow L Y
⊢ colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y ⋙ F) ((CostructuredArrow.map (𝟙 Y)).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L Y ⋙ F))

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
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α' ↔ IsIso φ

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'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝¹ : G.IsEquivalence
f : L' ⟶ L ⋙ G
inst✝ : IsIso f
F : C ⥤ H
⊢ (LeftExtension.postcomp₁ G f F).IsEquivalence

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'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝¹ : G.IsEquivalence
f : L ⋙ G ⟶ L'
inst✝ : IsIso f
F : C ⥤ H
⊢ (RightExtension.postcomp₁ G f F).IsEquivalence

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'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
ex : L'.LeftExtension F
⊢ StructuredArrow.IsUniversal ex ≃ StructuredArrow.IsUniversal ((postcomp₁ G e.inv F).obj ex)

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
inst✝ : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj g),
                naturality := ⋯ } }

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'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
ex : L'.RightExtension F
⊢ CostructuredArrow.IsUniversal ex ≃ CostructuredArrow.IsUniversal ((postcomp₁ G e.hom F).obj ex)

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
inst✝ : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) =
    colimit.ι (CostructuredArrow.proj L (L.obj X₁) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁))) ≫
      (L ⋙ L.pointwiseLeftKanExtension F).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
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ map₂ G f (map₁ η p) = map₁ η (map₂ F f p)

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
inst✝ : L.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
⊢ (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).ι.app j ≫
      (Iso.refl (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).pt).hom =
    ((LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F)).coconeAt X).ι.app j

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
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
⊢ ∀ ⦃X Y_1 : CostructuredArrow L Y⦄ (f : X ⟶ Y_1),
    (CostructuredArrow.proj L Y ⋙ F).map f ≫ α.app Y_1.left ≫ G.map Y_1.hom =
      (α.app X.left ≫ G.map X.hom) ≫ ((const (CostructuredArrow L Y)).obj (G.obj Y)).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
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun Y ↦ colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit 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 G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    (yonedaCollectionPresheaf A F).map f ≫ ↾YonedaCollection.map₁ η =
      ↾YonedaCollection.map₁ η ≫ (yonedaCollectionPresheaf A G).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
⊢ ∀ {Y Z : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (g : Y ⟶ Z),
    (yonedaCollectionFunctor A).map g ≫ yonedaCollectionPresheafToA Z = yonedaCollectionPresheafToA Y

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
p : YonedaCollection (restrictedYonedaObj η) X
⊢ unitForward μ X (YonedaCollection.map₁ (restrictedYonedaObjMap₁ ε hε) p) =
    (ConcreteCategory.hom (ε.app (op X))) (unitForward η X p)

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
p : YonedaCollection (restrictedYonedaObj η) Y
⊢ unitForward η X (YonedaCollection.map₂ (restrictedYonedaObj η) f p) =
    (ConcreteCategory.hom (F.map f.op)) (unitForward η Y p)

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
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

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 : Cᵒᵖ
p : YonedaCollection (restrictedYonedaObj η) (unop X)
⊢ (ConcreteCategory.hom (η.app X)) (unitForward η (unop X) p) = p.yonedaEquivFst

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 : C
x : F.obj (op X)
⊢ (ConcreteCategory.hom
        (η.app
          (op (unop (op (CostructuredArrow.mk (yonedaEquiv.symm ((ConcreteCategory.hom (η.app (op X))) x))))).left)))
      x =
    yonedaEquiv (unop (op (CostructuredArrow.mk (yonedaEquiv.symm ((ConcreteCategory.hom (η.app (op X))) x))))).hom

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
inst✝ : L.HasPointwiseRightKanExtension F
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : StructuredArrow Y₂ L
φ : g₁ ⟶ g₂
⊢ ((const (StructuredArrow Y₂ L)).obj (limit (StructuredArrow.proj Y₁ L ⋙ F))).map φ ≫
      limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g₂) =
    limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g₁) ≫ (StructuredArrow.proj Y₂ L ⋙ F).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 F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
x : F.obj (op X)
⊢ (unitForward η X ∘ unitBackward η X) x = id x

Tactic:
by

Goal state after: