awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
h : homRel.FactorsThroughLocalization W
W' : MorphismProperty.{v_1, u_1} (CategoryTheory.Quotient homRel)
hW : W = W'.inverseImage (Quotient.functor homRel)
⊢ (LocalizerMorphism.ofEq (W₁ := W) (W₂ := W') hW).IsLocalizedEquivalence (W₁ := W) (W₂ := W')

Tactic:
have : ((LocalizerMorphism.ofEq hW).functor ⋙ W'.Q).IsLocalization W :=
    Functor.IsLocalization.mk' _ _
      (h.strictUniversalPropertyFixedTarget' hW _)
      (h.strictUniversalPropertyFixedTarget' hW _)
  LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization _ W'.Q

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.MorphismProperty.Localization, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.IsLocalization.mk', CategoryTheory.LocalizerMorphism.ofEq, HomRel.FactorsThroughLocalization.strictUniversalPropertyFixedTarget', CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
⊢ ∃ (X₁ : C₁) (w : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) (hw : W₂ w), R = mk (W₁ := W₁) (W₂ := W₂) w hw

Tactic:
⟨_, R.w, R.hw, rfl⟩

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.w, CategoryTheory.LocalizerMorphism.RightResolution.hw, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
L : Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂
⊢ ∃ (X₁ : C₁) (w : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ⟶ X₂) (hw : W₂ w), L = mk (W₁ := W₁) (W₂ := W₂) w hw

Tactic:
⟨_, L.w, L.hw, rfl⟩

Premises used: CategoryTheory.LocalizerMorphism.LeftResolution.w, CategoryTheory.LocalizerMorphism.LeftResolution.hw, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
⊢ Hom.f (W₁ := W₁) (W₂ := W₂) (𝟙 R) = 𝟙 (R.X₁ (W₁ := W₁) (W₂ := W₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
R R' R'' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
φ : R ⟶ R'
ψ : R' ⟶ R''
⊢ (φ ≫ ψ).f (W₁ := W₁) (W₂ := W₂) = φ.f (W₁ := W₁) (W₂ := W₂) ≫ ψ.f (W₁ := W₁) (W₂ := W₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
R R' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
φ₁ φ₂ : R ⟶ R'
h : φ₁.f (W₁ := W₁) (W₂ := W₂) = φ₂.f (W₁ := W₁) (W₂ := W₂)
⊢ φ₁ = φ₂

Tactic:
Hom.ext h

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
L : Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂
⊢ Hom.f (W₁ := W₁) (W₂ := W₂) (𝟙 L) = 𝟙 (L.X₁ (W₁ := W₁) (W₂ := W₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
L L' L'' : Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂
φ : L ⟶ L'
ψ : L' ⟶ L''
⊢ (φ ≫ ψ).f (W₁ := W₁) (W₂ := W₂) = φ.f (W₁ := W₁) (W₂ := W₂) ≫ ψ.f (W₁ := W₁) (W₂ := W₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
L L' : Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂
φ₁ φ₂ : L ⟶ L'
h : φ₁.f (W₁ := W₁) (W₂ := W₂) = φ₂.f (W₁ := W₁) (W₂ := W₂)
⊢ φ₁ = φ₂

Tactic:
Hom.ext h

Premises used: CategoryTheory.LocalizerMorphism.LeftResolution.Hom.ext
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
⊢ Nonempty (Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂) ↔
    Nonempty (Φ.op (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.op) (W₂ := W₂.op) (Opposite.op X₂))

Tactic:
Equiv.nonempty_congr
    { toFun := fun L => L.op
      invFun := fun R => R.unop }

Premises used: Equiv.mk, CategoryTheory.LocalizerMorphism.RightResolution.unop, CategoryTheory.LocalizerMorphism.LeftResolution.op, Equiv.nonempty_congr
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
X₂ : C₂
⊢ Nonempty (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂) ↔
    Nonempty (Φ.op (W₁ := W₁) (W₂ := W₂).LeftResolution (W₁ := W₁.op) (W₂ := W₂.op) (Opposite.op X₂))

Tactic:
Equiv.nonempty_congr
    { toFun := fun R => R.op
      invFun := fun L => L.unop }

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.op, CategoryTheory.LocalizerMorphism.LeftResolution.unop, Equiv.mk, Equiv.nonempty_congr
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
⊢ Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
⟨fun _ X₂ => ⟨(Classical.arbitrary (Φ.LeftResolution X₂.unop)).op⟩,
    fun _ X₂ => ⟨(Classical.arbitrary (Φ.op.RightResolution (Opposite.op X₂))).unop⟩⟩

Premises used: CategoryTheory.LocalizerMorphism.LeftResolution, CategoryTheory.LocalizerMorphism.RightResolution, Nonempty.intro, CategoryTheory.LocalizerMorphism.RightResolution.unop, Opposite.op, Iff.intro, Classical.arbitrary, CategoryTheory.LocalizerMorphism.LeftResolution.op, Opposite.unop, CategoryTheory.LocalizerMorphism.op
-- Module: Mathlib.CategoryTheory.Localization.Resolution
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₂
⊢ Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
⟨fun _ X₂ => ⟨(Classical.arbitrary (Φ.RightResolution X₂.unop)).op⟩,
    fun _ X₂ => ⟨(Classical.arbitrary (Φ.op.LeftResolution (Opposite.op X₂))).unop⟩⟩

Premises used: CategoryTheory.LocalizerMorphism.LeftResolution, CategoryTheory.LocalizerMorphism.RightResolution, CategoryTheory.LocalizerMorphism.RightResolution.op, CategoryTheory.LocalizerMorphism.LeftResolution.unop, Nonempty.intro, Opposite.op, Iff.intro, Classical.arbitrary, Opposite.unop, CategoryTheory.LocalizerMorphism.op
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
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_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
inst_4 : Category.{v_5, u_5} H
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₂
Φ : LocalizerMorphism W₁ W₂
inst_5 rwa rwa₁ rwa₂ rwa₃ : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
rwa [← hasRightResolutions_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_op
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
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_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
inst_4 : Category.{v_5, u_5} H
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₂
Φ : LocalizerMorphism W₁ W₂
inst_5 rwa rwa₁ rwa₂ rwa₃ : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
rwa [← hasLeftResolutions_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_op
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
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_3 : L₂.IsLocalization W₂
inst_4 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
X₂ : D₂
⊢ L₂.EssSurj

Tactic:
have := Localization.essSurj L₂ W₂
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
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_3 : L₂.IsLocalization W₂
inst_4 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
X₂ : D₂
this : L₂.EssSurj
have :
  ∀ (R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) (L₂.objPreimage X₂)),
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂

Tactic:
have R : Φ.RightResolution (L₂.objPreimage X₂) := Classical.arbitrary _
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
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_3 : L₂.IsLocalization W₂
inst_4 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
X₂ : D₂
this : L₂.EssSurj
R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) (L₂.objPreimage X₂)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂

Tactic:
⟨R.X₁, ⟨(Localization.isoOfHom L₂ W₂ _ R.hw).symm ≪≫ L₂.objObjPreimageIso X₂⟩⟩

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.X₁, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.trans, CategoryTheory.LocalizerMorphism.RightResolution.hw, Exists.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
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_3 : L₂.IsLocalization W₂
inst_4 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
X₂ : D₂
this : L₂.EssSurj
R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) (L₂.objPreimage X₂)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂

Tactic:
exact ⟨R.X₁, ⟨(Localization.isoOfHom L₂ W₂ _ R.hw).symm ≪≫ L₂.objObjPreimageIso X₂⟩⟩
-- 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 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
mp :
  IsIso α →
    ∀ (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₁)))
mpr :
  (∀ (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₁)))) →
    IsIso α
⊢ IsIso α ↔
    ∀ (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₁)))

Tactic:
constructor
-- 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 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
F G : Functor.{v_4, v_5, u_4, u_5} D₂ H
α : F ⟶ G
h : IsIso α
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₁)))

Tactic:
infer_instance
-- 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 : Φ.HasRightResolutions (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_hasRightResolutions 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 : Φ.HasRightResolutions (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 : Φ.HasRightResolutions (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 : Φ.HasRightResolutions (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_hasRightResolutions 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 : Φ.HasRightResolutions (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 : Φ.HasRightResolutions (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_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
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_3 : L₂.IsLocalization W₂
inst_4 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
X₂ : D₂
⊢ L₂.EssSurj

Tactic:
have := Localization.essSurj L₂ W₂
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
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_3 : L₂.IsLocalization W₂
inst_4 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
X₂ : D₂
this : L₂.EssSurj
have :
  ∀ (L : Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) (L₂.objPreimage X₂)), (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂

Tactic:
have L : Φ.LeftResolution (L₂.objPreimage X₂) := Classical.arbitrary _
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
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_3 : L₂.IsLocalization W₂
inst_4 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
X₂ : D₂
this : L₂.EssSurj
L : Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) (L₂.objPreimage X₂)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂

Tactic:
⟨L.X₁, ⟨Localization.isoOfHom L₂ W₂ _ L.hw ≪≫ L₂.objObjPreimageIso X₂⟩⟩

Premises used: CategoryTheory.LocalizerMorphism.LeftResolution.X₁, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.LocalizerMorphism.LeftResolution.hw, CategoryTheory.Iso.trans, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.Resolution
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₂
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_3 : L₂.IsLocalization W₂
inst_4 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
X₂ : D₂
this : L₂.EssSurj
L : Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) (L₂.objPreimage X₂)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂

Tactic:
exact ⟨L.X₁, ⟨Localization.isoOfHom L₂ W₂ _ L.hw ≪≫ L₂.objObjPreimageIso X₂⟩⟩
-- 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
mp :
  IsIso α →
    ∀ (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₁)))
mpr :
  (∀ (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₁)))) →
    IsIso α
⊢ IsIso α ↔
    ∀ (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₁)))

Tactic:
constructor
-- 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 : IsIso α
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₁)))

Tactic:
infer_instance