Failed transport of structure

transport.lean

import data.equiv.basic
import algebra.ring
variables {α : Type*} {β : Type*} (e : α ≃ β)
include e

@[to_additive has_zero_of_equiv]
def has_one_of_equiv [has_one α] : has_one β := ⟨e 1⟩
@[to_additive has_add_of_equiv]
def has_mul_of_equiv [has_mul α] : has_mul β := ⟨λ x y, e $ (e.symm x) * (e.symm y)⟩

@[to_additive has_neg_of_equiv]
def has_inv_of_equiv [has_inv α] : has_inv β := ⟨λ x, e $ (e.symm x)⁻¹⟩

def monoid_of_equiv [monoid α] : monoid β :=
begin
  refine_struct {..has_one_of_equiv e, ..has_mul_of_equiv e},
  { intros a b c,
    dsimp [has_mul_of_equiv],
    simp [mul_assoc] },
  { intro a,
    change e (e.symm (e 1) * e.symm a) = a,
    simp },
  { intro a,
    change e (e.symm a * e.symm (e 1)) = a,
    simp }
end
attribute [to_additive add_monoid_of_equiv._proof_1] monoid_of_equiv._proof_1
attribute [to_additive add_monoid_of_equiv._proof_2] monoid_of_equiv._proof_2
attribute [to_additive add_monoid_of_equiv._proof_3] monoid_of_equiv._proof_3
attribute [to_additive add_monoid_of_equiv] monoid_of_equiv
attribute [to_additive add_monoid_of_equiv.equations._eqn_1] monoid_of_equiv.equations._eqn_1

@[to_additive of_equiv_add_monoid_hom]
lemma of_equiv_monoid_hom [monoid α] : @is_monoid_hom α β _ (monoid_of_equiv e) e :=
{ map_one := rfl,
  map_mul := λ x y, by change e (x * y) = e(e.symm (e x) * e.symm(e y)); simp }

def comm_monoid_of_equiv [comm_monoid α] : comm_monoid β :=
begin
  refine_struct {..monoid_of_equiv e},
  { intros a b,
    change e (e.symm a * e.symm b) = e (e.symm b * e.symm a),
    rw mul_comm },
end
attribute [to_additive add_comm_monoid_of_equiv._proof_1] comm_monoid_of_equiv._proof_1
attribute [to_additive add_comm_monoid_of_equiv._proof_2] comm_monoid_of_equiv._proof_2
attribute [to_additive add_comm_monoid_of_equiv._proof_3] comm_monoid_of_equiv._proof_3
attribute [to_additive add_comm_monoid_of_equiv._proof_4] comm_monoid_of_equiv._proof_4
attribute [to_additive add_comm_monoid_of_equiv] comm_monoid_of_equiv
attribute [to_additive add_comm_monoid_of_equiv.equations._eqn_1] comm_monoid_of_equiv.equations._eqn_1

def group_of_equiv [group α] : group β :=
begin
  refine_struct {..monoid_of_equiv e, ..has_inv_of_equiv e},
  intro a,
  change e ( e.symm (e ((equiv.symm e) a)⁻¹) * (e.symm a)) = e 1,
  simp,
end
attribute [to_additive add_group_of_equiv._proof_1] group_of_equiv._proof_1
attribute [to_additive add_group_of_equiv._proof_2] group_of_equiv._proof_2
attribute [to_additive add_group_of_equiv._proof_3] group_of_equiv._proof_3
attribute [to_additive add_group_of_equiv._proof_4] group_of_equiv._proof_4
attribute [to_additive add_group_of_equiv] group_of_equiv
attribute [to_additive add_group_of_equiv.equations._eqn_1] group_of_equiv.equations._eqn_1

@[to_additive of_equiv_add_group_hom]
lemma of_equiv_group_hom [group α] : @is_group_hom α β _ (group_of_equiv e) e :=
begin
  constructor,
  intros x y,
  change e (x * y) = e(e.symm (e x) * e.symm(e y)), simp,
end

def comm_group_of_equiv [comm_group α] : comm_group β :=
begin
  -- I could add comm_monoid_of_equiv e but that seems to confuse `to_additive`
  refine_struct {..group_of_equiv e},
  intros a b,
  change e (e.symm a * e.symm b) = e (e.symm b * e.symm a),
  rw mul_comm
end
attribute [to_additive add_comm_group_of_equiv._proof_1] comm_group_of_equiv._proof_1
attribute [to_additive add_comm_group_of_equiv._proof_2] comm_group_of_equiv._proof_2
attribute [to_additive add_comm_group_of_equiv._proof_3] comm_group_of_equiv._proof_3
attribute [to_additive add_comm_group_of_equiv._proof_4] comm_group_of_equiv._proof_4
attribute [to_additive add_comm_group_of_equiv._proof_5] comm_group_of_equiv._proof_5
attribute [to_additive add_comm_group_of_equiv] comm_group_of_equiv
attribute [to_additive add_comm_group_of_equiv.equations._eqn_1] comm_group_of_equiv.equations._eqn_1

def ring_of_equiv [ring α] : ring β :=
begin
  refine_struct {..add_comm_group_of_equiv e, ..monoid_of_equiv e},
  { intros a b c,
    haveI := add_comm_group_of_equiv e,
    apply congr_arg e,
    have h : e.symm (b + c) = e.symm b + e.symm c := (of_equiv_add_group_hom e).add, -- doesn't work
    simp only [h], -- doesn't work even with sorried `h`
    sorry},
end