awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
⊢ Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
have refine : W₂.IsInvertedBy (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip
Tactic: refine uncurry.obj (Construction.lift (prodLift₁ F hF).flip ?_).flip
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
X Y : C₂
f₂ : X ⟶ Y
hf₂ : W₂ f₂
X₁ : W₁.Localization
⊢ IsIso (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app X₁)
have obtain : ∀ (X₁ : C₁),
  IsIso (X :=
    ((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.obj X).obj
      ((Construction.objEquiv W₁ : (a : C₁) → W₁.Localization) X₁))
    (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app
      ((Construction.objEquiv W₁ : (a : C₁) → W₁.Localization) X₁))
Tactic: obtain ⟨X₁, rfl⟩ := (Construction.objEquiv W₁).surjective X₁
Cleared hypotheses: X₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
X Y : C₂
f₂ : X ⟶ Y
hf₂ : W₂ f₂
⊢ IsIso ((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂)
have this : ∀ (X₁ : W₁.Localization), IsIso (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app X₁)
Tactic: haveI : ∀ (X₁ : W₁.Localization),
      IsIso (((Functor.flip (prodLift₁ F hF)).map f₂).app X₁) := fun X₁ => by
    obtain ⟨X₁, rfl⟩ := (Construction.objEquiv W₁).surjective X₁
    exact ((MorphismProperty.isomorphisms E).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (eqToIso (Functor.congr_obj (prod_fac₁ F hF) X₁))).app (Arrow.mk f₂))).2
          (hF _ ⟨MorphismProperty.id_mem _ _, hf₂⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
⊢ W₂.Q ⋙ (obj curry (prodLift (W₁ := W₁) (W₂ := W₂) F hF)).flip = (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip
have simp : W₂.Q ⋙ Construction.lift (W := W₂) (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip sorry =
  (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip
Tactic: simp only [prodLift, Functor.curry_obj_uncurry_obj, Functor.flip_flip]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
⊢ W₁.Q.prod W₂.Q ⋙ prodLift (W₁ := W₁) (W₂ := W₂) F hF = F
have rw : obj uncurry (W₁.Q ⋙ (W₂.Q ⋙ (obj curry (prodLift (W₁ := W₁) (W₂ := W₂) F hF)).flip).flip) = F
Tactic: rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
    Functor.uncurry_obj_curry_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
rw : obj uncurry (W₁.Q ⋙ (W₂.Q ⋙ (obj curry (prodLift (W₁ := W₁) (W₂ := W₂) F hF)).flip).flip) = F
⊢ W₁.Q.prod W₂.Q ⋙ prodLift (W₁ := W₁) (W₂ := W₂) F hF = F
have rw₁ : obj uncurry (W₁.Q ⋙ (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.flip) = F
Tactic: rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
    Functor.uncurry_obj_curry_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
rw : obj uncurry (W₁.Q ⋙ (W₂.Q ⋙ (obj curry (prodLift (W₁ := W₁) (W₂ := W₂) F hF)).flip).flip) = F
rw₁ : obj uncurry (W₁.Q ⋙ (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.flip) = F
⊢ W₁.Q.prod W₂.Q ⋙ prodLift (W₁ := W₁) (W₂ := W₂) F hF = F
have rw₂ : obj uncurry (W₁.Q ⋙ prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF) = F
Tactic: rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
    Functor.uncurry_obj_curry_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
rw : obj uncurry (W₁.Q ⋙ (W₂.Q ⋙ (obj curry (prodLift (W₁ := W₁) (W₂ := W₂) F hF)).flip).flip) = F
rw₁ : obj uncurry (W₁.Q ⋙ (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.flip) = F
rw₂ : obj uncurry (W₁.Q ⋙ prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF) = F
⊢ W₁.Q.prod W₂.Q ⋙ prodLift (W₁ := W₁) (W₂ := W₂) F hF = F
have rw₃ : obj uncurry (obj curry F) = F
Tactic: rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
    Functor.uncurry_obj_curry_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (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₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
rw : obj uncurry (W₁.Q ⋙ (W₂.Q ⋙ (obj curry (prodLift (W₁ := W₁) (W₂ := W₂) F hF)).flip).flip) = F
rw₁ : obj uncurry (W₁.Q ⋙ (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.flip) = F
rw₂ : obj uncurry (W₁.Q ⋙ prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF) = F
rw₃ : obj uncurry (obj curry F) = F
⊢ W₁.Q.prod W₂.Q ⋙ prodLift (W₁ := W₁) (W₂ := W₂) F hF = F
have rw₄ : F = F
Tactic: rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
    Functor.uncurry_obj_curry_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Prod (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_4 : W₁.ContainsIdentities
inst_5 : W₂.ContainsIdentities
inst_6 : L₁.IsLocalization W₁
inst_7 : L₂.IsLocalization W₂
⊢ (L₁.prod L₂).IsLocalization (W₁.prod W₂)
have this : (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)
Tactic: haveI := Construction.prodIsLocalization W₁ W₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Quotient (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
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)
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L' : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (CategoryTheory.Quotient homRel) D
univ : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L' W' E
x x_1 : C
x_2 : x ⟶ x_1
hf : W x_2
⊢ W' ((Quotient.functor homRel).map x_2)
have rwa : ∀ (hf : W'.inverseImage (Quotient.functor homRel) x_2), W' ((Quotient.functor homRel).map x_2)
Tactic: rwa [hW] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Quotient (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
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)
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L' : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (CategoryTheory.Quotient homRel) D
univ : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L' W' E
F : CategoryTheory.Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
⊢ (Quotient.functor homRel ⋙ L') ⋙ univ.lift (W := W') (CategoryTheory.Quotient.lift homRel F ⋯) ⋯ = F
have rw : Quotient.functor homRel ⋙ L' ⋙ univ.lift (W := W') (CategoryTheory.Quotient.lift homRel F sorry) sorry = F
Tactic: rw [Functor.assoc, univ.fac, Quotient.lift_spec]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Quotient (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
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)
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L' : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (CategoryTheory.Quotient homRel) D
univ : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L' W' E
F : CategoryTheory.Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
rw : Quotient.functor homRel ⋙ L' ⋙ univ.lift (W := W') (CategoryTheory.Quotient.lift homRel F ⋯) ⋯ = F
⊢ (Quotient.functor homRel ⋙ L') ⋙ univ.lift (W := W') (CategoryTheory.Quotient.lift homRel F ⋯) ⋯ = F
have rw₁ : Quotient.functor homRel ⋙ CategoryTheory.Quotient.lift homRel F sorry = F
Tactic: rw [Functor.assoc, univ.fac, Quotient.lift_spec]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Quotient (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
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)
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L' : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (CategoryTheory.Quotient homRel) D
univ : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L' W' E
F : CategoryTheory.Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
rw : Quotient.functor homRel ⋙ L' ⋙ univ.lift (W := W') (CategoryTheory.Quotient.lift homRel F ⋯) ⋯ = F
rw₁ : Quotient.functor homRel ⋙ CategoryTheory.Quotient.lift homRel F ⋯ = F
⊢ (Quotient.functor homRel ⋙ L') ⋙ univ.lift (W := W') (CategoryTheory.Quotient.lift homRel F ⋯) ⋯ = F
have rw₂ : F = F
Tactic: rw [Functor.assoc, univ.fac, Quotient.lift_spec]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (hypothesis)
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₂
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂
have this : L₂.EssSurj
Tactic: have := Localization.essSurj L₂ W₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
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
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂
have have : ∀ (R : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) (L₂.objPreimage X₂)), (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂
Tactic: have R : Φ.RightResolution (L₂.objPreimage X₂) := Classical.arbitrary _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
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
⊢ 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₁)))
have 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₁)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
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₁)))
⊢ 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₁)))
have 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 α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (hypothesis)
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₂)
have this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
Tactic: have := Φ.essSurj_of_hasRightResolutions L₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
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 (α.app X₂)
have 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₂)))
Tactic: rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (hypothesis)
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₁)))
⊢ IsIso α
have this : ∀ (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α
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (hypothesis)
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₂
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂
have this : L₂.EssSurj
Tactic: have := Localization.essSurj L₂ W₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
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
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂
have have : ∀ (L : Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) (L₂.objPreimage X₂)), (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).essImage X₂
Tactic: have L : Φ.LeftResolution (L₂.objPreimage X₂) := Classical.arbitrary _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
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
⊢ 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₁)))
have 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₁)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
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₁)))
⊢ 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₁)))
have 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 α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (hypothesis)
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α :
  ∀ (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₂)
have this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
Tactic: have := Φ.essSurj_of_hasLeftResolutions L₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Resolution (goal)
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α :
  ∀ (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 (α.app X₂)
have 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₂)))
Tactic: rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]