[GOAL]
α : Type u_1
inst✝ : Group α
x✝ : (WithZero α)ˣ
⊢ ↑((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) ((fun a => unzero (_ : ↑a ≠ 0)) x✝)) = ↑x✝
[PROOFSTEP]
simp only [coe_unzero, Units.mk0_val]
[GOAL]
α : Type u_1
inst✝ : Group α
x✝¹ x✝ : (WithZero α)ˣ
⊢ ↑(Equiv.toFun
        { toFun := fun a => unzero (_ : ↑a ≠ 0), invFun := fun a => Units.mk0 ↑a (_ : ↑a ≠ 0),
          left_inv :=
            (_ : ∀ (x : (WithZero α)ˣ), (fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) ((fun a => unzero (_ : ↑a ≠ 0)) x) = x),
          right_inv :=
            (_ :
              ∀ (x : α),
                (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x) =
                  (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x)) }
        (x✝¹ * x✝)) =
    ↑(Equiv.toFun
          { toFun := fun a => unzero (_ : ↑a ≠ 0), invFun := fun a => Units.mk0 ↑a (_ : ↑a ≠ 0),
            left_inv :=
              (_ : ∀ (x : (WithZero α)ˣ), (fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) ((fun a => unzero (_ : ↑a ≠ 0)) x) = x),
            right_inv :=
              (_ :
                ∀ (x : α),
                  (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x) =
                    (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x)) }
          x✝¹ *
        Equiv.toFun
          { toFun := fun a => unzero (_ : ↑a ≠ 0), invFun := fun a => Units.mk0 ↑a (_ : ↑a ≠ 0),
            left_inv :=
              (_ : ∀ (x : (WithZero α)ˣ), (fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) ((fun a => unzero (_ : ↑a ≠ 0)) x) = x),
            right_inv :=
              (_ :
                ∀ (x : α),
                  (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x) =
                    (fun a => unzero (_ : ↑a ≠ 0)) ((fun a => Units.mk0 ↑a (_ : ↑a ≠ 0)) x)) }
          x✝)
[PROOFSTEP]
simp only [Units.val_mul, coe_unzero, coe_mul]
