Set membership

Stream: new members

[Anders Skovsted Buch]

How can I get rid of "sorry"? Figured it out.

import tactic

example : 4 ∈ { n : ℕ | n < 10 ∧ n < 10} :=
begin
  split; linarith,
end

example : 4 ∈ { n : ℕ | n < 10} :=
begin
  -- sorry,
  have : 4 < 10, linarith,
  exact this,
end

[Kevin Buzzard]

Do you understand how the previous proof worked?

[Kyle Miller]

It might help to see what's going on if you reduce the definitions first. I haven't checked, dsimp might work for this as a first tactic in each example.

[Anders Skovsted Buch]

Thanks! This helped:

#reduce 4 ∈ {n : ℕ | n < 10}