Proving that a structure is an `add_comm_group`

Stream: general

[Youjack]

Suppose I have a structure

structure mystruct :=
(a : ℝ)
(b : ℝ)

Is there an easy way to prove this?

instance : add_comm_group mystruct := sorry

I know that there is a prod.add_comm_group in mathlib, but I don't know how to apply this to mystruct.
Maybe I should use prod ℝ ℝ instead of mystruct, but I would like to extends mystruct later, so I prefer using structure.

[Kyle Miller]

For what it's worth, docs#prod is a structure that you can extend.

[Kyle Miller]

Regarding defining an add_comm_group structure on mystruct using an equivalence mystruct ≃ prod ℝ ℝ, I thought that mathlib had a way to transfer such a structure over an equivalence but I can't find it at the moment.

[Yaël Dillies]

Write the obvious function mystruct → ℝ × ℝ then show it's injective and finally use docs#function.injective.add_comm_group.

[Jireh Loreaux]

Note: you have to define all the data fields first.

[Yaël Dillies]

Alternatively, use tactic#equiv_rw.

[Notification Bot]

Youjack has marked this topic as resolved.

[Notification Bot]

Youjack has marked this topic as unresolved.

[Youjack]

I make it with equiv.add_comm_group

import data.real.basic
import logic.equiv.transfer_instance

structure mystruct :=
(a : ℝ)
(b : ℝ)

def mystruct_equiv_prod : mystruct ≃ (ℝ × ℝ) := {
  to_fun  := λ s, (s.a, s.b),
  inv_fun := λ p, ⟨p.1, p.2⟩,
  left_inv  := λ s, match s with | ⟨_,_⟩ := rfl end,
  right_inv := λ _, prod.mk.eta
}

instance : add_comm_group mystruct :=
  @equiv.add_comm_group _ _ mystruct_equiv_prod prod.add_comm_group

example (s1 s2 : mystruct) : (s1 + s2).a = s1.a + s2.a := rfl

Thank you all!