T : Type u
inst✝² : Category T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := CommaMorphism.mk (inv ff.left) (inv ff.right)
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g
T : Type u
inst✝² : Category T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g
let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩
T : Type u
inst✝² : Category T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := CommaMorphism.mk (inv ff.left) (inv ff.right)
⊢ ff ≫ inverse = 𝟙 f ∧ inverse ≫ ff = 𝟙 g
T : Type u
inst✝² : Category T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := CommaMorphism.mk (inv ff.left) (inv ff.right)
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g
apply Exists.intro inverse
no goals
T : Type u
inst✝² : Category T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := CommaMorphism.mk (inv ff.left) (inv ff.right)
⊢ ff ≫ inverse = 𝟙 f ∧ inverse ≫ ff = 𝟙 g
aesop_cat
no goals
T : Type u
inst✝² : Category T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
⊢ (𝟭 T).map (inv ff.left) ≫ f.hom = g.hom ≫ (𝟭 T).map (inv ff.right)
simp