case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61837
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61837
inst✝ : Category D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
intro X Y Z e f
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61837
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ IsIso f → IsIso (f ≫ e.hom)
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61837
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
simp only [isomorphisms.iff]
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61837
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
a✝ : IsIso f
⊢ IsIso (f ≫ e.hom)
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61837
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ IsIso f → IsIso (f ≫ e.hom)
intro
no goals
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61837
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
a✝ : IsIso f
⊢ IsIso (f ≫ e.hom)
infer_instance