awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₁'.RespectsIso
inst_5 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
e : T.op (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.op) (W₂ := W₂.op) ⋙
    R.op (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂.op) (W₂ := W₂'.op) ≅
  L.op (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁.op) (W₂ := W₁'.op) ⋙
    B.op (W₁ := W₁') (W₂ := W₂').functor (W₁ := W₁'.op) (W₂ := W₂'.op) :=
  NatIso.op iso.symm
⊢ T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ B.IsRightDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

Tactic:
simp only [isRightDerivabilityStructure_iff_op,
    isLeftDerivabilityStructure_iff_of_equivalences e]

Premises used: CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_op, CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_of_equivalences
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₁'.RespectsIso
inst_5 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
inst_10 : T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
rwa rwa₁ rwa₂ rwa₃ : T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ B.IsRightDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

Tactic:
rwa [← isRightDerivabilityStructure_iff_of_equivalences iso]

Premises used: CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_of_equivalences
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
rw rw₁ :
  Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
      (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
        whiskerRight
            (Iso.hom
              (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
            F₂ ≫
          (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom =
    Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
      (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
        whiskerRight
            (Iso.hom
              (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
            F₂ ≫
          (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom
⊢ α₁ ≫
      L₁.whiskerLeft
        (F₁.rightDerivedDesc α₁ W₁ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂)
          (Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
            (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
              whiskerRight
                  (Iso.hom
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
                  F₂ ≫
                (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom)) =
    Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
      (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
        whiskerRight
            (Iso.hom
              (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
            F₂ ≫
          (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom

Tactic:
rw [Functor.rightDerived_fac]

Premises used: CategoryTheory.Functor.rightDerived_fac
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
X : C₁
⊢ Eq (α :=
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).obj X ⟶ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).obj (L₁.obj X))
    (α₁.app X ≫ NatTrans.app (Φ.rightDerivedFunctorComparison (W₁ := W₁) (W₂ := W₂) L₁ L₂ F F₁ α₁ F₂ α₂) (L₁.obj X))
    (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      F₂.map
        (NatTrans.app
          (Iso.hom
            (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
          X))

Tactic:
simpa using congr_app (Φ.rightDerivedFunctorComparison_fac L₁ L₂ F F₁ α₁ F₂ α₂) X

Premises used: CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
X : C₁
e : W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≅
  (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj (W₁.Q.obj X) :=
  Iso.app
    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)) X
rw :
  (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔
    W₂.Q.HasPointwiseLeftKanExtensionAt F (W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
rw₁ :
  W₁.Q.HasPointwiseLeftKanExtensionAt (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) (W₁.Q.obj X) ↔
    W₂.Q.HasPointwiseLeftKanExtensionAt F (W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
rw₂ :
  W₂.Q.HasPointwiseLeftKanExtensionAt F ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj (W₁.Q.obj X)) ↔
    W₂.Q.HasPointwiseLeftKanExtensionAt F (W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
rw₃ rw₄ :
  W₂.Q.HasPointwiseLeftKanExtensionAt F ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj (W₁.Q.obj X)) ↔
    W₂.Q.HasPointwiseLeftKanExtensionAt F ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj (W₁.Q.obj X))
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔
    F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)

Tactic:
rw [F.hasPointwiseRightDerivedFunctorAt_iff W₂.Q W₂ (Φ.functor.obj X),
    (Φ.functor ⋙ F).hasPointwiseRightDerivedFunctorAt_iff W₁.Q W₁ X,
    TwoSquare.hasPointwiseLeftKanExtensionAt_iff ((Φ.catCommSq W₁.Q W₂.Q).iso).hom,
    Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso W₂.Q F e]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff, CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso, CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
mp : F.HasPointwiseRightDerivedFunctor W₂ → (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
mpr : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁ → F.HasPointwiseRightDerivedFunctor W₂
⊢ F.HasPointwiseRightDerivedFunctor W₂ ↔ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
hF : F.HasPointwiseRightDerivedFunctor W₂
X₁ : C₁
mp : F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X₁

Tactic:
rw [hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure]

Premises used: CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
hF : F.HasPointwiseRightDerivedFunctor W₂
X₁ : C₁
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)

Tactic:
apply hF
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
hF : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
X₂ : C₂
mpr : ∀ (R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂), F.HasPointwiseRightDerivedFunctorAt W₂ X₂
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ X₂

Tactic:
have R : Φ.RightResolution X₂ := Classical.arbitrary _
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
hF : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
X₂ : C₂
R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ X₂

Tactic:
simpa only [hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure,
      ← F.hasPointwiseRightDerivedFunctorAt_iff_of_mem W₂ R.w R.hw] using hF R.X₁

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.w, CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure, CategoryTheory.LocalizerMorphism.RightResolution.X₁, CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff_of_mem, CategoryTheory.LocalizerMorphism.RightResolution.hw
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
rw : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
⊢ F.HasPointwiseRightDerivedFunctor W₂

Tactic:
rw [Φ.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure]

Premises used: CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
⊢ F.HasPointwiseRightDerivedFunctor W₂

Tactic:
have : F.HasPointwiseRightDerivedFunctor W₂ := by
    rw [Φ.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure]
    infer_instance
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
rw :
  (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).IsLeftKanExtension
    (Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
      (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
        whiskerRight
            (Iso.hom
              (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
            F₂ ≫
          (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom)
⊢ IsIso
    (F₁.rightDerivedDesc α₁ W₁ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂)
      (Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
        (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
          whiskerRight
              (Iso.hom
                (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂
                  (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
              F₂ ≫
            (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom))

Tactic:
rw [← isRightDerivedFunctor_iff_isIso_rightDerivedDesc,
    isRightDerivedFunctor_iff_isLeftKanExtension]

Premises used: CategoryTheory.Functor.isRightDerivedFunctor_iff_isLeftKanExtension, CategoryTheory.Functor.isRightDerivedFunctor_iff_isIso_rightDerivedDesc
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).IsLeftKanExtension
    (Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
      (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
        whiskerRight
            (Iso.hom
              (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
            F₂ ≫
          (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom)

Tactic:
((F₂.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor α₂ W₂).compTwoSquare
    ((Φ.catCommSq L₁ L₂).iso).hom).isLeftKanExtension

Premises used: CategoryTheory.Functor.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.Functor.comp, CategoryTheory.CatCommSq.iso, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.compTwoSquare, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).IsLeftKanExtension
    (Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
      (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
        whiskerRight
            (Iso.hom
              (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
            F₂ ≫
          (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom)

Tactic:
exact ((F₂.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor α₂ W₂).compTwoSquare
    ((Φ.catCommSq L₁ L₂).iso).hom).isLeftKanExtension

Premises used: CategoryTheory.Functor.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.CatCommSq.iso, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.compTwoSquare, CategoryTheory.Iso.hom