subset member

Stream: new members

[Iocta]

import measure_theory.measure_space

open measure_theory measure_theory.measure_space classical

noncomputable theory

variable Ω   : Type

lemma mem_subset (a b : set Ω) (hab: a ⊂ b) (x : Ω) (hx : x ∈ a) : x ∈ b :=
begin

end

tactic failed, there are unsolved goals
state:
Ω : Type,
a b : set Ω,
hab : a ⊂ b,
x : Ω,
hx : x ∈ a
⊢ x ∈ b

[Iocta]

I was expecting library_search to work here

[Kevin Buzzard]

It's two steps. First rw ssubset_iff_subset_ne and then you're done by definition.

[Kevin Buzzard]

I found this by noting that ⊂ was called ssubset (by hovering over it), then searching for ssubset in data.set.basic. Then you can see all the API for this symbol. You know it's not the same as ⊆ right?

[Iocta]

I tried changing it to \subseteq,

lemma mem_subset (a b : set Ω) (hab: a ⊆ b) (x : Ω) (hx : x ∈ a) : x ∈ b :=
begin
library_search,
end

which says Try this: exact hab x hx, and when I click that it says

type mismatch at application
  hab x
term
  x
has type
  Ω : Type
but is expected to have type
  ?m_1 ∈ a : Prop
state:
Ω : Type,
a b : set Ω,
hab : a ⊆ b,
x : Ω,
hx : x ∈ a
⊢ x ∈ b

[Iocta]

I guess it means exact @hab x hx which works

[Bryan Gin-ge Chen]

Yeah, Lean 3's pretty printer sometimes gives bad suggestions, see also #5659 and lean#394.

[Iocta]

It's been a few months since I was in here; am I supposed to be on lean 4 now?

[Bryan Gin-ge Chen]

If you're curious, it's not too hard to play around with now (see the manual) and the videos from Lean Together 2021, but it's going to be many months before mathlib is ported to Lean 4.

[Iocta]

ok I'll stick with 3 then