C : Type u
inst✝² : Category C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono (prod.lift (𝟙 A) f ≫ (zeroMul t).hom)
⊢ IsIso f
C : Type u
inst✝² : Category C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
⊢ IsIso f
haveI : Mono (prod.lift (𝟙 A) f ≫ (zeroMul t).hom) := mono_comp _ _
C : Type u
inst✝² : Category C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono f
⊢ IsIso f
C : Type u
inst✝² : Category C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono (prod.lift (𝟙 A) f ≫ (zeroMul t).hom)
⊢ IsIso f
rw [zeroMul_hom, prod.lift_snd] at this
C : Type u
inst✝² : Category C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this✝ : Mono f
this : IsSplitEpi f
⊢ IsIso f
C : Type u
inst✝² : Category C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono f
⊢ IsIso f
haveI : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩
no goals
C : Type u
inst✝² : Category C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this✝ : Mono f
this : IsSplitEpi f
⊢ IsIso f
apply isIso_of_mono_of_isSplitEpi