-- Mathlib/CategoryTheory/Localization/Resolution.lean
lemma isIso_iff_of_hasRightResolutions [Φ.HasRightResolutions] {F G : D₂ ⥤ H} (α : F ⟶ G) :
    IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
a✝ : IsIso α
X₁✝ : C₁
⊢ IsIso (α.app (L₂.obj (Φ.functor.obj X₁✝)))

Tactic:
infer_instance

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage X₂)))

Tactic:
apply hα

Result:
no goals

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α → ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

Tactic:
intros

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
a✝ : IsIso α
X₁✝ : C₁
⊢ IsIso (α.app (L₂.obj (Φ.functor.obj X₁✝)))

Proof state:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α

Tactic:
intro hα

Result:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
⊢ IsIso α

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app X₂)

Tactic:
rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]

Result:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage X₂)))

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

Tactic:
constructor

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α → ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α

Proof state:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
⊢ IsIso α

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α

Result:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
this : ∀ (X₂ : D₂), IsIso (α.app X₂)
⊢ IsIso α

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
⊢ IsIso (α.app X₂)

Tactic:
have := Φ.essSurj_of_hasRightResolutions L₂

Result:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app X₂)