awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (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.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ Nonempty (T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)

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

Premises used: CategoryTheory.LocalizerMorphism.LeftResolution.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.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (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₂' (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂'))
⊢ W₂
    (R.functor (W₁ := W₂) (W₂ := W₂').preimage
      (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂')))

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.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (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₂' (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂'))

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

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.LeftResolution.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.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (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 (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂')) ≅
    Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂'))
⊢ W₂' (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂'))

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

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.LeftResolution.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.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (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 (iso.hom.app X₁ ≫ B.functor (W₁ := W₁') (W₂ := W₂').map e.hom ≫ ρ.w (W₁ := W₁') (W₂ := W₂')) ≅
    Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂'))

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

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.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (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.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)

Tactic:
exact ⟨{
    X₁ := X₁
    w := R.functor.preimage (iso.hom.app X₁ ≫ B.functor.map e.hom ≫ ρ.w)
    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.app _ ≪≫ B.functor.mapIso e) (Iso.refl _) }⟩
-- 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 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_8 : 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₂')
⊢ T.HasRightResolutions (W₁ := W₁) (W₂ := W₂) ↔ B.HasRightResolutions (W₁ := W₁') (W₂ := W₂')

Tactic:
⟨fun _ ↦ hasRightResolutions_of_iso_of_essSurj iso,
    fun _ ↦ hasRightResolutions_of_iso_of_essSurj_of_full iso⟩

Premises used: CategoryTheory.LocalizerMorphism.hasRightResolutions_of_iso_of_essSurj_of_full, Iff.intro, CategoryTheory.LocalizerMorphism.hasRightResolutions_of_iso_of_essSurj
-- 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 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_8 : 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₂')
⊢ T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂) ↔ B.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')

Tactic:
⟨fun _ ↦ hasLeftResolutions_of_iso_of_essSurj iso,
    fun _ ↦ hasLeftResolutions_of_iso_of_essSurj_of_full iso⟩

Premises used: CategoryTheory.LocalizerMorphism.hasLeftResolutions_of_iso_of_essSurj_of_full, Iff.intro, CategoryTheory.LocalizerMorphism.hasLeftResolutions_of_iso_of_essSurj
-- 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 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : 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_7 : T.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
⊢ B.arrow (W₁ := W₁') (W₂ := W₂').HasRightResolutions (W₁ := W₁'.arrow) (W₂ := W₂'.arrow)

Tactic:
hasRightResolutions_of_iso_of_essSurj
    (CatCommSq.iso T.arrow.functor L.arrow.functor R.arrow.functor B.arrow.functor)

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.arrow, CategoryTheory.LocalizerMorphism.hasRightResolutions_of_iso_of_essSurj
-- 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 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : 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_7 : T.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
⊢ B.arrow (W₁ := W₁') (W₂ := W₂').HasRightResolutions (W₁ := W₁'.arrow) (W₂ := W₂'.arrow)

Tactic:
exact hasRightResolutions_of_iso_of_essSurj
    (CatCommSq.iso T.arrow.functor L.arrow.functor R.arrow.functor B.arrow.functor)

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.arrow, CategoryTheory.LocalizerMorphism.hasRightResolutions_of_iso_of_essSurj
-- 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 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : 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_7 : T.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
⊢ B.arrow (W₁ := W₁') (W₂ := W₂').HasLeftResolutions (W₁ := W₁'.arrow) (W₂ := W₂'.arrow)

Tactic:
hasLeftResolutions_of_iso_of_essSurj
    (CatCommSq.iso T.arrow.functor L.arrow.functor R.arrow.functor B.arrow.functor)

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.arrow, CategoryTheory.LocalizerMorphism.hasLeftResolutions_of_iso_of_essSurj
-- 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 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_6 : 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_7 : T.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
⊢ B.arrow (W₁ := W₁') (W₂ := W₂').HasLeftResolutions (W₁ := W₁'.arrow) (W₂ := W₂'.arrow)

Tactic:
exact hasLeftResolutions_of_iso_of_essSurj
    (CatCommSq.iso T.arrow.functor L.arrow.functor R.arrow.functor B.arrow.functor)

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.arrow, CategoryTheory.LocalizerMorphism.hasLeftResolutions_of_iso_of_essSurj
-- 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₂').IsEquivalence
inst_5 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_6 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
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₂')
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
⊢ T.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow) ↔
    B.arrow (W₁ := W₁') (W₂ := W₂').HasRightResolutions (W₁ := W₁'.arrow) (W₂ := W₂'.arrow)

Tactic:
hasRightResolutions_iff_iso_of_essSurj_of_full
    (CatCommSq.iso T.arrow.functor L.arrow.functor R.arrow.functor B.arrow.functor)

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.arrow, CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_iso_of_essSurj_of_full
-- 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₂').IsEquivalence
inst_5 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_6 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
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₂')
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
⊢ T.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow) ↔
    B.arrow (W₁ := W₁') (W₂ := W₂').HasRightResolutions (W₁ := W₁'.arrow) (W₂ := W₂'.arrow)

Tactic:
exact hasRightResolutions_iff_iso_of_essSurj_of_full
    (CatCommSq.iso T.arrow.functor L.arrow.functor R.arrow.functor B.arrow.functor)

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.arrow, CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_iso_of_essSurj_of_full
-- 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₂').IsEquivalence
inst_5 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_6 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
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₂')
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
⊢ T.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow) ↔
    B.arrow (W₁ := W₁') (W₂ := W₂').HasLeftResolutions (W₁ := W₁'.arrow) (W₂ := W₂'.arrow)

Tactic:
hasLeftResolutions_iff_iso_of_essSurj_of_full
    (CatCommSq.iso T.arrow.functor L.arrow.functor R.arrow.functor B.arrow.functor)

Premises used: CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_iso_of_essSurj_of_full, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.arrow
-- 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₂').IsEquivalence
inst_5 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_6 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
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₂')
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
⊢ T.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow) ↔
    B.arrow (W₁ := W₁') (W₂ := W₂').HasLeftResolutions (W₁ := W₁'.arrow) (W₂ := W₂'.arrow)

Tactic:
exact hasLeftResolutions_iff_iso_of_essSurj_of_full
    (CatCommSq.iso T.arrow.functor L.arrow.functor R.arrow.functor B.arrow.functor)

Premises used: CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_iso_of_essSurj_of_full, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.arrow
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
mp : HasSmallLocalizedHom W X Y → Small.{w, v₂} (L.obj X ⟶ L.obj Y)
mpr : Small.{w, v₂} (L.obj X ⟶ L.obj Y) → HasSmallLocalizedHom W X Y
⊢ HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
constructor