Minimal example for struggling to show that some object mappings are inverses.

iso_test.lean

import algebra.group_with_zero
import data.equiv.mul_add

universe u

variables {S : Type*}

--We're going to show the 1-to-1 correspondence between groups (with additive notation)
--and groups_with_zero (with multiplicative notation). To make the mapping less trivial,
--we'll also use the opposite group: so a+b becomes b*a.

--First define how we multiply (with zero) from elements in an additive group.
--The operation:
def g₀_add_op [add_group S]: option S → option S → option S
| none _ := none
| _ none := none
| (some a) (some b) := some (b+a)

--The actual map:
def convert_g_into_g₀_op (g : add_group S) : group_with_zero (option S) := {
  mul := g₀_add_op,
  inv := begin intro a, cases a, exact none, exact some (-a) end,
  zero := none,
  one := some 0,
  mul_assoc := begin intros, cases a; cases b; cases c; simp [g₀_add_op], exact (add_assoc c b a).symm end,
  one_mul := begin intro, cases a; simp [g₀_add_op] end,
  mul_one := begin intro, cases a; simp [g₀_add_op] end,
  zero_mul := begin intro, cases a; simp [g₀_add_op] end,
  mul_zero := begin intro, cases a; simp [g₀_add_op] end,
  exists_pair_ne := ⟨none, some 0, by simp⟩,
  inv_zero := sorry, mul_inv_cancel := sorry
}

--Then the map from a group with zero back to an additive group defined on the units:
def convert_g₀_into_g_op (g0 : group_with_zero S) : add_group (units S) := {
  add := λ a b, b*a,
  neg := λ a, a⁻¹,
  zero := 1,
  add_assoc := begin intros, simp, exact (mul_assoc c b a).symm end,
  zero_add := by simp,
  add_zero := by simp,
  add_left_neg := sorry
}

--The syntax below is what's wrong and where I'm stuck.
--I want to show that convert_g_into_g₀_op and convert_g₀_into_g_op are inverses,
--in the sense that
--   convert_g_into_g₀_op (convert_g₀_into_g_op G) ≃* G
--for any group_with_zero G, and that
--   convert_g₀_into_g_op (convert_g_into_g₀_op G) ≃+ G
--for any add_group G.

def group_gzero_iso [g : add_group S]: convert_g₀_into_g_op (convert_g_into_g₀_op g) ≃+ g :=
begin
  sorry
end

def gzero_group_iso [g0 : group_with_zero S]: convert_g_into_g₀_op (convert_g₀_into_g_op g0) ≃* g0 :=
begin
  sorry
end

Found a good solution! Add

@[ancestor add_equiv]
structure add_equiv_with_structure {M N : Type*} {child : Type u → Type u}
  (cM : child M) (cN : child N) [hM : has_add M] [hN : has_add N]  extends M ≃+ N

@[ancestor mul_equiv, to_additive]
structure mul_equiv_with_structure {M N : Type*} {child : Type u → Type u}
  (cM : child M) (cN : child N) [hM : has_mul M] [hN : has_mul N] extends M ≃* N

infix ` ≃*' `:25 := mul_equiv_with_structure
infix ` ≃+' `:25 := add_equiv_with_structure

and then one can just write

def group_gzero_iso [g : add_group S]: convert_g₀_into_g_op (convert_g_into_g₀_op g) ≃+' g := sorry

with the extra apostrophe in ≃+'. The "child" lets it accept the group S, but then infer the has_mul S structure from that group, and turn that into a mul_equiv with no apostrophe.