awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
inst_3 : Category.{v_5, u_5} H
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_4 : L₂.IsLocalization W₂
inst_5 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
      (α.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
X₂ : D₂
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj

Tactic:
have := Φ.essSurj_of_hasLeftResolutions L₂
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
inst_3 : Category.{v_5, u_5} H
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_4 : L₂.IsLocalization W₂
inst_5 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
      (α.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
X₂ : D₂
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
rw :
  IsIso (X :=
    F.obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage X₂)))
    (α.app ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage X₂)))
⊢ IsIso (α.app X₂)

Tactic:
rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]

Premises used: CategoryTheory.NatTrans.isIso_app_iff_of_iso, CategoryTheory.Functor.comp, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.objObjPreimageIso
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
inst_3 : Category.{v_5, u_5} H
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_4 : L₂.IsLocalization W₂
inst_5 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
      (α.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
X₂ : D₂
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
⊢ IsIso (X :=
    F.obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage X₂)))
    (α.app ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage X₂)))

Tactic:
apply hα
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
inst_3 : Category.{v_5, u_5} H
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_4 : L₂.IsLocalization W₂
inst_5 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
      (α.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
⊢ ∀ (X₂ : D₂), IsIso (α.app X₂)

Tactic:
have : ∀ (X₂ : D₂), IsIso (α.app X₂) := fun X₂ => by
      have := Φ.essSurj_of_hasLeftResolutions L₂
      rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]
      apply hα
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
inst_3 : Category.{v_5, u_5} H
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_4 : L₂.IsLocalization W₂
inst_5 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
      (α.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
this : ∀ (X₂ : D₂), IsIso (α.app X₂)
⊢ IsIso α

Tactic:
NatIso.isIso_of_isIso_app α

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
inst_3 : Category.{v_5, u_5} H
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
inst_4 : L₂.IsLocalization W₂
inst_5 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
      (α.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
this : ∀ (X₂ : D₂), IsIso (α.app X₂)
⊢ IsIso α

Tactic:
exact NatIso.isIso_of_isIso_app α

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_5 : W₂'.RespectsIso
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₂')
inst_6 : T.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
Y₂ : D₂
obtain :
  ∀ (X₂ : C₂) (e : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂),
    Nonempty (B.RightResolution (W₁ := W₁') (W₂ := W₂') Y₂)
⊢ Nonempty (B.RightResolution (W₁ := W₁') (W₂ := W₂') Y₂)

Tactic:
obtain ⟨X₂, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := R.functor) Y₂

Premises used: CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.EssSurj.mem_essImage
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_5 : W₂'.RespectsIso
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₂')
inst_6 : T.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
Y₂ : D₂
X₂ : C₂
e : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂
ρ : T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂ := Classical.arbitrary (T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ Nonempty (B.RightResolution (W₁ := W₁') (W₂ := W₂') Y₂)

Tactic:
⟨{
    X₁ := L.functor.obj ρ.X₁
    w := e.inv ≫ R.functor.map ρ.w ≫ iso.hom.app _
    hw := (W₂'.arrow_mk_iso_iff (Arrow.isoMk e (iso.app _))).1 (R.map _ ρ.hw) }⟩

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.w, CategoryTheory.LocalizerMorphism.RightResolution.X₁, CategoryTheory.LocalizerMorphism.RightResolution.mk, CategoryTheory.LocalizerMorphism.functor, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.map, CategoryTheory.LocalizerMorphism.RightResolution.hw, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.Iso.app, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_5 : W₂'.RespectsIso
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₂')
inst_6 : T.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
Y₂ : D₂
X₂ : C₂
e : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂
ρ : T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂ := Classical.arbitrary (T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ Nonempty (B.RightResolution (W₁ := W₁') (W₂ := W₂') Y₂)

Tactic:
exact ⟨{
    X₁ := L.functor.obj ρ.X₁
    w := e.inv ≫ R.functor.map ρ.w ≫ iso.hom.app _
    hw := (W₂'.arrow_mk_iso_iff (Arrow.isoMk e (iso.app _))).1 (R.map _ ρ.hw) }⟩
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_5 : W₂'.RespectsIso
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₂')
inst_6 : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
Y₂ : D₂
obtain :
  ∀ (X₂ : C₂) (e : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂), Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)
⊢ Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)

Tactic:
obtain ⟨X₂, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := R.functor) Y₂

Premises used: CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.EssSurj.mem_essImage
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_5 : W₂'.RespectsIso
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₂')
inst_6 : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
Y₂ : D₂
X₂ : C₂
e : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂
ρ : T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂ := Classical.arbitrary (T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)

Tactic:
⟨{
    X₁ := L.functor.obj ρ.X₁
    w := iso.inv.app _ ≫ R.functor.map ρ.w ≫ e.hom
    hw := (W₂'.arrow_mk_iso_iff (Arrow.isoMk (iso.app _) e)).1 (R.map _ ρ.hw) }⟩

Premises used: CategoryTheory.LocalizerMorphism.LeftResolution.X₁, CategoryTheory.LocalizerMorphism.LeftResolution.w, CategoryTheory.LocalizerMorphism.functor, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.LeftResolution.hw, CategoryTheory.LocalizerMorphism.map, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.Iso.app, CategoryTheory.LocalizerMorphism.LeftResolution.mk, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_5 : W₂'.RespectsIso
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₂')
inst_6 : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
Y₂ : D₂
X₂ : C₂
e : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂
ρ : T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂ := Classical.arbitrary (T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)

Tactic:
exact ⟨{
    X₁ := L.functor.obj ρ.X₁
    w := iso.inv.app _ ≫ R.functor.map ρ.w ≫ e.hom
    hw := (W₂'.arrow_mk_iso_iff (Arrow.isoMk (iso.app _) e)).1 (R.map _ ρ.hw) }⟩
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
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₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
obtain :
  ∀ (X₁ : C₁) (e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')),
    Nonempty (T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ Nonempty (T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)

Tactic:
obtain ⟨X₁, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage L.functor ρ.X₁

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.X₁, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.EssSurj.mem_essImage
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
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₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
simp : W₂' (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁)
⊢ W₂
    (R.functor (W₁ := W₂) (W₂ := W₂').preimage
      (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁))

Tactic:
simp only [← R.inverseImage_eq, MorphismProperty.inverseImage_iff, Functor.map_preimage]

Premises used: CategoryTheory.MorphismProperty.inverseImage_iff, CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
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₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
⊢ W₂' (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁)

Tactic:
(W₂'.arrow_mk_iso_iff ?_).2 ρ.hw

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.RightResolution.hw
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
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₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
refine :
  Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁) ≅
    Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂'))
⊢ W₂' (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁)

Tactic:
refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.RightResolution.hw
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
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₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
⊢ Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂') ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.inv ≫ iso.inv.app X₁) ≅
    Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂'))

Tactic:
exact Arrow.isoMk (Iso.refl _) (iso.app _ ≪≫ B.functor.mapIso e)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.trans, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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_2, u_2} C₂
W₁' : MorphismProperty.{v_3, u_3} D₁
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 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_5 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : W₂'.RespectsIso
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₂')
inst_8 : B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.RightResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
X₁ : C₁
e : L.functor (W₁ := W₁) (W₂ := W₁').obj X₁ ≅ ρ.X₁ (W₁ := W₁') (W₂ := W₂')
⊢ Nonempty (T.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)

Tactic:
exact ⟨{
    X₁ := X₁
    w := R.functor.preimage (ρ.w ≫ B.functor.map e.inv ≫ iso.inv.app X₁)
    hw := by
      simp only [← R.inverseImage_eq, MorphismProperty.inverseImage_iff, Functor.map_preimage]
      refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
      exact Arrow.isoMk (Iso.refl _) (iso.app _ ≪≫ B.functor.mapIso e)}⟩