awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : f ≤ f'
hg : g ≤ g'
⊢ s.piecewise (π := π) f g ≤ s.piecewise (π := π) f' g'

Tactic:
s.piecewise_le_piecewise' (fun x _ => hf x) fun x _ => hg x

Premises used: Finset.piecewise_le_piecewise'
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : f ∈ Set.Icc f' g'
hg : g ∈ Set.Icc f' g'
⊢ s.piecewise (π := π) f g ∈ Set.Icc f' g'

Tactic:
⟨le_piecewise_of_le_of_le _ hf.1 hg.1, piecewise_le_of_le_of_le _ hf.2 hg.2⟩

Premises used: Set.Mem, setOf, Finset.piecewise_le_of_le_of_le, Set.Icc, And.right, And.left, Finset.le_piecewise_of_le_of_le, And.intro
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
h : f ≤ g
⊢ s.piecewise (π := π) f g ∈ Set.Icc f g

Tactic:
piecewise_mem_Icc_of_mem_of_mem _ (Set.left_mem_Icc.2 h) (Set.right_mem_Icc.2 h)

Premises used: Iff.mpr, Set.right_mem_Icc, Set.left_mem_Icc, Finset.piecewise_mem_Icc_of_mem_of_mem
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
h : g ≤ f
⊢ s.piecewise (π := π) f g ∈ Set.Icc g f

Tactic:
piecewise_mem_Icc_of_mem_of_mem _ (Set.right_mem_Icc.2 h) (Set.left_mem_Icc.2 h)

Premises used: Iff.mpr, Set.right_mem_Icc, Set.left_mem_Icc, Finset.piecewise_mem_Icc_of_mem_of_mem
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s t : Finset α
mk :
  ∀ (val : Multiset α) (nodup : val.Nodup),
    { val := val, nodup := nodup : Finset α } ∈ t.powerset ↔ { val := val, nodup := nodup : Finset α } ⊆ t
⊢ s ∈ t.powerset ↔ s ⊆ t

Tactic:
cases s
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
t : Finset α
val : Multiset α
nodup : val.Nodup
⊢ { val := val, nodup := nodup : Finset α } ∈ t.powerset ↔ { val := val, nodup := nodup : Finset α } ⊆ t

Tactic:
simp [powerset, mem_mk, mem_pmap, mk.injEq, exists_prop, exists_eq_right,
    ← val_le_iff]

Premises used: Finset.mem_mk, Finset.mk.injEq, exists_eq_right, exists_prop, Finset.powerset, Finset.val_le_iff, Multiset.mem_pmap
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
h :
  ∀ (x : Finset α),
    x ∈ (↑s.powerset : Set (Finset α)) ↔ Membership.mem (γ := Set (Finset α)) (SetLike.coe ⁻¹' 𝒫 (↑s : Set α)) x
⊢ (↑s.powerset : Set (Finset α)) = SetLike.coe ⁻¹' 𝒫 (↑s : Set α)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s x : Finset α
⊢ x ∈ (↑s.powerset : Set (Finset α)) ↔ Membership.mem (γ := Set (Finset α)) (SetLike.coe ⁻¹' 𝒫 (↑s : Set α)) x

Tactic:
simp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
⊢ ∅ ∈ s.powerset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
⊢ s ∈ s.powerset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
⊢ s.powerset.Nonempty

Tactic:
⟨∅, empty_mem_powerset _⟩

Premises used: Finset.empty_mem_powerset, Exists.intro, Finset.Nonempty, EmptyCollection.emptyCollection
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s t : Finset α
⊢ s.powerset ⊆ t.powerset ↔ s ⊆ t

Tactic:
⟨fun h => mem_powerset.1 <| h <| mem_powerset_self _, fun st _u h =>
    mem_powerset.2 <| Subset.trans (mem_powerset.1 h) st⟩

Premises used: Iff.mpr, Finset.Subset.trans, Finset.mem_powerset, Iff.intro, Iff.mp, Finset.mem_powerset_self
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := Finset α) powerset

Tactic:
.of_eq_imp_le (powerset_mono.1 ·.le)

Premises used: Eq.le, Iff.mp, Finset.powerset_mono, Function.Injective.of_eq_imp_le
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s t : Finset α
⊢ s.powerset = t.powerset ↔ s = t

Tactic:
powerset_injective.eq_iff

Premises used: Function.Injective.eq_iff, Finset.powerset_injective
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
⊢ Eq (α := Finset (Finset α)) (powerset ∅) {∅}

Tactic:
rfl

Premises used: Multiset.powerset, Multiset.cons, Multiset.zero, Finset.empty, List.pmap, Multiset.ofList, Multiset.pmap, Finset.powerset, rfl
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
rw : s.powerset = powerset ∅ ↔ s = ∅
rw₁ rw₂ : s = ∅ ↔ s = ∅
⊢ s.powerset = {∅} ↔ s = ∅

Tactic:
rw [← powerset_empty, powerset_inj]

Premises used: Finset.powerset_inj, Finset.powerset_empty
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
β : Type u_2
inst : DecidableEq β
f : α → β
H : Set.InjOn f (↑s : Set α)
z : Finset α
a : α
h : z ⊆ s
h_1 : a ∈ s
⊢ a ∈ z ↔ f a ∈ image f z

Tactic:
grind [H.eq_iff]

Premises used: Set.InjOn.eq_iff
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
β : Type u_2
inst : DecidableEq β
f : α → β
H : Set.InjOn f (↑s : Set α)
⊢ ∀ {z : Finset α} {a : α}, z ⊆ s → a ∈ s → (a ∈ z ↔ f a ∈ image f z)

Tactic:
have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
β : Type u_2
inst : DecidableEq β
f : α → β
H : Set.InjOn f (↑s : Set α)
this : ∀ {z : Finset α} {a : α}, z ⊆ s → a ∈ s → (a ∈ z ↔ f a ∈ image f z)
x : Finset α
h : x ∈ (↑s.powerset : Set (Finset α))
x_1 : Finset α
h_1 : x_1 ∈ (↑s.powerset : Set (Finset α))
h_2 : Eq.{u_2 + 1} (α := Finset β) ((fun (x : Finset α) ↦ image f x) x) ((fun (x : Finset α) ↦ image f x) x_1)
⊢ x = x_1

Tactic:
grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
β : Type u_2
inst : DecidableEq β
f : α → β
H : Set.InjOn f (↑s : Set α)
this : ∀ {z : Finset α} {a : α}, z ⊆ s → a ∈ s → (a ∈ z ↔ f a ∈ image f z)
⊢ Set.InjOn.{u_1, u_2} (β := Finset β) (fun (x : Finset α) ↦ image f x) (↑s.powerset : Set (Finset α))

Tactic:
exact fun _ _ _ _ _ => by grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
S : Finset (Finset α)
f : α → β
hf : Set.InjOn f (↑(S.biUnion id) : Set α)
⊢ (↑S : Set (Finset α)) ⊆ (↑(S.biUnion id).powerset : Set (Finset α))

Tactic:
aesop (add simp Set.subset_def)

Premises used: Set.subset_def
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
t : Finset α
inst : DecidableEq α
s : Finset (Finset α)
⊢ s.biUnion id ⊆ t ↔ s ⊆ t.powerset

Tactic:
aesop (add simp subset_iff)

Premises used: Finset.subset_iff
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
β : Type u_2
inst : DecidableEq β
f : α → β
t : Finset β
ht : t ∈ (↑(image f s).powerset : Set (Finset β))
⊢ {x ∈ s | f x ∈ t} ∈ (↑s.powerset : Set (Finset α)) ∧ (fun (x : Finset α) ↦ image f x) ({x ∈ s | f x ∈ t}) = t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
β : Type u_2
inst : DecidableEq β
f : α → β
a : Finset β
h : a ∈ (image f s).powerset
⊢ {x ∈ s | f x ∈ a} ∈ s.powerset ∧ image f ({x ∈ s | f x ∈ a}) = a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
β : Type u_2
inst : DecidableEq β
f : α → β
a : Finset β
⊢ Membership.mem (γ := Finset (Finset β)) (image (fun (x : Finset α) ↦ image f x) s.powerset) a →
    a ∈ (image f s).powerset

Tactic:
grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
⊢ #s.powerset = HPow.hPow (α := ℕ) 2 #s

Tactic:
(card_pmap _ _ _).trans (Multiset.card_powerset s.1)

Premises used: Multiset.powerset, Finset.val, Multiset.card_pmap, Multiset.pmap, Multiset.card_powerset, Finset.card, Eq.trans
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
apply : a ∈ t → a ∈ s
⊢ a ∉ t

Tactic:
apply mt _ h

Premises used: mt
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∈ t → a ∈ s

Tactic:
apply mem_powerset.1 ht

Premises used: Finset.mem_powerset, Iff.mp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
h : ∀ (t : Finset α), t ∈ (insert a s).powerset ↔ t ∈ s.powerset ∪ image (insert a) s.powerset
⊢ (insert a s).powerset = s.powerset ∪ image (insert a) s.powerset

Tactic:
ext t
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
t : Finset α
h : t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t
⊢ t ∈ (insert a s).powerset ↔ t ∈ s.powerset ∪ image (insert a) s.powerset

Tactic:
simp only [mem_powerset, mem_image, mem_union, subset_insert_iff]

Premises used: Finset.mem_image, Finset.mem_powerset, Finset.mem_union, Finset.subset_insert_iff
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
simp_rw :
  ∀ ⦃i : Finset α⦄,
    i ⊆ s → ∀ ⦃j : Finset α⦄, j ⊆ s → Set.Nonempty (α := Finset α) ({i, insert a i} ∩ {j, insert a j}) → i = j
⊢ (↑s.powerset : Set (Finset α)).PairwiseDisjoint (α := Set (Finset α)) fun (t : Finset α) ↦ {t, insert a t}

Tactic:
simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]

Premises used: Finset.mem_powerset, Set.pairwiseDisjoint_iff, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
simp : (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)
⊢ Set.Nonempty (α := Finset α) ({i, insert a i} ∩ {j, insert a j}) → i = j

Tactic:
simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
    exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and]

Premises used: Set.mem_inter_iff, exists_eq_left, or_imp, Set.Nonempty, Set.mem_singleton_iff, exists_eq_or_imp, imp_self, Set.mem_insert_iff, true_and
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)

Tactic:
⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩

Premises used: Finset.insert_erase_invOn, And.right, And.intro, Finset.notMem_mono, Set.LeftInvOn.injOn
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
refine_1 : i = insert a j → i = j
refine_2 : insert a i = j → i = j
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)

Tactic:
refine ⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
j : Finset α
hj : j ⊆ s
hi : insert a j ⊆ s
⊢ insert a j = j

Tactic:
cases Finset.notMem_mono ‹_› ha (Finset.mem_insert_self _ _)

Premises used: Finset.mem_insert_self, Finset.notMem_mono
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
hj : insert a i ⊆ s
⊢ i = insert a i

Tactic:
cases Finset.notMem_mono ‹_› ha (Finset.mem_insert_self _ _)

Premises used: Finset.mem_insert_self, Finset.notMem_mono
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s_1 t s : Finset α
p : Finset α → Prop
inst : (t : Finset α) → Decidable (p t)
⊢ (∃ (t : Finset α) (_ : t ⊆ s), p t) ↔ ∃ t ⊆ s, p t

Tactic:
simp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s_1 t s : Finset α
p : Finset α → Prop
inst : (t : Finset α) → Decidable (p t)
⊢ (∀ (t : Finset α) (_h : t ⊆ s), p t) ↔ ∀ t ⊆ s, p t

Tactic:
simp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : t ∈ s.powerset.erase s ↔ t ⊂ s
rw₁ : t ≠ s ∧ t ∈ s.powerset ↔ t ⊂ s
rw₂ : t ≠ s ∧ t ⊆ s ↔ t ⊂ s
rw₃ : t ≠ s ∧ t ⊆ s ↔ t ⊆ s ∧ t ≠ s
rw₄ rw₅ : t ⊆ s ∧ t ≠ s ↔ t ⊆ s ∧ t ≠ s
⊢ t ∈ s.ssubsets ↔ t ⊂ s

Tactic:
rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]

Premises used: Finset.ssubset_iff_subset_ne, and_comm, Finset.mem_powerset, Finset.mem_erase, Finset.ssubsets
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
h : s.Nonempty
rw : ∅ ⊆ s ∧ ∅ ≠ s
⊢ ∅ ∈ s.ssubsets

Tactic:
rw [mem_ssubsets, ssubset_iff_subset_ne]

Premises used: Finset.ssubset_iff_subset_ne, Finset.mem_ssubsets
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s

Tactic:
⟨empty_subset s, h.ne_empty.symm⟩

Premises used: Ne.symm, Finset.Nonempty.ne_empty, And.intro, Finset.empty_subset
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s

Tactic:
exact ⟨empty_subset s, h.ne_empty.symm⟩
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s t : Finset α
mk :
  ∀ (val : Multiset α) (nodup : val.Nodup),
    { val := val, nodup := nodup : Finset α } ∈ powersetCard n t ↔
      { val := val, nodup := nodup : Finset α } ⊆ t ∧ #{ val := val, nodup := nodup : Finset α } = n
⊢ s ∈ powersetCard n t ↔ s ⊆ t ∧ #s = n

Tactic:
cases s
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
t : Finset α
val : Multiset α
nodup : val.Nodup
⊢ { val := val, nodup := nodup : Finset α } ∈ powersetCard n t ↔
    { val := val, nodup := nodup : Finset α } ⊆ t ∧ #{ val := val, nodup := nodup : Finset α } = n

Tactic:
simp [powersetCard, val_le_iff.symm]

Premises used: Finset.powersetCard, Iff.symm, Finset.val_le_iff
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s t : Finset α
h : s ⊆ t
⊢ powersetCard n s ⊆ powersetCard n t

Tactic:
fun _u h' => mem_powersetCard.2 <|
    And.imp (fun h₂ => Subset.trans h₂ h) id (mem_powersetCard.1 h')

Premises used: Iff.mpr, And.imp, Finset.Subset.trans, id, Finset.mem_powersetCard, Iff.mp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ #(powersetCard n s) = (#s).choose n

Tactic:
(card_pmap _ _ _).trans (Multiset.card_powersetCard n s.1)

Premises used: Multiset.card_powersetCard, Finset.val, Multiset.card_pmap, Multiset.pmap, Finset.card, Multiset.powersetCard, Eq.trans
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
⊢ Set.InjOn (β := Finset α) (fun (x : Finset α) ↦ x ∪ s) (↑(powersetCard (n - #s) (t \ s)) : Set (Finset α))

Tactic:
have hinj : Set.InjOn (· ∪ s) ↑((t \ s).powersetCard (n - #s)) := fun a ha b hb hab =>
    (union_sdiff_cancel_right
      (disjoint_of_subset_left (mem_powersetCard.mp ha).1 disjoint_sdiff_self_left)).symm.trans
    ((congrArg (· \ s) hab).trans
      (union_sdiff_cancel_right
        (disjoint_of_subset_left (mem_powersetCard.mp hb).1 disjoint_sdiff_self_left)))
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hinj : Set.InjOn (β := Finset α) (fun (x : Finset α) ↦ x ∪ s) (↑(powersetCard (n - #s) (t \ s)) : Set (Finset α))
⊢ #({x ∈ powersetCard n t | s ⊆ x}) = (#t - #s).choose (n - #s)

Tactic:
simp only [filter_powersetCard_subset s t n hst hsn, card_image_of_injOn hinj,
             card_powersetCard, card_sdiff_of_subset hst]

Premises used: Finset.card_sdiff_of_subset, Finset.filter_powersetCard_subset, Finset.card_image_of_injOn, Finset.card_powersetCard
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
⊢ powersetCard 0 s = {∅}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
⊢ (↑(powersetCard n ∅) : Set (Finset α)).Subsingleton

Tactic:
simp [Set.Subsingleton, subset_empty]

Premises used: Finset.subset_empty, Set.Subsingleton
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
i : ℕ
⊢ Multiset.map val (powersetCard i s).val = Multiset.powersetCard i s.val

Tactic:
simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']

Premises used: Multiset.pmap_eq_map, Multiset.map_pmap, Finset.powersetCard, Multiset.map_id'
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
⊢ Multiset.map val (powersetCard 1 s).val =
    Multiset.map val (map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s).val

Tactic:
simp [Multiset.powersetCard_one]

Premises used: Multiset.powersetCard_one
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
h : #s < n
rw : (#s).choose n = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ #(powersetCard n s) = 0

Tactic:
rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]

Premises used: Nat.choose_eq_zero_of_lt, Finset.card_powersetCard
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
refine : powersetCard n s = ∅ → #s < n
⊢ powersetCard n s = ∅ ↔ #s < n

Tactic:
refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
contrapose! : n ≤ #s → (powersetCard n s).Nonempty
⊢ powersetCard n s = ∅ → #s < n

Tactic:
contrapose!
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
h : n ≤ #s
⊢ ∀ (a : Finset α), a ⊆ s ∧ #a = n → a ∈ powersetCard n s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ n ≤ #s → (powersetCard n s).Nonempty

Tactic:
exact fun h ↦ (exists_subset_card_eq h).imp <| by simp

Premises used: Finset.exists_subset_card_eq, Exists.imp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
hn : 0 < n
⊢ powersetCard (#s + n) s = ∅

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
h : ∀ (a : Finset α), a ∈ powersetCard n s ↔ a ∈ {x ∈ s.powerset | #x = n}
⊢ powersetCard n s = {x ∈ s.powerset | #x = n}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s a : Finset α
⊢ a ∈ powersetCard n s ↔ a ∈ {x ∈ s.powerset | #x = n}

Tactic:
simp [mem_powersetCard]

Premises used: Finset.mem_powersetCard
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
rw :
  powersetCard n.succ s ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
⊢ powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]

Premises used: Finset.powerset_insert, Finset.powersetCard_eq_filter, Finset.filter_union
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ s ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ (powersetCard n s).Nonempty ↔ n ≤ #s

Tactic:
aesop (add simp [Finset.Nonempty, exists_subset_card_eq, card_le_card])

Premises used: Finset.card_le_card, Finset.exists_subset_card_eq, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
h : ∀ (a : Finset α), a ∈ powersetCard (#s) s ↔ Membership.mem (γ := Finset (Finset α)) {s} a
⊢ powersetCard (#s) s = {s}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
h : a ⊆ s ∧ #a = #s ↔ a = s
⊢ a ∈ powersetCard (#s) s ↔ Membership.mem (γ := Finset (Finset α)) {s} a

Tactic:
rw [mem_powersetCard, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_powersetCard
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
h : a ⊆ s ∧ #a = #s → a = s
h₁ : a = s → a ⊆ s ∧ #a = #s
⊢ a ⊆ s ∧ #a = #s ↔ a = s

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
⊢ a ⊆ s ∧ #a = #s → a = s

Tactic:
fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge

Premises used: Eq.ge, Finset.eq_of_subset_of_card_le, _private.0.Finset.powersetCard_self.match_1, Eq
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
⊢ a ⊆ s ∧ #a = #s → a = s

Tactic:
exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
a : Finset α
⊢ a ⊆ a ∧ #a = #a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
⊢ _root_.Pairwise fun (i j : ℕ) ↦ Disjoint (powersetCard i s) (powersetCard j s)

Tactic:
fun _i _j hij =>
  Finset.disjoint_left.mpr fun _x hi hj =>
    hij <| (mem_powersetCard.mp hi).2.symm.trans (mem_powersetCard.mp hj).2

Premises used: Iff.mpr, Finset.mem_powersetCard, And.right, Pairwise, Iff.mp, Finset.disjoint_left, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
⊢ s.powerset = (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯

Tactic:
ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩

Premises used: Finset.ext, Iff.intro
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s : Finset α
refine_1 : ∀ (a : Finset α) (ha : a ∈ s.powerset), a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
refine_2 : ∀ (a : Finset α) (ha : a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯), a ∈ s.powerset
⊢ s.powerset = (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯

Tactic:
refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩

Premises used: Finset.ext, Iff.intro
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
refine_1 : ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s
⊢ a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯

Tactic:
rw [mem_disjiUnion]

Premises used: Finset.mem_disjiUnion
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s

Tactic:
⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp ha))),
        mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩

Premises used: Iff.mpr, Finset.card_le_card, Nat.lt_succ_of_le, Finset.mem_range, Finset.mem_powerset, Finset.mem_powersetCard, And.intro, Exists.intro, Iff.mp, Finset.card, rfl
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s

Tactic:
exact
      ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp ha))),
        mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
ha : a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
refine_2 : ∀ (i : ℕ) (_hi : i ∈ range (#s + 1)) (ha : a ∈ powersetCard i s), a ∈ s.powerset
⊢ a ∈ s.powerset

Tactic:
rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩

Premises used: Finset.mem_disjiUnion, Iff.mp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
ha_1 : a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
i : ℕ
_hi : i ∈ range (#s + 1)
ha : a ∈ powersetCard i s
⊢ a ∈ s.powerset

Tactic:
mem_powerset.mpr (mem_powersetCard.mp ha).1

Premises used: Iff.mpr, Finset.mem_powerset, Finset.mem_powersetCard, And.left, Iff.mp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
s a : Finset α
ha_1 : a ∈ (range (#s + 1)).disjiUnion (fun (i : ℕ) ↦ powersetCard i s) ⋯
i : ℕ
_hi : i ∈ range (#s + 1)
ha : a ∈ powersetCard i s
⊢ a ∈ s.powerset

Tactic:
exact mem_powerset.mpr (mem_powersetCard.mp ha).1

Premises used: Iff.mpr, Finset.mem_powerset, Finset.mem_powersetCard, And.left, Iff.mp
-- Module: Mathlib.Data.Finset.Powerset
Goal:
α : Type u_1
inst : DecidableEq (Finset α)
s : Finset α
⊢ s.powerset = (range (#s + 1)).biUnion fun (i : ℕ) ↦ powersetCard i s

Tactic:
simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s

Premises used: Finset.disjiUnion_eq_biUnion, Finset.powerset_card_disjiUnion