C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ IsInvertedBy W F₁ ↔ IsInvertedBy W F₂
suffices ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f) by
  constructor
  exact fun h X Y f hf => by
    rw [← this]
    exact h f hf
  exact fun h X Y f hf => by
    rw [this]
    exact h f hf
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
intro X Y f
no goals
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)
exact (RespectsIso.isomorphisms D).arrow_mk_iso_iff (Arrow.isoMk (e.app X) (e.app Y) (by simp))
case mp
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₁ → IsInvertedBy W F₂

case mpr
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₂ → IsInvertedBy W F₁
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₁ ↔ IsInvertedBy W F₂
constructor
case mpr
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₂ → IsInvertedBy W F₁
case mp
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₁ → IsInvertedBy W F₂

case mpr
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₂ → IsInvertedBy W F₁
exact fun h X Y f hf => by
  rw [← this]
  exact h f hf
no goals
case mpr
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₂ → IsInvertedBy W F₁
exact fun h X Y f hf => by
  rw [this]
  exact h f hf
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₁
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₁.map f)
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₁
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₂.map f)
rw [← this]
no goals
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₁
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₁.map f)
exact h f hf
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₂
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₂.map f)
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₂
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₁.map f)
rw [this]
no goals
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₂
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₂.map f)
exact h f hf
no goals
C : Type u
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ (e.app X).hom ≫ (Arrow.mk (F₂.map f)).hom = (Arrow.mk (F₁.map f)).hom ≫ (e.app Y).hom
simp