G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ g₁ = g₂
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
⊢ g₁ = g₂
have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by
  apply int_hom_ext
  simpa using h
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ g₁ = g₂
have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0
no goals
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂
apply asHom_injective t1
case w
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
⊢ ↑(asHom g₁ ≫ f) 1 = ↑(asHom g₂ ≫ f) 1
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
⊢ asHom g₁ ≫ f = asHom g₂ ≫ f
apply int_hom_ext
no goals
case w
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
⊢ ↑(asHom g₁ ≫ f) 1 = ↑(asHom g₂ ≫ f) 1
simpa using h