case mk
C : Type u_1
inst✝ : Category C
Q : Karoubi C
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : (mk X✝ p✝).X = Q.X
h_p : (mk X✝ p✝).p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ mk X✝ p✝ = Q
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
h_X : P.X = Q.X
h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ P = Q
cases P
case mk.mk
C : Type u_1
inst✝ : Category C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : (mk X✝¹ p✝¹).X = (mk X✝ p✝).X
h_p : (mk X✝¹ p✝¹).p ≫ eqToHom h_X = eqToHom h_X ≫ (mk X✝ p✝).p
⊢ mk X✝¹ p✝¹ = mk X✝ p✝
case mk
C : Type u_1
inst✝ : Category C
Q : Karoubi C
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : (mk X✝ p✝).X = Q.X
h_p : (mk X✝ p✝).p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ mk X✝ p✝ = Q
cases Q
case mk.mk
C : Type u_1
inst✝ : Category C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : X✝¹ = X✝
h_p : p✝¹ ≫ eqToHom h_X = eqToHom h_X ≫ p✝
⊢ mk X✝¹ p✝¹ = mk X✝ p✝
case mk.mk
C : Type u_1
inst✝ : Category C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : (mk X✝¹ p✝¹).X = (mk X✝ p✝).X
h_p : (mk X✝¹ p✝¹).p ≫ eqToHom h_X = eqToHom h_X ≫ (mk X✝ p✝).p
⊢ mk X✝¹ p✝¹ = mk X✝ p✝
dsimp at h_X h_p
case mk.mk
C : Type u_1
inst✝ : Category C
X✝ : C
p✝¹ : X✝ ⟶ X✝
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_p : p✝¹ ≫ eqToHom (_ : X✝ = X✝) = eqToHom (_ : X✝ = X✝) ≫ p✝
⊢ mk X✝ p✝¹ = mk X✝ p✝
case mk.mk
C : Type u_1
inst✝ : Category C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : X✝¹ = X✝
h_p : p✝¹ ≫ eqToHom h_X = eqToHom h_X ≫ p✝
⊢ mk X✝¹ p✝¹ = mk X✝ p✝
subst h_X
no goals
case mk.mk
C : Type u_1
inst✝ : Category C
X✝ : C
p✝¹ : X✝ ⟶ X✝
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_p : p✝¹ ≫ eqToHom (_ : X✝ = X✝) = eqToHom (_ : X✝ = X✝) ≫ p✝
⊢ mk X✝ p✝¹ = mk X✝ p✝
simpa only [mk.injEq, heq_eq_eq, true_and, eqToHom_refl, comp_id, id_comp] using h_p