[GOAL]
M N : GroupWithZeroCat
f g : M ⟶ N
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
M N : GroupWithZeroCat
g : M ⟶ N
toZeroHom✝ : ZeroHom ↑M ↑N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : ↑M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h : (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = (fun f => f.toFun) g
⊢ { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
M N : GroupWithZeroCat
toZeroHom✝¹ : ZeroHom ↑M ↑N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : ↑M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom ↑M ↑N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : ↑M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toZeroHom
M N : GroupWithZeroCat
toZeroHom✝¹ : ZeroHom ↑M ↑N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : ↑M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom ↑M ↑N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : ↑M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ toZeroHom✝¹ = toZeroHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toZeroHom.a
M N : GroupWithZeroCat
toZeroHom✝¹ : ZeroHom ↑M ↑N
map_one'✝¹ : ZeroHom.toFun toZeroHom✝¹ 1 = 1
map_mul'✝¹ : ∀ (x y : ↑M), ZeroHom.toFun toZeroHom✝¹ (x * y) = ZeroHom.toFun toZeroHom✝¹ x * ZeroHom.toFun toZeroHom✝¹ y
toZeroHom✝ : ZeroHom ↑M ↑N
map_one'✝ : ZeroHom.toFun toZeroHom✝ 1 = 1
map_mul'✝ : ∀ (x y : ↑M), ZeroHom.toFun toZeroHom✝ (x * y) = ZeroHom.toFun toZeroHom✝ x * ZeroHom.toFun toZeroHom✝ y
h :
  (fun f => f.toFun) { toZeroHom := toZeroHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toZeroHom := toZeroHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ ↑toZeroHom✝¹ = ↑toZeroHom✝
[PROOFSTEP]
exact h
[GOAL]
α β : GroupWithZeroCat
e : ↑α ≃* ↑β
⊢ ↑e ≫ ↑(MulEquiv.symm e) = 𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : GroupWithZeroCat
e : ↑α ≃* ↑β
x✝ : (forget GroupWithZeroCat).obj α
⊢ ↑(↑e ≫ ↑(MulEquiv.symm e)) x✝ = ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : GroupWithZeroCat
e : ↑α ≃* ↑β
⊢ ↑(MulEquiv.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : GroupWithZeroCat
e : ↑α ≃* ↑β
x✝ : (forget GroupWithZeroCat).obj β
⊢ ↑(↑(MulEquiv.symm e) ≫ ↑e) x✝ = ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
