[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
A✝ B✝ : C
f : A✝ ⟶ B✝
i : IsIso (F.map f)
⊢ F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 A✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
A✝ B✝ : C
f : A✝ ⟶ B✝
i : IsIso (F.map f)
⊢ F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 B✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : ReflectsIsomorphisms F
inst✝ : ReflectsIsomorphisms G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (G.map (F.map f))
⊢ IsIso f
[PROOFSTEP]
haveI := isIso_of_reflects_iso (F.map f) G
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : ReflectsIsomorphisms F
inst✝ : ReflectsIsomorphisms G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (G.map (F.map f))
this : IsIso (F.map f)
⊢ IsIso f
[PROOFSTEP]
exact isIso_of_reflects_iso f F
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : Balanced C
F : C ⥤ D
inst✝¹ : ReflectsMonomorphisms F
inst✝ : ReflectsEpimorphisms F
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (F.map f)
⊢ IsIso f
[PROOFSTEP]
haveI : Epi f := epi_of_epi_map F inferInstance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : Balanced C
F : C ⥤ D
inst✝¹ : ReflectsMonomorphisms F
inst✝ : ReflectsEpimorphisms F
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (F.map f)
this : Epi f
⊢ IsIso f
[PROOFSTEP]
haveI : Mono f := mono_of_mono_map F inferInstance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : Balanced C
F : C ⥤ D
inst✝¹ : ReflectsMonomorphisms F
inst✝ : ReflectsEpimorphisms F
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (F.map f)
this✝ : Epi f
this : Mono f
⊢ IsIso f
[PROOFSTEP]
exact isIso_of_mono_of_epi f
