awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).IsMultiplicative

Tactic:
infer_instance
-- 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₂
⊢ W₁.IsMultiplicative

Tactic:
have : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
-- 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₂
this : W₁.IsMultiplicative
⊢ Nonempty (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)

Tactic:
have : Nonempty (Φ.RightResolution X₂) := ⟨{ hw := hi X₂, .. }⟩
-- 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₂
this_1 : W₁.IsMultiplicative
this : Nonempty (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ IsPreconnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)

Tactic:
have : IsPreconnected (Φ.RightResolution X₂) :=
    zigzag_isPreconnected (fun R₀ R₄ ↦
      calc
        Zigzag R₀ { hw := W₂.comp_mem _ _ R₀.hw (hi _), .. } :=
          Zigzag.of_hom { f := (ι i).app R₀.X₁ }
        Zigzag (J := Φ.RightResolution X₂) _ { hw := hi X₂, .. } :=
          Zigzag.of_inv
            { f := ρ.map R₀.w
              comm := (i.naturality R₀.w).symm }
        Zigzag (J := Φ.RightResolution X₂) _ { hw := W₂.comp_mem _ _ R₄.hw (hi _), .. } :=
          Zigzag.of_hom
            { f := ρ.map R₄.w
              comm := (i.naturality R₄.w).symm }
        Zigzag _ R₄ := Zigzag.of_inv { f := (ι i).app R₄.X₁ })
-- 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₂
this_1 : W₁.IsMultiplicative
this_2 : Nonempty (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
this : IsPreconnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)

Tactic:
constructor
-- 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
rw : (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).IsMultiplicative
⊢ W₁.IsMultiplicative

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 : Φ.functor (W₁ := W₁) (W₂ := W₂).Full
inst_3 : Φ.functor (W₁ := W₁) (W₂ := W₂).Faithful
inst_4 : W₂.HasTwoOutOfThreeProperty
inst_5 : W₂.IsMultiplicative
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).IsMultiplicative

Tactic:
infer_instance
-- 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
⊢ W₁.IsMultiplicative

Tactic:
have : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
-- 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
this : W₁.IsMultiplicative
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
have := Φ.isLocalizedEquivalence_of_functorial_right_resolutions i hi 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 : Φ.functor (W₁ := W₁) (W₂ := W₂).Full
inst_3 : Φ.functor (W₁ := W₁) (W₂ := W₂).Faithful
inst_4 : W₂.HasTwoOutOfThreeProperty
inst_5 : W₂.IsMultiplicative
this_1 : W₁.IsMultiplicative
this : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
⊢ Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)

Tactic:
have := Φ.hasRightResolutions_arrow_of_functorial_resolutions i hi
-- 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
this_1 : W₁.IsMultiplicative
this_2 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
this : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
⊢ ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)

Tactic:
have := Φ.isConnected_rightResolution_of_functorial_resolutions i hi 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 : Φ.functor (W₁ := W₁) (W₂ := W₂).Full
inst_3 : Φ.functor (W₁ := W₁) (W₂ := W₂).Faithful
inst_4 : W₂.HasTwoOutOfThreeProperty
inst_5 : W₂.IsMultiplicative
this_1 : W₁.IsMultiplicative
this_2 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
this_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
this : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)

Tactic:
apply IsRightDerivabilityStructure.mk'

Premises used: CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
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_9 : TwoSquare.GuitartExact iso.inv
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 R.functor Y₂

Premises used: CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.EssSurj.mem_essImage
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
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_9 : TwoSquare.GuitartExact iso.inv
Y₂ : D₂
X₂ : C₂
e₂ : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂
have : ∀ (ρ : T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂), Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)
⊢ Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)

Tactic:
have ρ : T.LeftResolution X₂ := Classical.arbitrary _
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
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_9 : TwoSquare.GuitartExact iso.inv
Y₂ : D₂
X₂ : C₂
e₂ : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂
ρ : 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.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
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_9 : TwoSquare.GuitartExact iso.inv
Y₂ : D₂
X₂ : C₂
e₂ : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂
ρ : 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.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
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_9 : TwoSquare.GuitartExact iso.inv
⊢ B.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')

Tactic:
have : B.HasLeftResolutions := fun Y₂ ↦ by
    obtain ⟨X₂, ⟨e₂⟩⟩ := Functor.EssSurj.mem_essImage R.functor Y₂
    have ρ : T.LeftResolution X₂ := Classical.arbitrary _
    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.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
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_9 : TwoSquare.GuitartExact iso.inv
this_1 : B.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor (W₁ := W₁') (W₂ := W₂') W₁'.Q W₂'.Q
e' : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ W₂'.Q ≅ W₁'.Q ⋙ F :=
  CatCommSq.iso (B.functor (W₁ := W₁') (W₂ := W₂')) W₁'.Q W₂'.Q F
iso' : 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 }
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
  (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F :=
  CatCommSq.vComp (L.functor (W₁ := W₁) (W₂ := W₁')) W₁'.Q (T.functor (W₁ := W₁) (W₂ := W₂))
    (B.functor (W₁ := W₁') (W₂ := W₂')) F (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q
⊢ TwoSquare.GuitartExact
    (CatCommSq.iso (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
        (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F).inv

Tactic:
T.guitartExact_of_isLeftDerivabilityStructure' (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F
        (CatCommSq.iso _ _ _ _)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure'
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
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_9 : TwoSquare.GuitartExact iso.inv
this_1 : B.HasLeftResolutions (W₁ := W₁') (W₂ := W₂')
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor (W₁ := W₁') (W₂ := W₂') W₁'.Q W₂'.Q
e' : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ W₂'.Q ≅ W₁'.Q ⋙ F :=
  CatCommSq.iso (B.functor (W₁ := W₁') (W₂ := W₂')) W₁'.Q W₂'.Q F
iso' : 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 }
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
  (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F :=
  CatCommSq.vComp (L.functor (W₁ := W₁) (W₂ := W₁')) W₁'.Q (T.functor (W₁ := W₁) (W₂ := W₂))
    (B.functor (W₁ := W₁') (W₂ := W₂')) F (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q
h :
  TwoSquare.hComp iso.inv e'.inv =
    (CatCommSq.iso (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
        (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F).inv
⊢ (TwoSquare.hComp iso.inv e'.inv).GuitartExact

Tactic:
convert!
      T.guitartExact_of_isLeftDerivabilityStructure' (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F
        (CatCommSq.iso _ _ _ _)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure'