Zulip Chat Archive

Stream: new members

Topic: subset member


Iocta (Mar 06 2021 at 20:10):

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 (Mar 06 2021 at 20:10):

I was expecting library_search to work here

Kevin Buzzard (Mar 06 2021 at 20:12):

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

Kevin Buzzard (Mar 06 2021 at 20:13):

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 (Mar 06 2021 at 20:23):

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 (Mar 06 2021 at 20:26):

I guess it means exact @hab x hx which works

Bryan Gin-ge Chen (Mar 06 2021 at 20:29):

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

Iocta (Mar 06 2021 at 20:30):

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

Bryan Gin-ge Chen (Mar 06 2021 at 20:32):

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 (Mar 06 2021 at 20:33):

ok I'll stick with 3 then


Last updated: Dec 20 2023 at 11:08 UTC