## 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

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


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 := _ }


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 haves 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.

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: Dec 20 2023 at 11:08 UTC