Improving group proof

Stream: new members

[Kristaps Balodis]

I managed to show group homomorphisms send 1 to 1, and shortened this proof from what I originally had. I'm sure that this does not abide by "best practices", so I'm wondering what a "better" proof of this might look like.

import Mathlib.Deprecated.Subgroup

theorem redux_two [Group G] [Group H] (f : G → H)
(hom : ∀ a b, f ( a * b) = (f a) * (f b) )
: f (1) = 1 := by
have one_eff : 1 = f 1 := by simpa using congrArg ((f 1)⁻¹  * · ) (hom 1 1)
rw [← one_eff]

[Kristaps Balodis]

Right after posting the above, I figured out I could shorten it further to

theorem redux_three [Group G] [Group H] (f : G → H)
(hom : ∀ a b, f ( a * b) = (f a) * (f b) )
: 1 = f 1 :=
by simpa using congrArg ((f 1)⁻¹  * · ) (hom 1 1)

but I still suspect there's a better way to do this that's more in line with the community standards

[Thomas Browning]

Does by simpa using hom 1 1 not work?

[Kristaps Balodis]

It did, thanks.