# Zulip Chat Archive

## Stream: new members

### Topic: letter

#### Kevin Buzzard (Aug 14 2020 at 08:39):

@Iocta `rfl`

doesn't mean "it's obvious", it means "equality is reflexive" ie it proves X=X. Your goal is something like `true or P or Q or R`

#### Iocta (Aug 14 2020 at 08:48):

Got most of the way through it. How to fill the `sorry`

?

```
import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum
open set filter topological_space measure_theory
section e2_7_1
@[derive decidable_eq]
inductive letter : Type
| a : letter
| b : letter
| c : letter
| d : letter
namespace letter
instance fintype: fintype letter :=
{elems := {a, b, c, d}, complete := λ x, by cases x; simp}
@[simp]
lemma univ_letter : @finset.univ letter letter.fintype = {a, b, c, d} := rfl
def f1 : set (set letter) := {{}, {a, b}, {c, d}, {a,b,c,d}}
example : measurable_space letter := {
is_measurable := (λ s, s ∈ f1),
is_measurable_empty := by {
rw f1,
rw mem_insert_iff,
left,
simp only [eq_self_iff_true],
},
is_measurable_compl := by {
intros s h,
cases h,
{
rw f1,
simp,
right,
right,
right,
simp *,
ext1,
split,
{
intro h,
unfold univ at *,
simp * at *,
cases h,
cases x; finish,
},
intro h,
finish,
},
{
rw f1,
simp * at *,
cases h,
{
right,
right,
left,
simp * at *,
ext1,
split,
{
intro h',
simp * at *,
cases x; finish,
},
{
intro h',
cases x; finish,
},
},
cases h,
{
right,
left,
ext1,
split,
{ intro h', simp * at h', cases x; finish, },
{ intro h',
cases x; finish,
},
},
{
left,
ext1,
split,
{
intro h',
cases x; finish,
},
{
intro h',
cases x; finish,
}
},
},
},
is_measurable_Union := by {
intros s h,
simp * at *,
rw f1 at *,
/-
s : ℕ → set letter,
h : ∀ (i : ℕ), s i ∈ {∅, {a, b}, {c, d}, {a, b, c, d}}
⊢ Union s ∈ {∅, {a, b}, {c, d}, {a, b, c, d}}
-/
sorry,
}
}
end letter
end e2_7_1
```

#### Iocta (Aug 14 2020 at 08:53):

I'm never sure when I need to be thinking about how to do the math vs knowing about tactics/lemmas in mathlib. I guess this will come with experience.

#### Chris Wong (Aug 14 2020 at 08:55):

`suggest`

or `library_search`

might help here

#### Iocta (Aug 14 2020 at 08:57):

Those don't give me anything; for some reason my computer seems to be struggling with this example, maybe they timed out sooner than they shouldve

#### Scott Morrison (Aug 14 2020 at 09:12):

What would your maths argument be? Maybe write it out here in gory detail. A possible hint would be to look at the `fin_cases`

tactic, but you'll need to do some preparatory work before it's useful.

#### Kevin Buzzard (Aug 14 2020 at 09:38):

Yeah I echo Scott's comment. You might think this is "obvious" -- but what is the actual proof?

#### Chris Wong (Aug 14 2020 at 09:40):

Ooh, I see. So I guess we have to iterate over every possible union, and check that it's valid? That would explain why it isn't just a `library_search`

away.

#### Kevin Buzzard (Aug 14 2020 at 09:59):

And these are arbitrary possibly infinite unions

#### Scott Morrison (Aug 14 2020 at 10:18):

Since each `s i`

lives in some finite set, you might make an argument about the image of `s`

(which is some set of sets of letters).

#### Scott Morrison (Aug 14 2020 at 10:18):

Then do a case bash

#### Scott Morrison (Aug 14 2020 at 10:18):

(possibly with `fin_cases`

)

#### Iocta (Aug 15 2020 at 02:47):

I think this is in the direction described, but dunno how to fill it.

```
example : ∀ (f : ℕ → set letter), (∀ (i : ℕ), f i ∈ f1) → (⋃ (i : ℕ), f i) ∈ f1 :=
begin
intros f h,
rw f1 at *,
let im_f : (set (set letter)) := {q : set letter | ∃ i : ℕ, q = f i},
let sets : set (set letter) := {∅, {a, b}, {c, d}, {a, b, c, d}},
have imf2sets: ∀ (s: set letter), s ∈ im_f → s ∈ sets,
{
intros s hs,
simp at hs,
cases hs with i hi,
specialize h i,
rw hi,
exact h,
},
suffices: (⋃ (i : ℕ), f i) ∈ sets, { exact this, },
have uclosed_imf: (⋃ (i : ℕ), f i) ∈ im_f,
{
sorry,
},
exact imf2sets (⋃ (i : ℕ), f i) uclosed_imf,
```

#### Iocta (Aug 15 2020 at 05:47):

```
structure alg (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(closed_complements : ∀ s ∈ σ, sᶜ ∈ σ)
(closed_finite_unions : ∀ f : ℕ → set Ω, ∃ n : ℕ, (∀ i : ℕ, (f i) ∈ σ) → (⋃ i ≤ n, f i) ∈ σ)
```

this restricts the last line of `measurable_space`

to only finite unions. Is that the right expression for closed finite unions?

#### Chris Wong (Aug 15 2020 at 05:56):

Your `closed_countable_unions`

seems to be about finite unions, not countable ones?

#### Iocta (Aug 15 2020 at 05:56):

heh yeah that's what I meant

#### Iocta (Aug 15 2020 at 05:58):

[edited it to avoid confusion]

#### Chris Wong (Aug 15 2020 at 06:00):

If you only care about finite unions, then I think the statement can be simplified to `union`

(small u) of two sets

#### Iocta (Aug 15 2020 at 06:04):

oh that sounds true

#### Iocta (Aug 15 2020 at 08:11):

How to interpret the definition of `hr`

?

```
universe u
variable {α : Type u}
structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(closed_complements : ∀ s ∈ σ, sᶜ ∈ σ)
(closed_finite_unions (a b ∈ σ ): a ∪ b ∈ σ)
example (s : set (set α )) (a b: set α) (ha: a ∈ s) (hb : b ∈ s) (h: a ∩ bᶜ ∈ s) : algebra' α := {
σ := (λx, x ∈ s),
univ_mem := by {
sorry,
},
closed_complements := by {
intros r hr,
-- α: Type u
-- s: set (set α)
-- ab: set α
-- ha: a ∈ s
-- hb: b ∈ s
-- h: a ∩ bᶜ ∈ s
-- r: set α
-- hr: r ∈ λ (x : set α), x ∈ s
-- ⊢ rᶜ ∈ λ (x : set α), x ∈ s
},
closed_finite_unions := _ }
```

#### Kenny Lau (Aug 15 2020 at 08:12):

`set X`

is implemented as `X \r Prop`

#### Iocta (Aug 15 2020 at 08:12):

is that "proof that r is in the set of functions from sets x of alpha to proof that x is in s"?

#### Kenny Lau (Aug 15 2020 at 08:12):

so `\lambda x : x \in s`

is really `{ x | x \in s }`

#### Kenny Lau (Aug 15 2020 at 08:12):

so `hr`

is really saying `r \in s`

#### Kenny Lau (Aug 15 2020 at 08:13):

that's what happens if you use the `X \r Prop`

implementation to write `\sigma`

#### Kenny Lau (Aug 15 2020 at 08:13):

`σ := (λx, x ∈ s)`

#### Kenny Lau (Aug 15 2020 at 08:13):

instead of `σ := { x | x ∈ s }`

#### Kenny Lau (Aug 15 2020 at 08:14):

I don't think your hypothesis is saying what you want it to say either

#### Kenny Lau (Aug 15 2020 at 08:14):

you want to say that for all `a b \in s`

we have `a \cap b\^c \in s`

#### Iocta (Aug 15 2020 at 08:14):

I have a feeling there's something wrong with the quantifiers

#### Kenny Lau (Aug 15 2020 at 08:14):

not just for a specific `a`

and `b`

#### Iocta (Aug 15 2020 at 08:14):

yeah exactly

#### Kenny Lau (Aug 15 2020 at 08:15):

and instead of `σ := { x | x ∈ s }`

you should just write `σ := s`

#### Iocta (Aug 15 2020 at 08:15):

but I thought I could always put hypotheses on the left of the : instead of \foralling them

#### Kenny Lau (Aug 15 2020 at 08:15):

you're bracketing wrong

#### Iocta (Aug 15 2020 at 08:15):

okay I'll start over

#### Kenny Lau (Aug 15 2020 at 08:16):

`\forall a, a = a`

is the same as `(a) : a = a`

#### Kenny Lau (Aug 15 2020 at 08:16):

but `(\forall a, a = a) \to b`

is not the same as `(a) (h : a = a) : b`

#### Kenny Lau (Aug 15 2020 at 08:16):

that's what it means that forall can be replaced with colon

#### Iocta (Aug 15 2020 at 09:48):

This seems to work. I have some questions about improvements. Can I use `closed_complements`

in `closed_finite_unions`

? Currently I'm proving the same thing twice. Or can I pull it into an internal lemma to be used in both places?

```
import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum
import tactic.fin_cases
import data.set.basic
open set filter topological_space measure_theory
universe u
variable {α : Type u}
structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(closed_complements : ∀ s ∈ σ, sᶜ ∈ σ)
(closed_finite_unions (a b ∈ σ ): a ∪ b ∈ σ)
@[simp]
lemma compl_iff {x y : set α } : x = yᶜ ↔ xᶜ = y :=
begin
split,
{
intro h,
finish,
},
{
intro h,
ext1,
split; { intro h', finish },
}
end
lemma compl_inter_compl_eq_union (x y : set α ): (xᶜ ∩ yᶜ)ᶜ = x ∪ y :=
begin
have: (xᶜ ∩ yᶜ) = (x ∪ y)ᶜ, { simp only [compl_union], },
rw ← @compl_iff α (xᶜ ∩ yᶜ) (x ∪ y) ,
exact this,
end
example (s: set (set α )) (hs: set.univ ∈ s) (h: ∀ a b ∈ s, a ∩ bᶜ ∈ s) : algebra' α := {
σ := s,
univ_mem := hs,
closed_complements := by {
intros z hz,
specialize h set.univ z hs hz,
rw univ_inter at h,
exact h,
},
closed_finite_unions := by {
have cc: ∀ x ∈ s, xᶜ ∈ s, {
intros z hz,
specialize h set.univ z hs hz,
rw univ_inter at h,
exact h,
},
intros x y hx hy,
have hxc: xᶜ ∈ s, { apply cc x hx, },
have hyc: yᶜ ∈ s, { apply cc y hy},
have: xᶜ ∩ yᶜ ∈ s, { specialize h xᶜ y hxc hy , exact h},
have hc: (xᶜ ∩ yᶜ)ᶜ ∈ s, { apply cc (xᶜ ∩ yᶜ ) this},
have : (xᶜ ∩ yᶜ)ᶜ = x ∪ y, { apply compl_inter_compl_eq_union },
simp * at *,
}
}
```

#### Iocta (Aug 15 2020 at 10:00):

Also, there's gotta be an easier way to do those De Morgan-like lemmas, right?

#### Chris Wong (Aug 15 2020 at 12:08):

```
lemma compl_inter_compl (x y : set α) : (xᶜ ∩ yᶜ)ᶜ = x ∪ y :=
by simp only [compl_inter, compl_compl]
```

#### Chris Wong (Aug 15 2020 at 13:14):

```
example (s : set (set α)) (hs : set.univ ∈ s) (h : ∀ a b ∈ s, a ∩ bᶜ ∈ s) : algebra' α :=
have closed_complements : ∀ z ∈ s, zᶜ ∈ s :=
begin
intros z hz,
specialize h set.univ z hs hz,
rw univ_inter zᶜ at h,
exact h,
end,
{ σ := s,
univ_mem := hs,
closed_complements := closed_complements,
closed_finite_unions :=
begin
intros a b ha hb,
have hab : aᶜ ∩ bᶜ ∈ s := h _ _ (closed_complements _ ha) hb,
rw ← compl_union at hab,
rw ← compl_compl (a ∪ b),
apply closed_complements,
exact hab,
end }
```

#### Chris Wong (Aug 15 2020 at 13:35):

I'm using `have`

to share the `closed_complements`

proof – I haven't worked with structures much yet so I don't know if there's a better way

#### Kenny Lau (Aug 15 2020 at 17:16):

Iocta said:

Also, there's gotta be an easier way to do those De Morgan-like lemmas, right?

the canonical way to solve any 0th order logic (i.e. propositional logic) goal is `finish`

#### Iocta (Aug 15 2020 at 18:11):

Why doesn't `lemma compl_inter_compl_eq_union' (x y : set α ): (xᶜ ∩ yᶜ)ᶜ = x ∪ y := by finish`

work?

#### Kevin Buzzard (Aug 15 2020 at 18:15):

```
import tactic
variable (α : Type)
example (x y : set α ): (xᶜ ∩ yᶜ)ᶜ = x ∪ y :=
begin
ext,
finish
end
```

#### Kenny Lau (Aug 15 2020 at 18:25):

because it isn't a 0th order logic goal

#### Iocta (Aug 15 2020 at 21:53):

```
universe u
variable {α : Type u}
variables (s: set (set α)) (hs: set.univ ∈ s)
structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(closed_complements : ∀ s ∈ σ, sᶜ ∈ σ)
(closed_finite_unions (a b ∈ σ ): a ∪ b ∈ σ)
example (h : algebra' α) : set.univ ∈ s :=
begin
sorry,
end
```

How do I use the `univ_mem`

from the structure definition?

#### Kenny Lau (Aug 15 2020 at 21:56):

`h.univ_mem`

#### Kenny Lau (Aug 15 2020 at 21:56):

again I think that isn't what you meant

#### Kenny Lau (Aug 15 2020 at 21:57):

`h`

is some algebra structure on `\alpha`

that has nothing to do with `s`

#### Kenny Lau (Aug 15 2020 at 21:57):

the underlying set of `h`

is `h.\sigma`

#### Iocta (Aug 15 2020 at 22:08):

Like this I guess

```
example (a : algebra' α) : set.univ ∈ a.σ := a.univ_mem
```

#### Kenny Lau (Aug 15 2020 at 22:12):

yes that's right

#### Iocta (Aug 15 2020 at 22:25):

I don't totally get it. What do I mean here?

```
structure semialgebra (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(empty_mem : {} ∈ σ )
(semi_closed_complements : ∀ s ∈ σ, ∃ f : ℕ → set Ω, ∃ n : ℕ, (∀ i : ℕ, (f i) ∈ σ) → (⋃ i ≤ n, f i) = sᶜ)
example (a: algebra' α) : semialgebra a.σ := {
σ := _,
univ_mem := _,
empty_mem := _,
semi_closed_complements := _ }
```

#### Iocta (Aug 15 2020 at 22:34):

Oh maybe this

```
example (a: algebra' α) : semialgebra α := {
σ := a.σ,
univ_mem := a.univ_mem,
empty_mem := _,
semi_closed_complements := _ }
```

#### Iocta (Aug 16 2020 at 05:29):

How can I use `algebra'.univ_mem`

to fill this?

```
example (all_algebras: ∀n : ℕ, algebra' (ss n) ) : algebra' α :=
{
σ := Union ss,
univ_mem := by {
simp only [mem_Union],
specialize all_algebras 0,
let ss0 := (ss 0),
have: univ ∈ ss0,
{
-- α: Type u
-- ss: ℕ → set (set α)
-- all_algebras: algebra' ↥(ss 0)
-- ss0: set (set α) := ss 0
-- ⊢ univ ∈ ss0
}
},
closed_complements := _,
closed_finite_unions := _
}
```

#### Iocta (Aug 16 2020 at 05:45):

there's a sequence of `set (set alpha)`

, each of which contains `univ`

. So I should be able to pick the first one, show it has `univ`

, and then unioning it with the others should still have `univ`

.

#### Iocta (Aug 16 2020 at 05:45):

but I'm stuck at showing the first one has `univ`

#### Iocta (Aug 16 2020 at 05:49):

I figured it'd be `algebra'.univ_mem`

or something like that but no dice

#### Kenny Lau (Aug 16 2020 at 10:02):

@Iocta `algebra' (ss n)`

means an algebra structure on `ss n`

(coerced to a type), not an algebra structure on `\alpha`

whose underlying set is `ss n`

#### Kenny Lau (Aug 16 2020 at 10:06):

this should be what you mean:

```
import data.set.lattice
universe u
variable {α : Type u}
structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(closed_complements : ∀ s ∈ σ, sᶜ ∈ σ)
(closed_finite_unions (a b ∈ σ ): a ∪ b ∈ σ)
variables (ss : ℕ → algebra' α) (ss_increasing: ∀ n : ℕ, (ss n).σ ⊆ (ss (n + 1)).σ)
example : algebra' α :=
{ σ := ⋃ n, (ss n).σ,
univ_mem := set.mem_Union.2 ⟨0, (ss 0).univ_mem⟩,
closed_complements := _,
closed_finite_unions := _ }
```

#### Iocta (Aug 17 2020 at 00:23):

Yes, thank you.

#### Iocta (Aug 18 2020 at 06:59):

I guess it's complaining that `a <= `

might not be decidable? What is the normal way to handle this?

```
universe u
variable {α : Type u}
structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(closed_complements : ∀ s ∈ σ, sᶜ ∈ σ)
(closed_finite_unions (a b ∈ σ ): a ∪ b ∈ σ)
variables (ss : ℕ → algebra' α) (ss_subset_of_ss_succ: ∀ n : ℕ, (ss n).σ ⊆ (ss (n + 1)).σ)
include ss_subset_of_ss_succ
lemma ss_increasing (n m : ℕ) (h: n ≤ m) : (ss n).σ ⊆ (ss m).σ :=
begin
intros s hs,
induction h ,
{ exact hs, },
{
specialize ss_subset_of_ss_succ h_b,
apply ss_subset_of_ss_succ,
exact h_ih,
},
end
example : algebra' α :=
{ σ := ⋃ n, (ss n).σ,
univ_mem := set.mem_Union.2 ⟨0, (ss 0).univ_mem⟩,
closed_complements := by {
intros s hs,
have exists_ssn: ∃ n : ℕ, s ∈ (ss n).σ,
{
let sn:= {n : ℕ | s ∈ (ss n).σ },
simp at hs,
cases hs with n hn,
use n,
exact hn,
},
cases exists_ssn with n hn,
norm_num,
use n,
exact (ss n).closed_complements s hn,
},
closed_finite_unions := by {
intros a b ha hb,
simp * at *,
cases ha with na hna,
cases hb with nb hnb,
let nab := max na nb,
have na_subset: (ss na).σ ⊆ (ss nab).σ, {
apply ss_increasing,
apply le_max_left,
-- invalid apply tactic, failed to unify
-- ∀ (n : ℕ), (ss n).σ ⊆ (ss (n + 1)).σ
-- with
-- ∀ [_inst_1 : decidable_linear_order ?m_1] (a b : ?m_1), a ≤ max a b
},
have nb_subset: (ss nb).σ ⊆ (ss nab).σ, {
apply ss_increasing,
apply le_max_right,
},
use nab,
apply (ss nab).closed_finite_unions a b (na_subset hna) (nb_subset hnb),
}
}
```

#### Mario Carneiro (Aug 18 2020 at 07:01):

the error says you applied something that looks different than what lean wants

#### Mario Carneiro (Aug 18 2020 at 07:02):

I don't think it's a decidability problem, it's just a completely different theorem. `ss`

has no definition in your problem, it's just a variable

#### Mario Carneiro (Aug 18 2020 at 07:04):

it looks like when you did `apply ss_increasing`

, the first subgoal you got is `(ss_subset_of_ss_succ: ∀ n : ℕ, (ss n).σ ⊆ (ss (n + 1)).σ)`

, which should be a variable in your context

#### Iocta (Aug 18 2020 at 07:28):

Alright this works

```
universe u
variable {α : Type u}
structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(closed_complements : ∀ s ∈ σ, sᶜ ∈ σ)
(closed_finite_unions (a b ∈ σ ): a ∪ b ∈ σ)
variables (ss : ℕ → algebra' α) (ss_subset_of_ss_succ: ∀ n : ℕ, (ss n).σ ⊆ (ss (n + 1)).σ)
include ss_subset_of_ss_succ
lemma ss_increasing {n m : ℕ} (h: n ≤ m) : (ss n).σ ⊆ (ss m).σ :=
begin
intros s hs,
induction h ,
{ exact hs, },
{
specialize ss_subset_of_ss_succ h_b,
apply ss_subset_of_ss_succ,
exact h_ih,
},
end
example : algebra' α :=
{ σ := ⋃ n, (ss n).σ,
univ_mem := set.mem_Union.2 ⟨0, (ss 0).univ_mem⟩,
closed_complements := by {
intros s hs,
have exists_ssn: ∃ n : ℕ, s ∈ (ss n).σ,
{
let sn:= {n : ℕ | s ∈ (ss n).σ },
simp at hs,
cases hs with n hn,
use n,
exact hn,
},
cases exists_ssn with n hn,
norm_num,
use n,
exact (ss n).closed_complements s hn,
},
closed_finite_unions := by {
intros a b ha hb,
simp * at *,
cases ha with na hna,
cases hb with nb hnb,
use (max na nb),
apply (ss (max na nb)).closed_finite_unions a b,
{
have: (ss na).σ ⊆ (ss (max na nb)).σ,
{
apply ss_increasing,
intro n,
apply ss_subset_of_ss_succ,
apply le_max_left,
},
apply this hna,
},
{
have: (ss nb).σ ⊆ (ss (max na nb)).σ,
{
apply ss_increasing,
intro n,
apply ss_subset_of_ss_succ,
apply le_max_right,
},
apply this hnb,
},
}
}
```

#### Iocta (Aug 18 2020 at 07:28):

Those `have`

s are a little awkward, can I avoid?

#### Ruben Van de Velde (Aug 18 2020 at 07:37):

```
{
apply set.mem_of_mem_of_subset hna,
apply ss_increasing,
intro n,
apply ss_subset_of_ss_succ,
apply le_max_left,
},
{
apply set.mem_of_mem_of_subset hnb,
apply ss_increasing,
intro n,
apply ss_subset_of_ss_succ,
apply le_max_right,
},
```

#### Iocta (Aug 18 2020 at 07:40):

nice. Did you happen to know that one or was there a trick to figuring it out?

#### Kyle Miller (Aug 18 2020 at 07:40):

Looks like I did the same transformation as @Ruben Van de Velde there, but there are some other simplifications, too, elsewhere:

```
import data.set
universe u
variable {α : Type u}
structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ ∈ σ)
(closed_complements : ∀ s ∈ σ, sᶜ ∈ σ)
(closed_finite_unions (a b ∈ σ ): a ∪ b ∈ σ)
variables (ss : ℕ → algebra' α) (ss_subset_of_ss_succ: ∀ n : ℕ, (ss n).σ ⊆ (ss (n + 1)).σ)
include ss_subset_of_ss_succ
lemma ss_increasing {n m : ℕ} (h: n ≤ m) : (ss n).σ ⊆ (ss m).σ :=
begin
intros s hs,
induction h ,
{ exact hs, },
{ exact ss_subset_of_ss_succ h_b h_ih, }
end
example : algebra' α :=
{ σ := ⋃ n, (ss n).σ,
univ_mem := set.mem_Union.2 ⟨0, (ss 0).univ_mem⟩,
closed_complements := by {
intros s hs,
rw set.mem_Union at hs,
cases hs with n hn,
norm_num,
use n,
exact (ss n).closed_complements s hn,
},
closed_finite_unions := by {
intros a b ha hb,
rw set.mem_Union at ha hb ⊢,
cases ha with na hna,
cases hb with nb hnb,
use (max na nb),
apply (ss (max na nb)).closed_finite_unions a b,
{ apply set.mem_of_mem_of_subset hna,
apply ss_increasing,
intro n,
apply ss_subset_of_ss_succ,
apply le_max_left, },
{ apply set.mem_of_mem_of_subset hnb,
apply ss_increasing,
intro n,
apply ss_subset_of_ss_succ,
apply le_max_right, },
}
}
```

#### Iocta (Aug 18 2020 at 07:42):

That's much prettier!

#### Ruben Van de Velde (Aug 18 2020 at 07:43):

I first tried `apply (_ : (ss nb).σ ⊆ (ss (max na nb)).σ) hna`

, but that didn't look great either, so I scrolled through https://leanprover-community.github.io/mathlib_docs/data/set/basic.html and there it was :)

#### Kyle Miller (Aug 18 2020 at 07:43):

Iocta said:

nice. Did you happen to know that one or was there a trick to figuring it out?

Usually you're not supposed to take advantage of the way things are defined, so I looked for the lemma that takes `x ∈ s`

and `s ⊆ t`

to get `x ∈ t`

figuring it must exist for that reason. I guessed it was in `data.set.basic`

, and found it with a quick search for `⊆`

. You could also use `library_search`

to find this kind of theorem. The trick then is that applying `mem_of_mem_of_subset hna`

replaces the goal with the subset relation you want to prove.

#### Kyle Miller (Aug 18 2020 at 07:45):

And don't forget about `squeeze_simp`

to figure out what your `simp`

is doing. This is where `set.mem_Union`

came from.

#### Iocta (Aug 18 2020 at 07:48):

Cool, thanks :-)

#### Iocta (Aug 18 2020 at 07:48):

just learned about rw at \entails too

#### Kyle Miller (Aug 18 2020 at 07:51):

One thing I'm confused about is that `set.mem_of_mem_of_subset`

is marked with the `@[trans]`

attribute, but you can't use the `transitivity`

tactic in its place. I'm not sure how this is supposed to work.

Last updated: May 14 2021 at 02:15 UTC