Lucienne Felix

Stream: new members

[Yagub Aliyev]

I am trying to formalize some theorems from Lucienne Felix's book "Elementarmathematik
in moderner Darstellung". I think what I learned from Set Theory Game and Formaloversum should be enough for this. Somehow Lean doesn't show me my progress. How do you setup a proof like this?

import Mathlib.Tactic.Have
import Mathlib.Tactic.ByContra
import Mathlib.Tactic.Cases
import Mathlib.Tactic.ApplyAt

theorem lfelix' (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
intro x h
rw[inter_def]

[Ruben Van de Velde]

It seems to choke on the \^c, not sure what you need to make that so work

[Riccardo Brasca]

This

import Mathlib

theorem lfelix' {U : Type*} (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
intro x h
rw[inter_def]

works (except that inter_def does not exists). I think something is needed to use the notation.

[Yakov Pechersky]

docs#Set.inter_def or open Set

[Riccardo Brasca]

Also import Mathlib.Tactic is enough.

[Yakov Pechersky]

but I think the right thing is Set.mem_inter or Set.mem_inter_iff

[Riccardo Brasca]

Yakov Pechersky said:

docs#Set.inter_def or open Set

Yes, of course. The strange problem is that with the imports in the first post there is an error about the notation Cᶜ.

[Riccardo Brasca]

I mean that this

import Mathlib.Tactic.Have
import Mathlib.Tactic.ByContra
import Mathlib.Tactic.Cases
import Mathlib.Tactic.ApplyAt

theorem lfelix' {U : Type*} (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
  sorry

gives an error.

[Yakov Pechersky]

Needs Mathlib.Order.Notation

[Yakov Pechersky]

Does that import come in via the mentioned tactics?

[Yakov Pechersky]

Those tactics look really basic, such that they wouldn't pull in set definitional API

[Riccardo Brasca]

Ah yes, it needs Mathlib.Data.Set.Defs.

[Riccardo Brasca]

I totally forgot that ᶜ is not notation for Set.compl, but it is obtained via the class HasCompl.

[Riccardo Brasca]

@Yagub Aliyev the short answer to your question is: to use the ᶜ just add import Mathlib.Data.Set.Defs.

[Riccardo Brasca]

In general don't try to minimize so much the imports. import Mathlib.Tactic is probably a good trade off.

[Ruben Van de Velde]

(I find the choice to use foo_def for what mathlib calls mem_foo in the set theory game odd)

[Dan Velleman]

@Yagub Aliyev The tactics used in the set theory game are all standard tactics, but there are a some theorems defined in the set theory game that you can't use outside of that game. inter_def is one of them.

[Yagub Aliyev]

Thank you! I completed with your help.

import Mathlib.Tactic
import Mathlib.Data.Set.Defs

theorem lfelix' (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
intro x h
rw[Set.mem_inter_iff] at h
have hA : x ∈ A := h.left
have hB : x ∈ B := h.right
have h0 : x ∈ C ∨ x ∈ Cᶜ
rw[← Set.mem_union]
rw[Set.union_compl_self]
tauto
cases' h0 with h5 h6
left
rw[Set.mem_inter_iff]
constructor
exact hA
exact h5
right
constructor
exact hB
exact h6

[Yagub Aliyev]

How do you save it or keep for further reference? Will this stay in Zulip forever? How do you include it in mathlib if it is useful?

[Yagub Aliyev]

Also I find it interesting that the following works, too

 import Mathlib.Tactic
import Mathlib.Data.Set.Defs

theorem lfelix' (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
intro x h
rw[Set.mem_inter_iff] at h
have hA : x ∈ A := h.left
have hB : x ∈ B := h.right
have h0 : x ∈ C ∨ x ∈ Cᶜ
rw[← Set.mem_union]
rw[Set.union_compl_self]
tauto
tauto

but the following doesn't

import Mathlib.Tactic
import Mathlib.Data.Set.Defs

theorem lfelix' (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
intro x h
tauto

Something in the middle made tauto work but I don't know what.

[Yagub Aliyev]

Dan Velleman said:

Yagub Aliyev The tactics used in the set theory game are all standard tactics, but there are a some theorems defined in the set theory game that you can't use outside of that game. inter_def is one of them.

Maybe the users of the game should be informed about this from the beginning. Some might prefer not to learn the commands that they can't use outside of the game.

[Dan Velleman]

I'll think about this. In some cases there are complications that arise with the standard theorem names that I did't want to have to explain in the set theory game. (For example, in some standard theorems arguments are implicit, in others they are not.) I avoided this issue by using my own system of names. But I can see that there's a disadvantage to that.

[Dan Velleman]

Note that most of the theorems in the set theory game are proven in the game, and become available for use once you have proven them. Those are, of course, not available outside of the game.

[Riccardo Brasca]

Does aesop prove all of them? In mathlib I mean

[Dan Velleman]

Do you mean does aesop prove all of the theorems in the set theory game? Probably many of them, but not all of them. The game is intended for beginners, so the early theorems are quite easy. But by the end there are some hard ones.

[Riccardo Brasca]

Sure, I wasn't suggesting to use it in the game!

[Yagub Aliyev]

I found another solution. Does it deserve to be in Mathlib? What are the criteria? :-)

import Mathlib.Tactic
import Mathlib.Data.Set.Defs

theorem lfelix' (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
rw[← Set.inter_eq_right]
nth_rewrite 1 [Set.inter_comm]
rw[Set.inter_union_distrib_left]
rw[Set.inter_inter_distrib_left]
nth_rewrite 2 [Set.inter_inter_distrib_left]
rw[Set.inter_assoc A B A]
rw[Set.inter_left_comm A B A]
rw[Set.inter_assoc A B B]
rw[Set.inter_self]
rw[Set.inter_self]
rw[Set.inter_comm]
rw[Set.inter_comm B A]
rw[Set.inter_comm (A ∩ B ∩ C) (A ∩ B)]
rw[← Set.inter_union_distrib_left]
rw[← Set.inter_union_distrib_left]
rw[Set.union_compl_self]
rw[Set.inter_univ]
rw[Set.inter_self]

[Kevin Buzzard]

I think that mathlib already has all the useful statements needed to do basic set theory; I suspect that something like this would only be added if someone was working on a more advanced result and discovered that this theorem was needed in order to make progress.

theorem lfelix' (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
  rintro x
  have := em (x ∈ C)
  aesop

[Yagub Aliyev]

Kevin Buzzard said:

I think that mathlib already has all the useful statements needed to do basic set theory; I suspect that something like this would only be added if someone was working on a more advanced result and discovered that this theorem was needed in order to make progress.

theorem lfelix' (A B C: Set U) : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) := by
  rintro x
  have := em (x ∈ C)
  aesop

Thank you! I wonder how to prove this without aesop

import Mathlib.Tactic
import Mathlib.Data.Set.Defs

theorem lfelix3 (A B: Set U) (h: A ⊆ B) : A ∪ B = B := by
sorry

[Kevin Buzzard]

Just prove it yourself using ext?

[Yagub Aliyev]

What does it mean ext?. You also mentioned before exact?
Lean doesn't react when you type this. Should Lean suggest some variant when we type it? I use online version of Lean.

[Kevin Buzzard]

ext is a tactic, just try it as the first line of your proof

[Dan Velleman]

By the way, ext is introduced in the set theory game, Intersection World, level 8