-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
@[simp]
lemma IsInvertedBy.iff_comp {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃]
    (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (G : C₂ ⥤ C₃) [G.ReflectsIsomorphisms] :
    W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F

Proof state:
case mpr
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
hF : W.IsInvertedBy F
⊢ W.IsInvertedBy (F ⋙ G)

Tactic:
exact IsInvertedBy.of_comp W F hF G

Result:
no goals

Proof state:
case mpr
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy F → W.IsInvertedBy (F ⋙ G)

Tactic:
intro hF

Result:
case mpr
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
hF : W.IsInvertedBy F
⊢ W.IsInvertedBy (F ⋙ G)

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (G.map (F.map f))
⊢ IsIso (F.map f)

Tactic:
exact isIso_of_reflects_iso (F.map f) G

Result:
no goals

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy (F ⋙ G) → W.IsInvertedBy F

Tactic:
intro h X Y f hf

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)

Tactic:
have : IsIso (G.map (F.map f)) := h _ hf

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (G.map (F.map f))
⊢ IsIso (F.map f)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F

Tactic:
constructor

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy (F ⋙ G) → W.IsInvertedBy F

case mpr
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_4, u_1} C₁
inst✝² : Category.{u_5, u_2} C₂
inst✝¹ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy F → W.IsInvertedBy (F ⋙ G)