Proving m ∈ F given set membership conditions

Stream: new members

[Gridiron Player]

I have these assumptions:
h: (∀ t ∈ F, x ∈ t) ∧ ∀ t ∈ G, x ∈ t
h2: m ∈ F → x ∈ m
h1B: m ∈ G
h3: ∀ t ∈ G, x ∈ t
h4: m ∈ G → x ∈ m
h5: x ∈ m

Goal: m ∈ F

Isnt the following a valid counterexample?

F={A,B}

G={C,D}

x∈A,x∈B,x∈m

m=C

We have x∈A,x∈B,x∈C

However C∉F

I might misunderstand something here. This is part of the set theory game.

[Luigi Massacci]

It would be better if you make this into an #mwe (and see #backticks) or if you link to the specific point in the game. But yes at a glance it looks like your goal is unprovable from those assumptions, I assume because you must have gone down the wrong path at some point earlier in the proof of whatever you had to prove originally

[Dan Velleman]

You're right, you won't be able to prove m ∈ F from the assumptions you have.
What level of the set theory game are you working on? If you got yourself into a situation in which you need to prove this goal, then you've probably made a mistake.

[Gridiron Player]

@Dan Velleman @Luigi Massacci
Whats up guys. Sorry for the late response. I am working on level 4 of the "Family Intersection World". Specifically, I have to proof that  ⋂(F∪G)=(⋂F)∩(⋂G).

This is what I have so far, but obviously, I went way too far:

apply Subset.antisymm

intro x

intro h

rewrite [mem_inter_iff]

apply And.intro

rewrite [mem_sInter] at h

rewrite [mem_sInter]

intro m

intro h1

apply h m

rewrite [mem_union]

apply Or.inl

exact h1

rewrite [mem_sInter] at h

rewrite [mem_sInter]

intro m

intro h1

apply h m

apply Or.inr

exact h1

intro x

intro h

rewrite [mem_sInter]

intro m

intro h1

rewrite [mem_inter_iff] at h

rewrite [mem_sInter] at h

have h2 : m ∈ F → x ∈ m := by exact h.left m

apply h2

cases' h1 with h1A h1B

exact h1A

rewrite [mem_sInter] at h

rewrite [← mem_sInter] at h

rewrite [← mem_sInter] at h

rewrite [mem_sInter] at h

rewrite [mem_sInter] at h

have h3 : ∀ t ∈ G, x ∈ t := by exact h.right

have h4 : m ∈ G → x ∈ m := h3 m

have h5 : x ∈ m := h4 h1B

[Luigi Massacci]

Am from phone so can't really check properly, but at a glance your problem is at the apply h2 line. How about you do the cases split first ; ) ?

[Luigi Massacci]

Having said that, I think this whole thread should be moved to #new members in whole likelyhood. Maybe Patrick Massot can do that if I'm not mistaken (tagging someone whom I guess is highly likely to be in this channel and that can move threads)

[Notification Bot]

This topic was moved here from #Lean for teaching > Proving m ∈ F given set membership conditions by Patrick Massot.

[Gridiron Player]

Luigi Massacci said:

Am from phone so can't really check properly, but at a glance your problem is at the apply h2 line. How about you do the cases split first ; ) ?

Thanks, that was easy. Solved the level in 2 mins after making that change. One mistake led me down a rabbit hole. Good reminder to not brute force myself through the levels and make precise moves instead.

[Dan Velleman]

Note that your problem was with the mathematics, not with Lean. It is sometimes tempting to invoke Lean tactics that seem appropriate without thinking through the mathematics to determine if that tactic is really the right way to go. Better to think more about the mathematics--and also to be willing to backtrack when you get stuck and see if you made a bad choice somewhere.

[Gridiron Player]

Yep. Very tempting indeed to use Lean as a crutch.