*lift* a theorem on a type to a subtype?

Stream: Is there code for X?

[Ben]

I have the following subtype and want to show it satisfies associativity of addition. As the definitions of addition are the same for the subtype, is there a better way of expressing lemma even_natural_number.add_assoc?

import tactic

def even_natural_number : Type := @subtype nat (λa, 2 ∣ a)

def even_natural_number.add (a b: even_natural_number) : even_natural_number
  := subtype.mk (nat.add (subtype.val a) (subtype.val b)) (dvd_add a.property b.property)

instance : has_add even_natural_number := ⟨even_natural_number.add⟩

-- Is there a one liner here...?
lemma even_natural_number.add_assoc : ∀a b c: even_natural_number, a + b + c = a + (b + c) := begin
  intros a b c,
  rw subtype.ext_iff,
  exact add_assoc (subtype.val a) (subtype.val b) (subtype.val c),
end

or is this the best way, I could see this failing if addition had a different definition to the base type

[Ben]

Additionally I am bit confused why this only works with the import tactic import. Removing that import and replacing with import algebra.ring.divisibility and import data.subtype causes the inference dvd_add and add_assoc to fail...?

[Eric Wieser]

You likely want docs#function.injective.add_comm_monoid

[Ben]

Ah would that then automatically derive add_comm_monoid for even_natural_number? How would I start that?

def enn_add_is_homo: function.injective.add_comm_monoid even_natural_number.add := {
   -- todo
}

[Eric Wieser]

instance : add_comm_monoid even_natural_number.add :=
function.injective.add_comm_monoid _ subtype.coe_injective _ _ _

or similar

[Ben]

Ah that's cool! so that function effectively generates the structure definition without having to write all the members :mind_blown: