C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso f
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso h
w : f ≫ g = h
⊢ IsIso f
rw [← w] at hh
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
this : IsIso (f ≫ g)
⊢ IsIso f
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso f
haveI := hh
no goals
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso g
hh : IsIso (f ≫ g)
w : f ≫ g = h
this : IsIso (f ≫ g)
⊢ IsIso f
exact of_isIso_comp_right f g