mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
⊢ (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j))) ≫
      ((diagram V F₁ F₂).obj (Opposite.op j)).map f =
    (s.π.app j' ≫ enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j'))) ≫
      ((diagram V F₁ F₂).map f.op).app j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

Goal state before:
pp: A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
b : B
⊢ PreservesLimitsOfShape J colim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift g χ'
hφ' : (forget F).IsHomLift (g ≫ f) (χ' ≫ cartesianLift a f)
⊢ g = χ'.base

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

Goal state before:
pp: A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
⊢ IsFiltered A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
⊢ lift s ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
m : s.pt ⟶ (coneFunctorEnrichedHom V F₁ F₂).pt
hm : ∀ (j : J), m ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j
⊢ m = lift s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
⊢ IsFiltered A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ ∃! χ, (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Flat

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsCofiltered D
inst✝ : RepresentablyFlat F
⊢ IsCofiltered C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c } =
    { base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
      { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
⊢ (fiberInclusion.map f).base = 𝟙 S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf : (fiberInclusion.map f).base = 𝟙 S
⊢ (F.map (fiberInclusion.map f).base.op.toLoc).toFunctor.obj
      (fiberInclusion.obj ((Fiber.inducedFunctor ⋯).obj Y)).fiber =
    (F.map (𝟙 { as := op S })).toFunctor.obj Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasFunctorEnrichedHom V F₁ F₂
inst✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
⊢ (functorEnrichedHom V F₁ F₂ ⊗ functorEnrichedHom V F₂ F₃).map f ≫
      enrichedComp V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃) =
    enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
      (functorEnrichedHom V F₁ F₃).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasFunctorEnrichedHom V F₁ F₁
⊢ (λ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedId V F₁ ▷ functorEnrichedHom V F₁ F₂ ≫ functorEnrichedComp V F₁ F₁ F₂ =
    𝟙 (functorEnrichedHom V F₁ F₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁴ : Category.{v₂, u₂} H
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
F : C ⥤ Cat
K : J ⥤ Grothendieck F ⥤ H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : HasLimitsOfShape J H
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ (fiberwiseColimit (limit K)).map f ≫
      (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₂)).symm ≪≫
          preservesLimitIso colim (K ⋙ (whiskeringLeft (↑(F.obj c₂)) (Grothendieck F) H).obj (Grothendieck.ι F c₂)) ≪≫
            HasLimit.isoOfNatIso
                (K.associator ((whiskeringLeft (↑(F.obj c₂)) (Grothendieck F) H).obj (Grothendieck.ι F c₂)) colim ≪≫
                  K.isoWhiskerLeft (fiberwiseColimCompEvaluationIso c₂).symm ≪≫
                    (K.associator (fiberwiseColim F H) ((evaluation C H).obj c₂)).symm) ≪≫
              (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₂).symm).hom =
    (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₁)).symm ≪≫
          preservesLimitIso colim (K ⋙ (whiskeringLeft (↑(F.obj c₁)) (Grothendieck F) H).obj (Grothendieck.ι F c₁)) ≪≫
            HasLimit.isoOfNatIso
                (K.associator ((whiskeringLeft (↑(F.obj c₁)) (Grothendieck F) H).obj (Grothendieck.ι F c₁)) colim ≪≫
                  K.isoWhiskerLeft (fiberwiseColimCompEvaluationIso c₁).symm ≪≫
                    (K.associator (fiberwiseColim F H) ((evaluation C H).obj c₁)).symm) ≪≫
              (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₁).symm).hom ≫
      (limit (K ⋙ fiberwiseColim F H)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasFunctorEnrichedHom V F₂ F₂
⊢ (ρ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedHom V F₁ F₂ ◁ functorEnrichedId V F₂ ≫ functorEnrichedComp V F₁ F₂ F₂ =
    𝟙 (functorEnrichedHom V F₁ F₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
⊢ (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)).inv ≫
      functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄ ≫ functorEnrichedComp V F₁ F₃ F₄ =
    functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄ ≫ functorEnrichedComp V F₁ F₂ F₄

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
⊢ ∃ a, (Fiber.inducedFunctor ⋯).map a = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₁
⊢ (functorHomEquiv V) (𝟙 F₁) = functorEnrichedId V F₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b : ↑(F.obj { as := op S })
⊢ Function.Injective (Fiber.inducedFunctor ⋯).map

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
⊢ (fiberInclusion.obj Y).base = S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans
    (Trans.trans
      (Trans.trans (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm)
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
⊢ IsIso (limit.post K colim)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
⊢ PreservesLimitsOfShape J colim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
⊢ (Fiber.inducedFunctor ⋯).EssSurj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ IsFilteredOrEmpty (Grothendieck F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
⊢ Nonempty (Grothendieck F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
⊢ IsFiltered (Grothendieck F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (functorHomEquiv V) (f ≫ g) =
    (λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ₘ (functorHomEquiv V) g) ≫ functorEnrichedComp V F₁ F₂ F₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsLeftDerivedFunctor α W ↔ LF.IsRightKanExtension α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
LF' LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
α' : L ⋙ LF' ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
e : LF ≅ LF'
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ LF.IsLeftDerivedFunctor α W ↔ LF'.IsLeftDerivedFunctor α' W

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
LF' LF : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
τ : F' ⟶ F
⊢ L.whiskerLeft (LF'.leftDerivedNatTrans LF α' α W τ) ≫ α = α' ≫ τ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
LF' LF : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
τ : F' ⟶ F
X : C
⊢ (LF'.leftDerivedNatTrans LF α' α W τ).app (L.obj X) ≫ α.app X = α'.app X ≫ τ.app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
⊢ L.whiskerLeft (LF.leftDerivedNatTrans LF α α W (𝟙 F)) ≫ α = L.whiskerLeft (𝟙 LF) ≫ α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_5, u_2} H
LF'' LF' LF : D ⥤ H
F F' F'' : C ⥤ H
L : C ⥤ D
α'' : L ⋙ LF'' ⟶ F''
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : LF.IsLeftDerivedFunctor α W
inst✝ : LF'.IsLeftDerivedFunctor α' W
τ' : F'' ⟶ F'
τ : F' ⟶ F
⊢ L.whiskerLeft (LF''.leftDerivedNatTrans LF' α'' α' W τ' ≫ LF'.leftDerivedNatTrans LF α' α W τ) ≫ α =
    L.whiskerLeft (LF''.leftDerivedNatTrans LF α'' α W (τ' ≫ τ)) ≫ α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
G : D ⥤ H
β : L ⋙ G ⟶ F
this : LF.IsRightKanExtension α
⊢ L.whiskerLeft (LF.leftDerivedLift α W G β) ≫ α = β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
G : D ⥤ H
β : L ⋙ G ⟶ F
⊢ G.IsLeftDerivedFunctor β W ↔ IsIso (LF.leftDerivedLift α W G β)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ L.HasPointwiseRightKanExtensionAt F (L.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
X : C
inst✝ : F.HasPointwiseLeftDerivedFunctorAt W X
⊢ L.HasPointwiseRightKanExtensionAt F (L.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ F.HasLeftDerivedFunctor W ↔ L.HasRightKanExtension F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
X Y : C
w : X ⟶ Y
hw : W w
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ F.HasPointwiseLeftDerivedFunctorAt W Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ F.HasLeftDerivedFunctor W ↔ F'.HasLeftDerivedFunctor W

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : F.HasLeftDerivedFunctor W
⊢ L.HasRightKanExtension F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseLeftDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
⊢ L.HasPointwiseRightKanExtensionAt F Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
inst✝ : F.HasPointwiseLeftDerivedFunctor W
⊢ W.Q.HasRightKanExtension F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_2} D
inst✝² : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
⊢ F.HasLeftDerivedFunctor W

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (𝟙 (L.obj Y))) =
    s.π.app (StructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
C' : Type ?u.4
D : Type u_2
D' : Type ?u.8
H : Type u_3
H' : Type ?u.12
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, ?u.4} C'
inst✝⁵ : Category.{v_3, u_2} D
inst✝⁴ : Category.{v_4, ?u.8} D'
inst✝³ : Category.{v_5, u_3} H
inst✝² : Category.{v_6, ?u.12} H'
LF'' LF' LF : D ⥤ H
F F' F'' : C ⥤ H
e : F ≅ F'
L : C ⥤ D
α'' : L ⋙ LF'' ⟶ F''
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
α'₂ : L ⋙ LF' ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : F.HasLeftDerivedFunctor W
⊢ (F.totalLeftDerived L W).IsRightKanExtension (F.totalLeftDerivedCounit L W)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : 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} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
this : G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom = 𝟙 G'
Y₁ : D₁
⊢ G'.map (η.app Y₁) ≫ ε.app (G'.obj Y₁) = 𝟙 (G'.obj Y₁)

Tactic:
by

Goal state after: