proof

Stream: general

[Jane]

Does anyone know how to write the proof of (∩ i, D i) ∪ (∩ i, E i) ⊆ ∩ i, (D i ∪ E i) in lean??

[Kenny Lau]

can you write the theorem in lean and use sorry for the proof and then post the code here?

[Jane]

I am in a math class of this lol

[Jane]

This is the first time I use this chat room, nice to meet you btw. How can I post it here?
like this?
example : (∩ i, D i) ∪ (∩ i, E i) ⊆ ∩ i, (D i ∪ E i) :=
sorry

[Kenny Lau]

that would be closer, but it wouldn't compile because you have not specified the types of D and E

[Patrick Massot]

You need to surround your code with ```lean  and ``` 

[Jane]

variables {U I : Type}
variables D E : I → set U
example : (∩ i, D i) ∪ (∩ i, E i) ⊆ ∩ i, (D i ∪ E i) :=
    assume x,
    assume h: x ∈ (∩ i, D i) ∪ (∩ i, E i),
    or.elim h (sorry)(sorry)

This is what I got so far.

[Patrick Massot]

Is that accepted by Lean?

[Patrick Massot]

The intersection symbols don't look right.

[Sebastien Gouezel]

Non-pedagogic answer:

open set

lemma zou (C D : E → set F) :
  (⋂ i, C i) ∪ (⋂ i, D i) ⊆ (⋂ i, C i ∪ D i) :=
union_subset (Inter_subset_Inter (λ i, subset_union_left _ _)) (Inter_subset_Inter (λ i, subset_union_right _ _))

[Patrick Massot]

Sébastien intersections look right.

[Jane]

I have no clue. our teacher uses cocalc

[Mario Carneiro]

use copy paste

[Patrick Massot]

Sébastien, do you mean this lemma is not in mathlib?

[Mario Carneiro]

are you using cocalc, or do you have a local installation? In either case, lean should give you an error if you use the wrong intersection symbol

[Patrick Massot]

This is shocking

[Mario Carneiro]

I'm not that shocked that this lemma is not available, but it wouldn't hurt to add it

[Mario Carneiro]

probably finish can handle it

[Jane]

It says "unexpected token" what does that suppose to mean?

[Mario Carneiro]

that means you used the wrong symbol

[Jane]

oh, but I copy the lemma you post here, I am so frustrated

[Mario Carneiro]

The problem is that ∩ is the binary intersection symbol, and ⋂ is the "big" intersection

[Mario Carneiro]

which is for doing indexed intersection

[Patrick Massot]

example (U : Type) (I : Type) (D E : I → set U) :
 (⋂ i, D i) ∪ (⋂ i, E i) ⊆ ⋂ i, (D i ∪ E i) :=
begin
  intros x,
  finish
end

does work

[Kenny Lau]

non-pedagogical answer 2:

import data.set.lattice

variables {U I : Type}
variables D E : I → set U
example : (⋂ i, D i) ∪ (⋂ i, E i) ⊆ ⋂ i, (D i ∪ E i) :=
by rintros x (hx | hx) _ ⟨i, rfl⟩; [left, right]; exact hx _ ⟨i, rfl⟩

[Patrick Massot]

It's a bit unfortunate that broken syntax highlighting flags that big intersection symbol

[Johan Commelin]

@Jane Aside: Who is the teacher?

[Sebastien Gouezel]

finish does not kill it. Is is not in mathlib (at least, it is not found by library_search). And I am not really surprised it is not there, as it is not that common or useful -- I mean, if it is not in mathlib it means that noone has needed it until now.

[Jane]

Paige N? I am in the Ohio State

[Mario Carneiro]

oh hey, my alma mater

[Mario Carneiro]

they are doing lean now?

[Patrick Massot]

finish kills it after intro x

[Sebastien Gouezel]

Yes indeed.

[Jane]

whaaaaaat is going on now?? I am so lost.

[Patrick Massot]

Let me try a semi-pedagogical one:

import data.set

set_option pp.beta true

example (U : Type) (I : Type) (D E : I → set U) :
 (⋂ i, D i) ∪ (⋂ i, E i) ⊆ ⋂ i, (D i ∪ E i) :=
begin
  intros x h,
  rintro _ ⟨i, rfl⟩,
  cases h with hl hr,
  left,
  finish,
  right,
  finish,
end

[Patrick Massot]

At least you can follow the main steps of the proof.

[Patrick Massot]

but I guess the rintro line looks pretty mysterious

[Mario Carneiro]

maybe use simp there

[Kenny Lau]

non-pedagogical one 3:

import data.set.lattice

open lattice

variables {U I : Type}
variables D E : I → set U
example : (⋂ i, D i) ∪ (⋂ i, E i) ⊆ ⋂ i, (D i ∪ E i) :=
show (⨅ i, D i) ⊔ (⨅ i, E i) ≤ ⨅ i, (D i ⊔ E i),
from le_infi $ λ i, sup_le_sup (infi_le D i) (infi_le E i)

[Patrick Massot]

Yes, simp, intro i is better than rintro dark magic

[Kenny Lau]

I don't see what's wrong with Sébastien's proof

[Patrick Massot]

Where is that "lattices for the win" emoji again?

[Kenny Lau]

it's perfectly reasonable and it flows from the theorem

[Mario Carneiro]

I think your proof 3 is the same as Sebastien's first proof

[Kenny Lau]

all proofs are equal

[Patrick Massot]

It's the same after recasting in lattices terms

[Mario Carneiro]

do you actually need the show?

[Patrick Massot]

Probably not.

[Jane]

OMG thank you guys very much although I am confused about it

[Mario Carneiro]

lol there are too many non pedagogical proofs floating around now

[Patrick Massot]

Sorry it turned into an expert discussion pretty quickly

[Jane]

Just being curious, where do people use lean??

[Mario Carneiro]

on their computers?

[Jane]

like in which area??

[Jane]

pure math?

[Mario Carneiro]

what area are you in?

[Jane]

Biology lol

[Kenny Lau]

finally, in the style of Jane's attempt:

import data.set.lattice

variables {U I : Type}
variables D E : I → set U
example : (⋂ i, D i) ∪ (⋂ i, E i) ⊆ ⋂ i, (D i ∪ E i) :=
assume x : U,
assume h : x ∈ (⋂ i, D i) ∪ (⋂ i, E i),
or.elim h
  (assume hd : x ∈ ⋂ i, D i,
    set.mem_Inter_of_mem $ assume i : I, or.inl (set.mem_Inter.1 hd i))
  (assume he : x ∈ ⋂ i, E i,
    set.mem_Inter_of_mem $ assume i : I, or.inr (set.mem_Inter.1 he i))

[Mario Carneiro]

formal math sits somewhere between pure math, computer science and logic

[Kenny Lau]

and biology

[Mario Carneiro]

that's a nice pedagogical proof kenny

[Jane]

Thank you guys so much

[Mario Carneiro]

although maybe the tactic folks won't like it

[Jane]

do any of you know Dr. Paige North??

[Mario Carneiro]

I don't think she has appeared here, and I don't think I met her in undergrad either. Is she in biology?

[Patrick Massot]

https://paigenorth.github.io/

[Patrick Massot]

Doesn't sounds like biology to me

[Jane]

I am in math-bio track and ecology double major now.

[Mario Carneiro]

Oh, she does HoTT

[Jane]

Hey sorry to bother you guys' Monday night, here comes another problem. I really don't know how to do this.

variables A B C : set U
variables D E F: I → set U
variable u : U
example : (A ⊆ B) ↔ (powerset A) ⊆ (powerset B) :=
sorry

this looks so obvious but none of my friends know how to do it....

[Johan Commelin]

@Jane I would start with

begin
  split,
  { intros h s hs,
    sorry },
  { intros h x hx,
    sorry }
end

[Johan Commelin]

See if that helps...