case mp
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f

case mpr
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g ↔ f.f = g.f
constructor
case mp
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
f g : P ⟶ Q
h : f = g
⊢ f.f = g.f
case mp
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f
intro h
no goals
case mp
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
f g : P ⟶ Q
h : f = g
⊢ f.f = g.f
rw [h]
no goals
case mpr
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g
apply Hom.ext