C : Type u
inst✝¹ : Category C
D : Type ?u.62388
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
⊢ IsIso (f ≫ g)
C : Type u
inst✝¹ : Category C
D : Type ?u.62388
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.isomorphisms C f
hg : MorphismProperty.isomorphisms C g
⊢ MorphismProperty.isomorphisms C (f ≫ g)
rw [isomorphisms.iff] at hf hg⊢
C : Type u
inst✝¹ : Category C
D : Type ?u.62388
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
this : IsIso f
⊢ IsIso (f ≫ g)
C : Type u
inst✝¹ : Category C
D : Type ?u.62388
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
⊢ IsIso (f ≫ g)
haveI := hf
C : Type u
inst✝¹ : Category C
D : Type ?u.62388
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
this✝ : IsIso f
this : IsIso g
⊢ IsIso (f ≫ g)
C : Type u
inst✝¹ : Category C
D : Type ?u.62388
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
this : IsIso f
⊢ IsIso (f ≫ g)
haveI := hg
no goals
C : Type u
inst✝¹ : Category C
D : Type ?u.62388
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
this✝ : IsIso f
this : IsIso g
⊢ IsIso (f ≫ g)
infer_instance