Zulip Chat Archive

Stream: new members

Topic: letter


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Chris Wong (Aug 14 2020 at 08:55):

suggest or library_search might help here

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 09:59):

And these are arbitrary possibly infinite unions

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Aug 14 2020 at 10:18):

Then do a case bash

view this post on Zulip Scott Morrison (Aug 14 2020 at 10:18):

(possibly with fin_cases)

view this post on Zulip 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,

view this post on Zulip 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?

view this post on Zulip Chris Wong (Aug 15 2020 at 05:56):

Your closed_countable_unions seems to be about finite unions, not countable ones?

view this post on Zulip Iocta (Aug 15 2020 at 05:56):

heh yeah that's what I meant

view this post on Zulip Iocta (Aug 15 2020 at 05:58):

[edited it to avoid confusion]

view this post on Zulip 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

view this post on Zulip Iocta (Aug 15 2020 at 06:04):

oh that sounds true

view this post on Zulip 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 := _ }

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:12):

set X is implemented as X \r Prop

view this post on Zulip 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"?

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:12):

so \lambda x : x \in s is really { x | x \in s }

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:12):

so hr is really saying r \in s

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:13):

that's what happens if you use the X \r Prop implementation to write \sigma

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:13):

σ := (λx, x ∈ s)

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:13):

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

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:14):

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

view this post on Zulip 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

view this post on Zulip Iocta (Aug 15 2020 at 08:14):

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

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:14):

not just for a specific a and b

view this post on Zulip Iocta (Aug 15 2020 at 08:14):

yeah exactly

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:15):

and instead of σ := { x | x ∈ s } you should just write σ := s

view this post on Zulip Iocta (Aug 15 2020 at 08:15):

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

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:15):

you're bracketing wrong

view this post on Zulip Iocta (Aug 15 2020 at 08:15):

okay I'll start over

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:16):

\forall a, a = a is the same as (a) : a = a

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 15 2020 at 08:16):

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

view this post on Zulip 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 *,
  }
}

view this post on Zulip Iocta (Aug 15 2020 at 10:00):

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

view this post on Zulip 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]

view this post on Zulip 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 }

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 18:15):

import tactic

variable (α : Type)

example (x y : set α ): (x  y) = x  y :=
begin
  ext,
  finish
end

view this post on Zulip Kenny Lau (Aug 15 2020 at 18:25):

because it isn't a 0th order logic goal

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Aug 15 2020 at 21:56):

h.univ_mem

view this post on Zulip Kenny Lau (Aug 15 2020 at 21:56):

again I think that isn't what you meant

view this post on Zulip Kenny Lau (Aug 15 2020 at 21:57):

h is some algebra structure on \alpha that has nothing to do with s

view this post on Zulip Kenny Lau (Aug 15 2020 at 21:57):

the underlying set of h is h.\sigma

view this post on Zulip Iocta (Aug 15 2020 at 22:08):

Like this I guess

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

view this post on Zulip Kenny Lau (Aug 15 2020 at 22:12):

yes that's right

view this post on Zulip 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 := _ }

view this post on Zulip 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 := _ }

view this post on Zulip 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 := _
}

view this post on Zulip 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.

view this post on Zulip Iocta (Aug 16 2020 at 05:45):

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

view this post on Zulip Iocta (Aug 16 2020 at 05:49):

I figured it'd be algebra'.univ_mem or something like that but no dice

view this post on Zulip 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

view this post on Zulip 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 := _ }

view this post on Zulip Iocta (Aug 17 2020 at 00:23):

Yes, thank you.

view this post on Zulip 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),
  }
}

view this post on Zulip Mario Carneiro (Aug 18 2020 at 07:01):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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,
    },
  }
}

view this post on Zulip Iocta (Aug 18 2020 at 07:28):

Those haves are a little awkward, can I avoid?

view this post on Zulip 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,
    },

view this post on Zulip Iocta (Aug 18 2020 at 07:40):

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

view this post on Zulip 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, },
  }
}

view this post on Zulip Iocta (Aug 18 2020 at 07:42):

That's much prettier!

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Iocta (Aug 18 2020 at 07:48):

Cool, thanks :-)

view this post on Zulip Iocta (Aug 18 2020 at 07:48):

just learned about rw at \entails too

view this post on Zulip 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