awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this_1 :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
this : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom
rw : (TwoSquare.vComp' e'.hom e'''.hom e₁ e₂).GuitartExact ↔ TwoSquare.GuitartExact e.hom
⊢ TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))) ↔
    TwoSquare.GuitartExact e.hom
have rw₁ : TwoSquare.GuitartExact e.hom ↔ TwoSquare.GuitartExact e.hom
Tactic: rw [← TwoSquare.GuitartExact.vComp'_iff_of_equivalences e'.hom E₁ E₂ e''' e₁ e₂, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : W₁.ContainsIdentities
⊢ (id W₁).IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₁)
have rw : TwoSquare.GuitartExact (C₁ := C₁) (C₂ := C₁) (C₃ := W₁.Localization) (C₄ := W₁.Localization) (T :=
  (id W₁).functor (W₁ := W₁) (W₂ := W₁)) (L := W₁.Q) (R := W₁.Q) (B := 𝟭 W₁.Localization)
  (Iso.hom (Iso.refl ((id W₁).functor (W₁ := W₁) (W₂ := W₁) ⋙ W₁.Q)))
Tactic: rw [(LocalizerMorphism.id W₁).isRightDerivabilityStructure_iff W₁.Q W₁.Q (𝟭 W₁.Localization)
    (Iso.refl _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
have eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
Tactic: have eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv :=
    TwoSquare.guitartExact_op_iff _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
have mp : Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) →
  Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
mp :
  Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) →
    Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
have mpr : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op) →
  Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
hasLeftResolutions : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
guitartExact' :
  TwoSquare.GuitartExact (R := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
    (Iso.inv
      (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
have mp : TwoSquare.GuitartExact e'.hom
Tactic: rwa [Φ.op.isRightDerivabilityStructure_iff _ _ _ e', eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
have rw : Φ.op (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.op) (W₂ := W₂.op)
Tactic: rw [hasLeftResolutions_iff_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
Tactic: have : Φ.HasLeftResolutions := by
      rw [hasLeftResolutions_iff_op]
      infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have mpr : TwoSquare.GuitartExact (R := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
  (Iso.inv
    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
Tactic: refine ⟨inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
⊢ TwoSquare.GuitartExact (R := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
    (Iso.inv
      (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
have mpr : TwoSquare.GuitartExact e'.hom
Tactic: rw [← eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ TwoSquare.GuitartExact e.inv
have rw : TwoSquare.GuitartExact (NatIso.op e.symm).hom ↔ (TwoSquare.op e.inv).GuitartExact
Tactic: rw [isLeftDerivabilityStructure_iff_op,
    Φ.op.isRightDerivabilityStructure_iff L₁.op L₂.op F.op (NatIso.op e.symm),
    ← TwoSquare.guitartExact_op_iff e.inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : W₁.ContainsIdentities
⊢ (id W₁).IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₁)
have rw : TwoSquare.GuitartExact (C₁ := C₁) (C₂ := W₁.Localization) (C₃ := C₁) (C₄ := W₁.Localization) (T := W₁.Q) (L :=
  (id W₁).functor (W₁ := W₁) (W₂ := W₁)) (R := 𝟭 W₁.Localization) (B := W₁.Q)
  (Iso.inv (Iso.refl ((id W₁).functor (W₁ := W₁) (W₂ := W₁) ⋙ W₁.Q)))
Tactic: rw [(LocalizerMorphism.id W₁).isLeftDerivabilityStructure_iff W₁.Q W₁.Q (𝟭 W₁.Localization)
    (Iso.refl _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
have eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
Tactic: have eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom :=
    TwoSquare.guitartExact_op_iff _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
have refine_1 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) →
  Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂) →
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
        (Iso.hom
          (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
            (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))) →
      Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
Tactic: refine ⟨fun ⟨_, _⟩ ↦ ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
refine_1 :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) →
    Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂) →
      TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
          (Iso.hom
            (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
              (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))) →
        Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
have refine_2 : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op) →
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
Tactic: refine ⟨fun ⟨_, _⟩ ↦ ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
have rw : Φ.op (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.op) (W₂ := W₂.op)
Tactic: rw [hasRightResolutions_iff_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
Tactic: have : Φ.HasRightResolutions := by
      rw [hasRightResolutions_iff_op]
      infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have refine_2 : TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
  (Iso.hom
    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
Tactic: refine ⟨inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
e' : Φ.functor (W₁ := W₁) (W₂ := W₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
⊢ TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
    (Iso.hom
      (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
have refine_2 : TwoSquare.GuitartExact e'.inv
Tactic: rw [← eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor (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₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
φ : R ⟶ R'
⊢ ((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
                (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).structuredArrowDownwards
            X₂).map
        (StructuredArrow.homMk (φ.f (W₁ := W₁) (W₂ := W₂)) ⋯) ≫
      (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y) ⋯)).hom =
    (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y) ⋯)).hom
have h : StructuredArrow.Hom.right
    (((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
                (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).structuredArrowDownwards
            X₂).map
        (StructuredArrow.homMk (φ.f (W₁ := W₁) (W₂ := W₂)) sorry) ≫
      (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) sorry).inv ≫ y) sorry)).hom) =
  StructuredArrow.Hom.right
    (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) sorry).inv ≫ y) sorry)).hom
Tactic: ext