G : Type u_1
g₁ g₂ : Group G
h_mul : Mul.mul = Mul.mul
h₁ : One.one = One.one
f : G →* G := { toOneHom := { toFun := id, map_one' := h₁ }, map_mul' := (_ : ∀ (x y : G), Mul.mul x y = Mul.mul x y) }
⊢ g₁ = g₂
G : Type u_1
g₁ g₂ : Group G
h_mul : Mul.mul = Mul.mul
h₁ : One.one = One.one
⊢ g₁ = g₂
let f : @MonoidHom G G g₁.toMulOneClass g₂.toMulOneClass :=
  @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
    (fun x y => congr_fun (congr_fun h_mul x) y)
no goals
G : Type u_1
g₁ g₂ : Group G
h_mul : Mul.mul = Mul.mul
h₁ : One.one = One.one
f : G →* G := { toOneHom := { toFun := id, map_one' := h₁ }, map_mul' := (_ : ∀ (x y : G), Mul.mul x y = Mul.mul x y) }
⊢ g₁ = g₂
exact
  Group.toDivInvMonoid_injective
    (DivInvMonoid.ext h_mul
      (funext <| @MonoidHom.map_inv G G g₁ g₂.toDivisionMonoid f))