Zulip Chat Archive
Stream: new members
Topic: Proving an element of a power set
Colin Jones ⚛️ (Jan 31 2024 at 22:04):
How would I prove this:
import Mathlib
example : {1,2} ∈ Finset.powerset {1,2,3} := by sorry
Colin Jones ⚛️ (Jan 31 2024 at 22:04):
apply? and simp? are running out of heartbeats when trying to find a theorem that solves it
Kevin Buzzard (Jan 31 2024 at 22:10):
Do we have docs#Finset.mem_powerset or docs#Finset.mem_powerset_iff ?
Kevin Buzzard (Jan 31 2024 at 22:11):
Yeah we have the first one. So the answer to your question is "guess what the relevant lemma is called, and then check it's there and rewrite or apply it depending on whether it's a <-> or a ->"
Eric Wieser (Jan 31 2024 at 22:13):
by decide works here, but Kevin's solution works more generally
Colin Jones ⚛️ (Jan 31 2024 at 22:14):
It works now:
import Mathlib
example : {1,2} ∈ (Finset.powerset {1,2,3}) := by
apply Finset.mem_powerset.mpr; simp [*]
But why could apply? not find the lemma?
Damiano Testa (Jan 31 2024 at 22:17):
Actually, apply? is instantaneous on the Lean server, but it outputs:
exact
List.Mem.tail
{ val := ↑[],
nodup :=
List.pmap.proof_3 (↑[])
(List.map Multiset.ofList
(List.append [[1]]
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append [[2]]
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(Finset.powerset.proof_1 {1, 2, 3}) }
(List.Mem.tail
{ val := ↑[1],
nodup :=
List.pmap.proof_3 (↑[1])
(List.map Multiset.ofList
(List.append []
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append [[2]]
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(List.pmap.proof_4 (↑[])
(List.map Multiset.ofList
(List.append [[1]]
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append [[2]]
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(Finset.powerset.proof_1 {1, 2, 3})) }
(List.Mem.tail
{ val := ↑[2],
nodup :=
List.pmap.proof_3 (↑[2])
(List.map Multiset.ofList
(List.append [[1, 2]]
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append []
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(List.pmap.proof_4 (↑[1])
(List.map Multiset.ofList
(List.append []
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append [[2]]
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(List.pmap.proof_4 (↑[])
(List.map Multiset.ofList
(List.append [[1]]
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append [[2]]
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(Finset.powerset.proof_1 {1, 2, 3}))) }
(List.Mem.head
(List.pmap Finset.mk
(List.map Multiset.ofList
(List.append []
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append []
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(List.pmap.proof_4 (↑[1, 2])
(List.map Multiset.ofList
(List.append []
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append []
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(List.pmap.proof_4 (↑[2])
(List.map Multiset.ofList
(List.append [[1, 2]]
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append []
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(List.pmap.proof_4 (↑[1])
(List.map Multiset.ofList
(List.append []
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append [[2]]
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(List.pmap.proof_4 (↑[])
(List.map Multiset.ofList
(List.append [[1]]
(List.join
(List.map (fun x => [x, 1 :: x])
(List.append [[2]]
(List.join
(List.map (fun x => [x, 2 :: x])
(List.append [[3]]
(List.join (List.map (fun x => [x, 3 :: x]) []))))))))))
(Finset.powerset.proof_1 {1, 2, 3})))))))))
Colin Jones ⚛️ (Feb 01 2024 at 04:05):
Yeah Im using Lean 4 on VS code and I definitely did not get that lol
Kevin Buzzard (Feb 01 2024 at 07:09):
Are you using an old mathlib?
Colin Jones ⚛️ (Feb 01 2024 at 13:40):
No I am using Mathlib 4
Ruben Van de Velde (Feb 01 2024 at 15:48):
Yes, that's clear, but mathlib 4 moves at breakneck speed
Kevin Buzzard (Feb 01 2024 at 16:25):
I'm suggesting you "bump" mathlib to get it into Feb 2024. Mathlib is constantly being tweaked to make it better. Note that bumping mathlib might make all your code break. But it might not. People typically try it out on a branch first. here are the instructions on how to do it.
Last updated: May 02 2025 at 03:31 UTC