awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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₂')
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
e : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂) ≅
  L.inv (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁') (W₂ := W₁) ⋙ T.functor (W₁ := W₁) (W₂ := W₂) :=
  (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.counitIso.symm
        (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor
          (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
            (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor.associator (B.functor (W₁ := W₁') (W₂ := W₂'))
                (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))).symm ≪≫
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
              (isoWhiskerRight iso.symm (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
            L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂'))
                  (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
              L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                  (T.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft
                    R.functor (W₁ := W₂) (W₂ := W₂').asEquivalence.unitIso.symm) ≪≫
                (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator (T.functor (W₁ := W₁) (W₂ := W₂))
                      (𝟭 C₂)).symm ≪≫
                  (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse ⋙ T.functor (W₁ := W₁) (W₂ := W₂)).rightUnitor
⊢ W₁.RespectsIso
have rw : (W₁'.inverseImage (L.functor (W₁ := W₁) (W₂ := W₁'))).RespectsIso
Tactic: rw [← L.inverseImage_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (hypothesis)
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₂')
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
e : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂) ≅
  L.inv (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁') (W₂ := W₁) ⋙ T.functor (W₁ := W₁) (W₂ := W₂) :=
  (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.counitIso.symm
        (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor
          (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
            (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor.associator (B.functor (W₁ := W₁') (W₂ := W₂'))
                (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))).symm ≪≫
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
              (isoWhiskerRight iso.symm (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
            L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂'))
                  (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
              L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                  (T.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft
                    R.functor (W₁ := W₂) (W₂ := W₂').asEquivalence.unitIso.symm) ≪≫
                (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator (T.functor (W₁ := W₁) (W₂ := W₂))
                      (𝟭 C₂)).symm ≪≫
                  (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse ⋙ T.functor (W₁ := W₁) (W₂ := W₂)).rightUnitor
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this : W₁.RespectsIso
Tactic: have : W₁.RespectsIso := by rw [← L.inverseImage_eq]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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₂')
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
e : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂) ≅
  L.inv (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁') (W₂ := W₁) ⋙ T.functor (W₁ := W₁) (W₂ := W₂) :=
  (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.counitIso.symm
        (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor
          (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
            (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor.associator (B.functor (W₁ := W₁') (W₂ := W₂'))
                (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))).symm ≪≫
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
              (isoWhiskerRight iso.symm (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
            L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂'))
                  (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
              L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                  (T.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft
                    R.functor (W₁ := W₂) (W₂ := W₂').asEquivalence.unitIso.symm) ≪≫
                (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator (T.functor (W₁ := W₁) (W₂ := W₂))
                      (𝟭 C₂)).symm ≪≫
                  (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse ⋙ T.functor (W₁ := W₁) (W₂ := W₂)).rightUnitor
this : W₁.RespectsIso
⊢ W₂.RespectsIso
have rw : (W₂'.inverseImage (R.functor (W₁ := W₂) (W₂ := W₂'))).RespectsIso
Tactic: rw [← R.inverseImage_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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₁
⊢ α₁ ≫
      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
have 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
Tactic: rw [Functor.rightDerived_fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔
    F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)
have rw : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔
  W₂.Q.HasPointwiseLeftKanExtensionAt F (W₂.Q.obj (Φ.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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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))
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔
    F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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))
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔
    F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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))
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔
    F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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₂)
⊢ F.HasPointwiseRightDerivedFunctor W₂ ↔ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
have mp : F.HasPointwiseRightDerivedFunctor W₂ → (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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₁
⊢ F.HasPointwiseRightDerivedFunctor W₂ ↔ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
have mpr : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁ → F.HasPointwiseRightDerivedFunctor W₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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₁
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X₁
have mp : F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)
Tactic: rw [hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (goal)
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₂
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ X₂
have mpr : ∀ (R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂), F.HasPointwiseRightDerivedFunctorAt W₂ X₂
Tactic: have R : Φ.RightResolution X₂ := Classical.arbitrary _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (hypothesis)
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₂
⊢ IsIso (Y := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂)
    (Φ.rightDerivedFunctorComparison (W₁ := W₁) (W₂ := W₂) L₁ L₂ F F₁ α₁ F₂ α₂)
have this : F.HasPointwiseRightDerivedFunctor W₂
Tactic: have : F.HasPointwiseRightDerivedFunctor W₂ := by
    rw [Φ.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure]
    infer_instance