-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
@[simp]
lemma IsInvertedBy.isoClosure_iff (W : MorphismProperty C) (F : C ⥤ D) :
    W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
this : IsIso (F.map f')
⊢ IsIso (F.map e.inv.left ≫ F.map f' ≫ F.map e.hom.right)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F → W.IsInvertedBy F

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.IsInvertedBy F → W.isoClosure.IsInvertedBy F

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map e.inv.left ≫ F.map f' ≫ F.map e.hom.right)

Tactic:
have := h _ hf'

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
this : IsIso (F.map f')
⊢ IsIso (F.map e.inv.left ≫ F.map f' ≫ F.map e.hom.right)

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map f)

Tactic:
simp only [Arrow.iso_w' e, F.map_comp]

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map e.inv.left ≫ F.map f' ≫ F.map e.hom.right)

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.isoClosure.IsInvertedBy F
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)

Tactic:
exact h _ (W.le_isoClosure _ hf)

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.IsInvertedBy F → W.isoClosure.IsInvertedBy F

Tactic:
intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map f)

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F → W.IsInvertedBy F

Tactic:
intro h X Y f hf

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.isoClosure.IsInvertedBy F
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)