Unfolding the definition of a member of a smul

Stream: Is there code for X?

[Ben]

I have the following

import group_theory.group_action.basic

open_locale pointwise

def even (n: ℕ) : Prop := ∃ d: ℕ, d * 2 = n
example (b: ℕ) (h: b ∈ 2 • set_of even) : 4 ∣ b := begin
  sorry,
end

I have tried writing rw set.mem_smul_set.1 at h but it doesn't work for some reason... any ideas?

[Ruben Van de Velde]

That doesn't seem to have the necessary imports - can you share a #mwe?

[Ben]

ah didn't realise what it needed, have updated message

[Ruben Van de Velde]

And are you sure that means what you think it does?

Pointwise monoids (set, finset, filter) have derived pointwise actions of the form
has_smul α β → has_smul α (set β). When α is ℕ or ℤ, this action conflicts with the
nat or int action coming from set β being a monoid or div_inv_monoid. For example,
2 • {a, b} can both be {2 • a, 2 • b} (pointwise action, pointwise repeated addition,
set.has_smul_set) and {a + a, a + b, b + a, b + b} (nat or int action, repeated pointwise
addition, set.has_nsmul).

Because the pointwise action can easily be spelled out in such cases, we give higher priority to the
nat and int actions.

[Eric Wieser]

As @Ruben Van de Velde suggests, as currently written your lemma is false:

import group_theory.group_action.basic
import tactic.slim_check
import data.nat.parity

open_locale pointwise

example (b: ℕ) (h: b ∈ 2 • {x : ℕ | even x}) : 4 ∣ b := begin
  simp_rw [two_smul, set.mem_add, set.mem_set_of, even] at h,
  obtain ⟨x, y, hx, hy, rfl⟩ := h,
  slim_check,
end

[Eric Wieser]

(note I swapped your even for the builtin even since lean knows how to use slim_check on the latter)

[Eric Wieser]

Here's a true version of your statement:

import group_theory.group_action.basic
import tactic.slim_check

open_locale pointwise

def even (n: ℕ) : Prop := ∃ d: ℕ, d * 2 = n
example (b: ℕ) (h: b ∈ (by haveI : has_smul ℕ (set ℕ) := set.has_smul_set; exact 2 • set_of even)) : 4 ∣ b := begin
  simp_rw [set.mem_smul_set, set.mem_set_of] at h,
  obtain ⟨_, ⟨x, rfl⟩, rfl⟩ := h,
  rw [smul_eq_mul, mul_left_comm],
  norm_num,
end