awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (goal)
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
have rw : (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).IsMultiplicative
Tactic: rw [hW₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (hypothesis)
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₂
⊢ IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
have this : W₁.IsMultiplicative
Tactic: have : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (hypothesis)
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
⊢ IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
have this₁ : Nonempty (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
Tactic: have : Nonempty (Φ.RightResolution X₂) := ⟨{ hw := hi X₂, .. }⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (hypothesis)
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₂)
⊢ IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
have this₁ : 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₁ })
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (goal)
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
have rw : (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).IsMultiplicative
Tactic: rw [hW₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (hypothesis)
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
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this : W₁.IsMultiplicative
Tactic: have : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (hypothesis)
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
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this₁ : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
Tactic: have := Φ.isLocalizedEquivalence_of_functorial_right_resolutions i hi hW₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (hypothesis)
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₂)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this₁ : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
Tactic: have := Φ.hasRightResolutions_arrow_of_functorial_resolutions i hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (hypothesis)
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)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this₁ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
Tactic: have := Φ.isConnected_rightResolution_of_functorial_resolutions i hi hW₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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₂
⊢ Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)
have obtain : ∀ (X₂ : C₂) (e₂ : R.functor (W₁ := W₂) (W₂ := W₂').obj X₂ ≅ Y₂), Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)
Tactic: obtain ⟨X₂, ⟨e₂⟩⟩ := Functor.EssSurj.mem_essImage R.functor Y₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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₂
⊢ Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)
have have : ∀ (ρ : T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂), Nonempty (B.LeftResolution (W₁ := W₁') (W₂ := W₂') Y₂)
Tactic: have ρ : T.LeftResolution X₂ := Classical.arbitrary _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (hypothesis)
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.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
have this : 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) }⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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.hComp iso.inv e'.inv).GuitartExact
have 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
Tactic: convert!
      T.guitartExact_of_isLeftDerivabilityStructure' (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F
        (CatCommSq.iso _ _ _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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.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
have h : ∀ (X : C₁),
  (TwoSquare.hComp iso.inv e'.inv).natTrans.app X =
    (TwoSquare.natTrans
          (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).app
      X
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (hypothesis)
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
⊢ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
have this₁ : (TwoSquare.hComp iso.inv e'.inv).GuitartExact
Tactic: have : (TwoSquare.hComp iso.inv e'.inv).GuitartExact := by
    convert!
      T.guitartExact_of_isLeftDerivabilityStructure' (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F
        (CatCommSq.iso _ _ _ _)
    ext
    simp [e', CatCommSq.iso, iso']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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_2 : 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
this : (TwoSquare.hComp iso.inv e'.inv).GuitartExact
⊢ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
have rw : TwoSquare.GuitartExact e'.inv
Tactic: rw [B.isLeftDerivabilityStructure_iff W₁'.Q W₂'.Q F e']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (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_11 : TwoSquare.GuitartExact iso.inv
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
have refine : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂') → T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
Tactic: refine ⟨fun _ ↦ isLeftDerivabilityStructure_of_isLocalizedEquivalence iso, fun _ ↦ ?_⟩