awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
rw : ∀ (X : D₂), IsIso (φ.app X)
⊢ IsIso φ

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
rw :
  IsIso (X :=
    (F.totalRightDerived L₂ W₂).obj
      ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂)))
    (φ.app ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂)))
⊢ IsIso (φ.app Y₂)

Tactic:
rw [NatTrans.isIso_app_iff_of_iso φ ((Φ.functor ⋙ L₂).objObjPreimageIso Y₂).symm]

Premises used: CategoryTheory.NatTrans.isIso_app_iff_of_iso, CategoryTheory.Functor.comp, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
dsimp :
  IsIso (X :=
    (F.totalRightDerived L₂ W₂).obj
      (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂))))
    (φ.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂))))
⊢ IsIso (X :=
    (F.totalRightDerived L₂ W₂).obj
      ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂)))
    (φ.app ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
⊢ ∀ (X₁ : C₁),
    IsIso (X := (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (φ.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))

Tactic:
simp only [← hφ, NatTrans.comp_app, Functor.whiskerLeft_app, isIso_comp_left_iff] at hα

Premises used: CategoryTheory.isIso_comp_left_iff, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
hα :
  ∀ (X₁ : C₁),
    IsIso (X := (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (φ.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
⊢ IsIso (X :=
    (F.totalRightDerived L₂ W₂).obj
      (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂))))
    (φ.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂))))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
⊢ IsIso φ

Tactic:
have : IsIso φ := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro Y₂
    rw [NatTrans.isIso_app_iff_of_iso φ ((Φ.functor ⋙ L₂).objObjPreimageIso Y₂).symm]
    dsimp
    simp only [← hφ, NatTrans.comp_app, Functor.whiskerLeft_app, isIso_comp_left_iff] at hα
    infer_instance
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_3 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
this : IsIso φ
rw : (F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂
⊢ RF.IsRightDerivedFunctor α W₂

Tactic:
rw [← Functor.isRightDerivedFunctor_iff_of_iso (F.totalRightDerivedUnit L₂ W₂) α W₂
    (asIso φ) (by cat_disch)]

Premises used: CategoryTheory.Functor.isRightDerivedFunctor_iff_of_iso, CategoryTheory.asIso, CategoryTheory.Functor.totalRightDerivedUnit
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_3 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
this : IsIso φ
⊢ (F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
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₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
⊢ RF.IsRightDerivedFunctor α W₂ ↔
    ∀ (X₁ : C₁),
      IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))

Tactic:
⟨fun _ _ ↦ h.isIso α _, h.isRightDerivedFunctor_of_isIso α⟩

Premises used: CategoryTheory.LocalizerMorphism.Derives.isIso, CategoryTheory.LocalizerMorphism.Derives.isRightDerivedFunctor_of_isIso, Iff.intro
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
⊢ Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)

Tactic:
fun f ↦
    ⟨{ X₁ := Arrow.mk (ρ.map f.hom)
       w := Arrow.homMk (i.app _) (i.app _) (i.naturality f.hom).symm
       hw := ⟨hi _, hi _⟩ }⟩

Premises used: CategoryTheory.Comma.right, CategoryTheory.Comma.left, CategoryTheory.LocalizerMorphism.RightResolution.mk, CategoryTheory.Arrow.hom, Nonempty.intro, CategoryTheory.NatTrans.naturality, And.intro, Eq.symm, CategoryTheory.NatTrans.app, CategoryTheory.Arrow.homMk
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
rw : W₂ ≤ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage ρ
⊢ W₂ ≤ W₁.inverseImage ρ

Tactic:
rw [hW₁]
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
⊢ Functor.map (𝟭 C₂) f ≫ i.app Y = i.app X ≫ (ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)).map f

Tactic:
have := i.naturality f
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f)
simp : W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f))
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage ρ f

Tactic:
simp only [MorphismProperty.inverseImage_iff]

Premises used: CategoryTheory.MorphismProperty.inverseImage_iff
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f)
rw : W₂ (f ≫ i.app Y)
⊢ W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f))

Tactic:
rw [← W₂.precomp_iff _ _ (hi X), ← this]

Premises used: CategoryTheory.MorphismProperty.precomp_iff
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f)
⊢ W₂ (f ≫ i.app Y)

Tactic:
W₂.comp_mem _ _ hf (hi Y)

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f)
⊢ W₂ (f ≫ i.app Y)

Tactic:
exact W₂.comp_mem _ _ hf (hi Y)

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).Full
inst_3 : Φ.functor (W₁ := W₁) (W₂ := W₂).Faithful
X₁ : C₁
⊢ Φ.functor (W₁ := W₁) (W₂ := W₂).map ((ι (W₁ := W₁) (W₂ := W₂) i).app X₁) =
    i.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)

Tactic:
NatTrans.congr_app (((whiskeringRight C₁ C₁ C₂).obj Φ.functor).map_preimage
    (X := 𝟭 C₁) (Y := Φ.functor ⋙ ρ) (whiskerLeft Φ.functor i)) X₁

Premises used: CategoryTheory.Functor.whiskerLeft, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.whiskeringRight, CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.obj, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).Full
inst_3 : Φ.functor (W₁ := W₁) (W₂ := W₂).Faithful
X₁ : C₁
⊢ W₁ ((ι (W₁ := W₁) (W₂ := W₂) i).app X₁)

Tactic:
simpa [hW₁] using hi (Φ.functor.obj X₁)

Premises used: CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).Full
inst_3 : Φ.functor (W₁ := W₁) (W₂ := W₂).Faithful
inst_4 : W₂.HasTwoOutOfThreeProperty
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
Φ.isLocalizedEquivalence_of_unit_of_unit (localizerMorphismInv hi hW₁) (ι i) i
    (W₁_ι_app hi hW₁) hi

Premises used: CategoryTheory.LocalizerMorphism.functorialRightResolutions.W₁_ι_app, CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_unit_of_unit, CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι, CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInv
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).Full
inst_3 : Φ.functor (W₁ := W₁) (W₂ := W₂).Faithful
inst_4 : W₂.HasTwoOutOfThreeProperty
inst_5 : W₂.IsMultiplicative
X₂ : C₂
rw : (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).IsMultiplicative
⊢ W₁.IsMultiplicative

Tactic:
rw [hW₁]