mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinsetObj F),
        ι := Discrete.natTrans fun j ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    { pt := colimit (liftToFinsetObj F),
                ι :=
                  Discrete.natTrans fun j ↦
                    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.ι.app
          j ≫
        m =
      s.ι.app j
⊢ m =
    colimit.desc (liftToFinsetObj F)
      { pt := s.pt, ι := { app := fun x ↦ Sigma.desc fun x_1 ↦ s.ι.app ↑x_1, naturality := ⋯ } }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
e_1✝ : (f (↑j).as ⟶ ∐ f) = ((Discrete.functor f).obj ↑j ⟶ (colimit.cocone (Discrete.functor f)).pt)
e_3✝ : f (↑j).as = (Discrete.functor f).obj ↑j
e_4✝ : colimit (liftToFinsetObj (Discrete.functor f)) = (liftToFinsetColimitCocone (Discrete.functor f)).cocone.pt
⊢ {↑j} ⊆ S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
⊢ ∀ (j : Finset (Discrete α)),
    (colimit.cocone (liftToFinsetObj (Discrete.functor f))).ι.app j ≫
        ((liftToFinsetColimitCocone (Discrete.functor f)).isColimit.coconePointUniqueUpToIso
            (colimit.isColimit (Discrete.functor f))).hom =
      (finiteSubcoproductsCocone f).ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape (Discrete α) C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ C
J : Finset (Discrete α)
j : ↥J
⊢ Sigma.ι (fun x ↦ F.obj ↑x) j ≫
      colimit.ι (liftToFinsetObj F) J ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone F)).inv =
    colimit.ι F ↑j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasColimitsOfShape (Discrete α) C
X✝ Y✝ : Discrete α ⥤ C
β : X✝ ⟶ Y✝
⊢ (liftToFinset C α ⋙ colim).map β ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone Y✝)).symm.hom =
    (colimit.isoColimitCocone (liftToFinsetColimitCocone X✝)).symm.hom ≫ colim.map β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteCoproducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
⊢ (liftToFinset C α ⋙ (evaluation (Finset (Discrete α)) C).obj I).map x✝ ≫
      (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Y✝.obj ↑x).obj x))).hom =
    (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ X✝.obj ↑x).obj x))).hom ≫
      ((Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C).obj (Discrete.functor fun x ↦ ↑x) ⋙ colim).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
j : Discrete α
⊢ j ∈ {j}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
⊢ m =
    limit.lift (liftToFinsetObj F)
      { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
f : α → C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
j : ↥(unop S)
⊢ {↑j} ⊆ unop S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
f : α → C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasProduct f
⊢ ∀ (j : (Finset (Discrete α))ᵒᵖ),
    (limit.cone (liftToFinsetObj (Discrete.functor f))).π.app j =
      ((liftToFinsetLimitCone (Discrete.functor f)).isLimit.conePointUniqueUpToIso
            (limit.isLimit (Discrete.functor f))).hom ≫
        (finiteSubproductsCone f).π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasLimitsOfShape (Discrete α) C
X✝ Y✝ : Discrete α ⥤ C
β : X✝ ⟶ Y✝
⊢ (liftToFinset C α ⋙ lim).map β ≫ (limit.isoLimitCone (liftToFinsetLimitCone Y✝)).symm.hom =
    (limit.isoLimitCone (liftToFinsetLimitCone X✝)).symm.hom ≫ lim.map β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteProducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
⊢ (liftToFinset C α ⋙ (evaluation (Finset (Discrete α))ᵒᵖ C).obj (op I)).map x✝ ≫
      (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Y✝.obj ↑x).obj x))).hom =
    (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ X✝.obj ↑x).obj x))).hom ≫
      ((Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C).obj (Discrete.functor fun x ↦ ↑x) ⋙ lim).map x✝

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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
⊢ L.HasPointwiseLeftKanExtensionAt F Y₁ ↔ L.HasPointwiseLeftKanExtensionAt F Y₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : Dᵒᵖ
x✝ : ↑(Cat.of (StructuredArrow (Opposite.unop d) T))
left✝ : Discrete PUnit.{1}
right✝ : C
hom✝ : (Functor.fromPUnit (Opposite.unop d)).obj left✝ ⟶ T.obj right✝
⊢ (map (𝟙 d).unop).toCatHom.toFunctor.obj { left := left✝, right := right✝, hom := hom✝ } =
    (𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T))).toFunctor.obj { left := left✝, right := right✝, hom := hom✝ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : Dᵒᵖ
⊢ (map (𝟙 d).unop).toCatHom = 𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
X✝ Y✝ Z✝ : Dᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(Cat.of (StructuredArrow (Opposite.unop X✝) T))
⊢ (map (f ≫ g).unop).toCatHom.toFunctor.obj x✝ = ((map f.unop).toCatHom ≫ (map g.unop).toCatHom).toFunctor.obj x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
X✝ Y✝ Z✝ : Dᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (map (f ≫ g).unop).toCatHom = (map f.unop).toCatHom ≫ (map g.unop).toCatHom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : D
x✝ : ↑(Cat.of (CostructuredArrow T d))
left✝ : C
right✝ : Discrete PUnit.{1}
hom✝ : T.obj left✝ ⟶ (Functor.fromPUnit d).obj right✝
⊢ (map (𝟙 d)).toCatHom.toFunctor.obj { left := left✝, right := right✝, hom := hom✝ } =
    (𝟙 (Cat.of (CostructuredArrow T d))).toFunctor.obj { left := left✝, right := right✝, hom := hom✝ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : D
⊢ (map (𝟙 d)).toCatHom = 𝟙 (Cat.of (CostructuredArrow T d))

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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
⊢ L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(Cat.of (CostructuredArrow T X✝))
⊢ (map (f ≫ g)).toCatHom.toFunctor.obj x✝ = ((map f).toCatHom ≫ (map g).toCatHom).toFunctor.obj x✝

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
L' : C ⥤ D
e : L ≅ L'
Y : D
⊢ L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (map (f ≫ g)).toCatHom = (map f).toCatHom ≫ (map g).toCatHom

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
L' : C ⥤ D
e : L ≅ L'
Y : D
⊢ L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
L : C ⥤ D
R : E ⥤ D
X✝ Y✝ : Grothendieck (R ⋙ functor L)
f : X✝ ⟶ Y✝
⊢ L.map f.fiber.left ≫ { left := left Y✝.fiber, right := Y✝.base, hom := hom Y✝.fiber }.hom =
    { left := left X✝.fiber, right := X✝.base, hom := hom X✝.fiber }.hom ≫ R.map f.base

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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
⊢ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
L : C ⥤ D
R : E ⥤ D
X : E
X✝ Y✝ : ↑((R ⋙ functor L).obj X)
x✝ : X✝ ⟶ Y✝
⊢ (Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).map x✝ ≫
      (Iso.refl
          ((Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj Y✝)).hom =
    (Iso.refl ((Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X✝)).hom ≫
      (proj L (R.obj X)).map x✝

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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
L : C ⥤ D
R : E ⥤ D
X : Comma L R
⊢ eqToHom ⋯ ≫ { base := (𝟙 X).right, fiber := homMk (𝟙 X).left ⋯ }.fiber =
    (𝟙 { base := X.right, fiber := mk X.hom }).fiber

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
L : C ⥤ D
R : E ⥤ D
X✝ Y✝ Z✝ : Comma L R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ { base := (f ≫ g).right, fiber := homMk (f ≫ g).left ⋯ }.fiber =
    ({ base := f.right, fiber := homMk f.left ⋯ } ≫ { base := g.right, fiber := homMk g.left ⋯ }).fiber

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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
⊢ L'.HasPointwiseRightKanExtensionAt F Y'

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₁ F₂ : C ⥤ H
φ : F₁ ⟶ F₂
⊢ (𝟭 (C ⥤ H)).map φ ≫ L.leftKanExtensionUnit F₂ =
    L.leftKanExtensionUnit F₁ ≫ (L.lan ⋙ (whiskeringLeft C D H).obj L).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.HasLeftKanExtension F
F : C ⥤ H
⊢ (L.lan.obj F).IsLeftKanExtension (L.lanUnit.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
F : C ⥤ H
inst✝¹ : L.HasPointwiseLeftKanExtension F
inst✝ : L.HasLeftKanExtension F
X : D
f : CostructuredArrow L X
⊢ colimit.ι (proj L X ⋙ F) f ≫ (L.leftKanExtensionObjIsoColimit F X).inv =
    (L.leftKanExtensionUnit F).app f.left ≫ (L.leftKanExtension F).map f.hom

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
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X : C
⊢ (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj 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
F : C ⥤ H
inst✝¹ : L.HasPointwiseLeftKanExtension F
inst✝ : L.HasLeftKanExtension F
this : ∀ (X : D), HasColimit (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) :=
  fun X ↦
    hasColimit_of_iso
      (isoWhiskerRight (eqToIso (id (congrArg Cat.Hom.toFunctor ((functor L).map_id X))))
            (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) ≪≫
          (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F).leftUnitor).symm
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ ∀ (j : ↑((functor L).obj X✝)),
    colimit.ι (Grothendieck.ι (functor L) X✝ ⋙ grothendieckProj L ⋙ F) j ≫
        (fiberwiseColimit (grothendieckProj L ⋙ F)).map f ≫
          (HasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L Y✝) F) ≪≫
              (L.leftKanExtensionObjIsoColimit F Y✝).symm).hom =
      colimit.ι (Grothendieck.ι (functor L) X✝ ⋙ grothendieckProj L ⋙ F) j ≫
        (HasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L X✝) F) ≪≫
              (L.leftKanExtensionObjIsoColimit F X✝).symm).hom ≫
          (L.leftKanExtension F).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
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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y'

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 L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L'.HasPointwiseLeftKanExtensionAt F' Y

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 L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L'.HasPointwiseRightKanExtensionAt F' Y

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
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.proj L Y ⋙ F).map φ ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫
      ((const (CostructuredArrow L Y)).obj ((StructuredArrow.right E).obj Y)).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
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app G ≫ (StructuredArrow.Hom.right φ).app Y = (E'.coconeAt Y).ι.app 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
X : C
h : E.IsPointwiseLeftKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso ((StructuredArrow.hom E).app X)

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
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseLeftKanExtensionAt Y
⊢ (fun h ↦ E.isPointwiseLeftKanExtensionAtOfIso' h e.symm) ((fun h ↦ E.isPointwiseLeftKanExtensionAtOfIso' 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 : L.LeftExtension F
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseLeftKanExtensionAt Y'
⊢ (fun h ↦ E.isPointwiseLeftKanExtensionAtOfIso' h e) ((fun h ↦ E.isPointwiseLeftKanExtensionAtOfIso' h e.symm) 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₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
⊢ L.lanUnit.app F₁ ≫ L.whiskerLeft (((L.lan.obj F₁).homEquivOfIsLeftKanExtension (L.lanUnit.app F₁) G).symm (f ≫ α)) =
    L.lanUnit.app F₁ ≫
      L.whiskerLeft (L.lan.map f ≫ ((L.lan.obj F₂).homEquivOfIsLeftKanExtension (L.lanUnit.app 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
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
T : H
f g : (StructuredArrow.right E).obj Y ⟶ T
hfg :
  ∀ ⦃X : C⦄ (φ : L.obj X ⟶ Y),
    (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ f =
      (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ g
j : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app j ≫ f = (E.coconeAt Y).ι.app j ≫ 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
F : C ⥤ H
G₁ G₂ : D ⥤ H
β : L.lan.obj F ⟶ G₁
f : G₁ ⟶ G₂
⊢ ((L.lan.obj F).homEquivOfIsLeftKanExtension (L.lanUnit.app F) G₂) (β ≫ f) =
    ((L.lan.obj F).homEquivOfIsLeftKanExtension (L.lanUnit.app F) G₁) β ≫ ((whiskeringLeft C D H).obj L).map f

Tactic:
by

Goal state after: