English
In a binary biproduct, biprod.map f g being an iso implies f is an iso (alternative formulation).
Русский
В бинарном биобразовании, изоморфизм biprod.map f g -> f является изоморфизмом (альтернативная формулировка).
LaTeX
$$$\mathrm{IsIso}(\mathrm{biprod.map} f g) \Rightarrow \mathrm{IsIso}(f)$$$
Lean4
/-- If
```
(f 0)
(0 g)
```
is invertible, then `f` is invertible.
-/
theorem isIso_left_of_isIso_biprod_map {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [IsIso (biprod.map f g)] : IsIso f :=
⟨⟨biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst,
⟨by
have t := congrArg (fun p : W ⊞ X ⟶ W ⊞ X => biprod.inl ≫ p ≫ biprod.fst) (IsIso.hom_inv_id (biprod.map f g))
simp only [Category.id_comp, Category.assoc, biprod.inl_map_assoc] at t
simp [t],
by
have t := congrArg (fun p : Y ⊞ Z ⟶ Y ⊞ Z => biprod.inl ≫ p ≫ biprod.fst) (IsIso.inv_hom_id (biprod.map f g))
simp only [Category.id_comp, Category.assoc, biprod.map_fst] at t
simp only [Category.assoc]
simp [t]⟩⟩⟩
