C : Type u
inst✝⁴ : Category C
D : Type ?u.46661
inst✝³ : Category D
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category C₁
inst✝¹ : Category C₂
inst✝ : Category C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : IsInvertedBy W F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)
C : Type u
inst✝⁴ : Category C
D : Type ?u.46661
inst✝³ : Category D
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category C₁
inst✝¹ : Category C₂
inst✝ : Category C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : IsInvertedBy W F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso ((F ⋙ G).map f)
haveI := hF f hf
C : Type u
inst✝⁴ : Category C
D : Type ?u.46661
inst✝³ : Category D
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category C₁
inst✝¹ : Category C₂
inst✝ : Category C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : IsInvertedBy W F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))
C : Type u
inst✝⁴ : Category C
D : Type ?u.46661
inst✝³ : Category D
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category C₁
inst✝¹ : Category C₂
inst✝ : Category C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : IsInvertedBy W F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)
dsimp
no goals
C : Type u
inst✝⁴ : Category C
D : Type ?u.46661
inst✝³ : Category D
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category C₁
inst✝¹ : Category C₂
inst✝ : Category C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : IsInvertedBy W F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))
infer_instance