-- Mathlib/CategoryTheory/Localization/Bousfield.lean
lemma W_iff_isIso_map {X Y : D} (f : X ⟶ Y) :
    W (· ∈ Set.range F.obj) f ↔ IsIso (G.map f)

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
h : IsIso ((G ⋙ F).map f)
⊢ IsIso (G.map f)

Tactic:
dsimp at h

Result:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
h : IsIso (F.map (G.map f))
⊢ IsIso (G.map f)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ IsIso ((G ⋙ F).map f) ↔ IsIso (G.map f)

Tactic:
constructor

Result:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ IsIso ((G ⋙ F).map f) → IsIso (G.map f)

case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ IsIso (G.map f) → IsIso ((G ⋙ F).map f)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ W (fun x => x ∈ Set.range F.obj) (f ≫ adj.unit.app Y) ↔ IsIso (G.map f)

Tactic:
erw [adj.unit.naturality f]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ W (fun x => x ∈ Set.range F.obj) (adj.unit.app X ≫ (G ⋙ F).map f) ↔ IsIso (G.map f)

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
a✝ : IsIso (G.map f)
⊢ IsIso ((G ⋙ F).map f)

Tactic:
rw [Functor.comp_map]

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
a✝ : IsIso (G.map f)
⊢ IsIso (F.map (G.map f))

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ IsIso (G.map f) → IsIso ((G ⋙ F).map f)

Tactic:
intro

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
a✝ : IsIso (G.map f)
⊢ IsIso ((G ⋙ F).map f)

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
a✝ : IsIso (G.map f)
⊢ IsIso (F.map (G.map f))

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ IsIso ((G ⋙ F).map f) → IsIso (G.map f)

Tactic:
intro h

Result:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
h : IsIso ((G ⋙ F).map f)
⊢ IsIso (G.map f)

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
h : IsIso (F.map (G.map f))
⊢ IsIso (G.map f)

Tactic:
exact isIso_of_fully_faithful F (G.map f)

Result:
no goals