World: Mengenlehre

Stream: new members

[Yagub Aliyev]

https://adam.math.hhu.de/#/g/hhu-adam/robo/world/SetTheory/level/5

If you have as an assumption:
h8: ∃ x, ¬(x ∈ s → x ∈ ∅)
how do you extract that x from the existential quantifier? I want to use that x to get contradiction with
h: ∀ (x : A), x ∉ s

theorem Set.eq_empty_iff_forall_not_mem {A : Type _} (s : Set A) : s = ∅ ↔ ∀ x, x ∉ s := by
constructor
intro h
rw[h]
tauto
intro h
by_contra h0
rw[Subset.antisymm_iff] at h0
rw[not_and_or] at h0
cases' h0 with h8 h9
rw[subset_def] at h8
rw[not_forall] at h8

[Marcus Rossel]

The nice way is have \<x, hx\> := h8, or using obtain instead of have if you have imported Mathlib. (Or you can match/cases on h8 as with any other inductive type.)

[Yagub Aliyev]

Was away from Lean for a week and started to forget some stuff. How do you remember all of these guys? Do you take notes? Google search doesn't seem to be much helpful with Lean.

[Kevin Cheung]

Yagub Aliyev said:

Was away from Lean for a week and started to forget some stuff. How do you remember all of these guys? Do you take notes? Google search doesn't seem to be much helpful with Lean.

I use Loogle and Mathlib documentation search. And a lot of apply? and rw?

[Kevin Buzzard]

It's not hard to learn the 30 or so common tactics in use in lean code doing standard mathematics. It takes practice but it's definitely feasible. It's much harder to learn the 100000 lemmas in mathlib but that's what exact? is for.

[Kevin Cheung]

I also keep a set of examples around.

[Jon Eugster]

I added your solution as a sample solution with a hint at the position you got stuck, @Yagub Aliyev, for future users. I see that level doesn't have barely any hints at all.

I think the game introduced rcases h8 with \<x, hx\> to take all sorts of assumptions appart. Defacto one needs to make a choice between these options, which all do essentially the same:

• rcases
• cases' (I always think of primed tactics as lean3-relicts that are just still around for convenience)
• cases (multiline syntax, doesnt work in the games)
• match (multiline syntax, doesnt work in the games)
• have/obtain (another good option)