case mk
C : Type u
inst✝ : Category C
X Y Z : C
β : X ≅ Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w : (mk hom✝ inv✝).hom = β.hom
this : (mk hom✝ inv✝).inv = β.inv
⊢ mk hom✝ inv✝ = β
C : Type u
inst✝ : Category C
X Y Z : C
α β : X ≅ Y
w : α.hom = β.hom
this : α.inv = β.inv
⊢ α = β
cases α
case mk.mk
C : Type u
inst✝ : Category C
X Y Z : C
hom✝¹ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝¹ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝¹ = 𝟙 Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w : (mk hom✝¹ inv✝¹).hom = (mk hom✝ inv✝).hom
this : (mk hom✝¹ inv✝¹).inv = (mk hom✝ inv✝).inv
⊢ mk hom✝¹ inv✝¹ = mk hom✝ inv✝
case mk
C : Type u
inst✝ : Category C
X Y Z : C
β : X ≅ Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w : (mk hom✝ inv✝).hom = β.hom
this : (mk hom✝ inv✝).inv = β.inv
⊢ mk hom✝ inv✝ = β
cases β
case mk.mk.refl
C : Type u
inst✝ : Category C
X Y Z : C
hom✝ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝ = 𝟙 Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
this : (mk hom✝ inv✝¹).inv = (mk hom✝ inv✝).inv
⊢ mk hom✝ inv✝¹ = mk hom✝ inv✝
case mk.mk
C : Type u
inst✝ : Category C
X Y Z : C
hom✝¹ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝¹ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝¹ = 𝟙 Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w : (mk hom✝¹ inv✝¹).hom = (mk hom✝ inv✝).hom
this : (mk hom✝¹ inv✝¹).inv = (mk hom✝ inv✝).inv
⊢ mk hom✝¹ inv✝¹ = mk hom✝ inv✝
cases w
case mk.mk.refl.refl
C : Type u
inst✝ : Category C
X Y Z : C
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝¹ : inv✝ ≫ hom✝ = 𝟙 Y
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
⊢ mk hom✝ inv✝ = mk hom✝ inv✝
case mk.mk.refl
C : Type u
inst✝ : Category C
X Y Z : C
hom✝ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝ = 𝟙 Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
this : (mk hom✝ inv✝¹).inv = (mk hom✝ inv✝).inv
⊢ mk hom✝ inv✝¹ = mk hom✝ inv✝
cases this
no goals
case mk.mk.refl.refl
C : Type u
inst✝ : Category C
X Y Z : C
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝¹ : inv✝ ≫ hom✝ = 𝟙 Y
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
⊢ mk hom✝ inv✝ = mk hom✝ inv✝
rfl
no goals
C : Type u
inst✝ : Category C
X Y Z : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv = α.inv ≫ β.hom ≫ β.inv
rw [Iso.hom_inv_id, Category.comp_id]
no goals
C : Type u
inst✝ : Category C
X Y Z : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv ≫ β.hom ≫ β.inv = (α.inv ≫ α.hom) ≫ β.inv
rw [Category.assoc, ← w]
no goals
C : Type u
inst✝ : Category C
X Y Z : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ (α.inv ≫ α.hom) ≫ β.inv = β.inv
rw [Iso.inv_hom_id, Category.id_comp]