-- Mathlib/CategoryTheory/Localization/Adjunction.lean
lemma isLocalization [F.Full] [F.Faithful] :
    G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Tactic:
let W := ((MorphismProperty.isomorphisms C₂).inverseImage G)

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Tactic:
have : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X) := fun X =>
  Localization.inverts W.Q W _ (by
    change IsIso _
    infer_instance)

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
this : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
this✝ : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
this : IsIso (whiskerRight adj.unit W.Q)
e : W.Localization ≌ C₂ :=
  Equivalence.mk (lift G hG W.Q) (F ⋙ W.Q)
    (liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) (𝟭 W.Localization) (lift G hG W.Q ⋙ F ⋙ W.Q)
      (W.Q.leftUnitor.symm ≪≫ asIso (whiskerRight adj.unit W.Q)))
    (F.associator W.Q (lift G hG W.Q) ≪≫ isoWhiskerLeft F (fac G hG W.Q) ≪≫ asIso adj.counit)
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Tactic:
apply Functor.IsLocalization.of_equivalence_target W.Q W G e
  (Localization.fac G hG W.Q)

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
X : C₁
⊢ W (adj.unit.app X)

Tactic:
change IsIso _

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
X : C₁
⊢ IsIso (G.map (adj.unit.app X))

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
X : C₁
⊢ IsIso (G.map (adj.unit.app X))

Tactic:
infer_instance

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
this : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Tactic:
have : IsIso (whiskerRight adj.unit W.Q) := NatIso.isIso_of_isIso_app _

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
this✝ : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
this : IsIso (whiskerRight adj.unit W.Q)
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
this✝ : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
this : IsIso (whiskerRight adj.unit W.Q)
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Tactic:
let e : W.Localization ≌ C₂ := Equivalence.mk (Localization.lift G hG W.Q) (F ⋙ W.Q)
  (liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) _ _
  (W.Q.leftUnitor.symm ≪≫ asIso (whiskerRight adj.unit W.Q)))
  (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Localization.fac G hG W.Q) ≪≫
    asIso adj.counit)

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
this✝ : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X)
this : IsIso (whiskerRight adj.unit W.Q)
e : W.Localization ≌ C₂ :=
  Equivalence.mk (lift G hG W.Q) (F ⋙ W.Q)
    (liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) (𝟭 W.Localization) (lift G hG W.Q ⋙ F ⋙ W.Q)
      (W.Q.leftUnitor.symm ≪≫ asIso (whiskerRight adj.unit W.Q)))
    (F.associator W.Q (lift G hG W.Q) ≪≫ isoWhiskerLeft F (fac G hG W.Q) ≪≫ asIso adj.counit)
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)

Tactic:
have hG : W.IsInvertedBy G := fun _ _ _ hf => hf

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_6, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
W : MorphismProperty C₁ := (MorphismProperty.isomorphisms C₂).inverseImage G
hG : W.IsInvertedBy G
⊢ G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G)