C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → (IsIso (F₁.map f) ↔ IsIso (F₂.map f))
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ : C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)
revert F₁ F₂
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → IsIso (F₁.map f) → IsIso (F₂.map f)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → (IsIso (F₁.map f) ↔ IsIso (F₂.map f))
suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) by
  exact fun F₁ F₂ e => ⟨this e, this e.symm⟩
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → IsIso (F₁.map f) → IsIso (F₂.map f)
intro F₁ F₂ e hf
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ F₂.map f ≫ e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X = 𝟙 (F₂.obj X)

case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ (e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X) ≫ F₂.map f = 𝟙 (F₂.obj Y)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)
refine' IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, _, _⟩
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
this : ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → IsIso (F₁.map f) → IsIso (F₂.map f)
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → (IsIso (F₁.map f) ↔ IsIso (F₂.map f))
exact fun F₁ F₂ e => ⟨this e, this e.symm⟩
no goals
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ F₂.map f ≫ e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X = 𝟙 (F₂.obj X)
simp only [NatTrans.naturality_assoc, IsIso.hom_inv_id_assoc, Iso.inv_hom_id_app]
no goals
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
X✝ Y✝ X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ (e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X) ≫ F₂.map f = 𝟙 (F₂.obj Y)
simp only [assoc, ← e.hom.naturality, IsIso.inv_hom_id_assoc, Iso.inv_hom_id_app]