awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l : List α
succ :
  List.map (cons a) (powersetCardAux n l) ++ List.map (cons b) (powersetCardAux n (a :: l)) ~
    List.map (cons b) (powersetCardAux n l) ++ List.map (cons a) (powersetCardAux n (b :: l))
⊢ powersetCardAux (n + 1) l ++
      (List.map (cons a) (powersetCardAux n l) ++ List.map (cons b) (powersetCardAux n (a :: l))) ~
    powersetCardAux (n + 1) l ++
      (List.map (cons b) (powersetCardAux n l) ++ List.map (cons a) (powersetCardAux n (b :: l)))

Tactic:
apply Perm.append_left

Premises used: List.Perm.append_left
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l : List α
succ :
  ∀ (IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂),
    List.map (cons a) (powersetCardAux 0 l) ++ List.map (cons b) (powersetCardAux 0 (a :: l)) ~
      List.map (cons b) (powersetCardAux 0 l) ++ List.map (cons a) (powersetCardAux 0 (b :: l))
succ₁ :
  ∀ (n : ℕ) (IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂),
    List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons b) (powersetCardAux (n + 1) (a :: l)) ~
      List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons a) (powersetCardAux (n + 1) (b :: l))
⊢ List.map (cons a) (powersetCardAux n l) ++ List.map (cons b) (powersetCardAux n (a :: l)) ~
    List.map (cons b) (powersetCardAux n l) ++ List.map (cons a) (powersetCardAux n (b :: l))

Tactic:
cases n
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂
⊢ List.map (cons a) (powersetCardAux 0 l) ++ List.map (cons b) (powersetCardAux 0 (a :: l)) ~
    List.map (cons b) (powersetCardAux 0 l) ++ List.map (cons a) (powersetCardAux 0 (b :: l))

Tactic:
simp [Perm.swap]

Premises used: List.Perm.swap
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
succ :
  List.map (cons a) (powersetCardAux (n + 1) l) ++
      (List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons b ∘ cons a) (powersetCardAux n l)) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++
      (List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons a ∘ cons b) (powersetCardAux n l))
⊢ List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons b) (powersetCardAux (n + 1) (a :: l)) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons a) (powersetCardAux (n + 1) (b :: l))

Tactic:
simp only [powersetCardAux_cons, map_append, List.map_map]

Premises used: List.map_map, List.map_append, Multiset.powersetCardAux_cons
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
h : ∀ (s : Multiset α), (cons b ∘ cons a) s = (cons a ∘ cons b) s
⊢ cons b ∘ cons a = cons a ∘ cons b

Tactic:
funext s
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
s : Multiset α
⊢ (cons b ∘ cons a) s = (cons a ∘ cons b) s

Tactic:
simp [cons_swap]

Premises used: Multiset.cons_swap
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
succ :
  List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons b) (powersetCardAux (n + 1) l) ++
      List.map (cons a ∘ cons b) (powersetCardAux n l) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons a) (powersetCardAux (n + 1) l) ++
      List.map (cons a ∘ cons b) (powersetCardAux n l)
⊢ List.map (cons a) (powersetCardAux (n + 1) l) ++
      (List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons b ∘ cons a) (powersetCardAux n l)) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++
      (List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons a ∘ cons b) (powersetCardAux n l))

Tactic:
rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]

Premises used: List.append_assoc
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons b) (powersetCardAux (n + 1) l) ++
      List.map (cons a ∘ cons b) (powersetCardAux n l) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons a) (powersetCardAux (n + 1) l) ++
      List.map (cons a ∘ cons b) (powersetCardAux n l)

Tactic:
perm_append_comm.append_right _

Premises used: List.perm_append_comm, List.Perm.append_right
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons b) (powersetCardAux (n + 1) l) ++
      List.map (cons a ∘ cons b) (powersetCardAux n l) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons a) (powersetCardAux (n + 1) l) ++
      List.map (cons a ∘ cons b) (powersetCardAux n l)

Tactic:
exact perm_append_comm.append_right _

Premises used: List.perm_append_comm, List.Perm.append_right
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ l₁_1 l₂_1 l₃ : List α
h : l₁_1 ~ l₂_1
h_1 : l₂_1 ~ l₃
IH₁ : powersetCardAux (n + 1) l₁_1 ~ powersetCardAux (n + 1) l₂_1
IH₂ : powersetCardAux (n + 1) l₂_1 ~ powersetCardAux (n + 1) l₃
⊢ powersetCardAux (n + 1) l₁_1 ~ powersetCardAux (n + 1) l₃

Tactic:
IH₁.trans IH₂

Premises used: List.Perm.trans
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ l₁_1 l₂_1 l₃ : List α
h : l₁_1 ~ l₂_1
h_1 : l₂_1 ~ l₃
IH₁ : powersetCardAux (n + 1) l₁_1 ~ powersetCardAux (n + 1) l₂_1
IH₂ : powersetCardAux (n + 1) l₂_1 ~ powersetCardAux (n + 1) l₃
⊢ powersetCardAux (n + 1) l₁_1 ~ powersetCardAux (n + 1) l₃

Tactic:
exact IH₁.trans IH₂

Premises used: List.Perm.trans
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
succ : Perm.{u_1} (α := Multiset α) (powersetCardAux (n + 1) []) (powersetCardAux (n + 1) [])
succ₁ :
  ∀ (x : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) (IH : powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂),
    powersetCardAux (n + 1) (x :: l₁) ~ powersetCardAux (n + 1) (x :: l₂)
succ₂ : ∀ (a b : α) (l : List α), powersetCardAux (n + 1) (b :: a :: l) ~ powersetCardAux (n + 1) (a :: b :: l)
succ₃ :
  ∀ {l₁ l₂ l₃ : List α},
    l₁ ~ l₂ →
      l₂ ~ l₃ →
        ∀ (IH₁ : powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂)
          (IH₂ : powersetCardAux (n + 1) l₂ ~ powersetCardAux (n + 1) l₃),
          powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₃
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂

Tactic:
induction p with
  | nil => rfl
  | cons _ p IH =>
    simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)
  | swap a b =>
    simp only [powersetCardAux_cons, append_assoc]
    apply Perm.append_left
    cases n
    · simp [Perm.swap]
    simp only [powersetCardAux_cons, map_append, List.map_map]
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

Premises used: List.append_assoc, Multiset.cons, List.map_map, List.Perm.append_left, List.Perm.swap, List.perm_append_comm, List.map_append, List.Perm.append_right, Multiset.powersetCardAux_cons, List.nil
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
l : List α
⊢ powersetCard n (↑l : Multiset α) = (↑(powersetCardAux n l) : Multiset (Multiset α))

Tactic:
rfl

Premises used: Multiset.powersetCard, rfl
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
l : List α
⊢ powersetCard n (↑l : Multiset α) = (↑(List.map ofList (sublistsLen n l)) : Multiset (Multiset α))

Tactic:
congr_arg ((↑) : List (Multiset α) → Multiset (Multiset α)) powersetCardAux_eq_map_coe

Premises used: Multiset.powersetCardAux_eq_map_coe, congr_arg, Multiset.ofList, Multiset.powersetCard
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
⊢ powersetCard 0 ⟦l⟧ = {0}

Tactic:
simp [powersetCard_coe']

Premises used: Multiset.powersetCard_coe'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
⊢ Eq.{u_1 + 1} (α := Multiset (Multiset α)) (powersetCard (n + 1) 0) 0

Tactic:
rfl

Premises used: List.sublistsLenAux, Multiset.zero, Multiset.powersetCardAux, Multiset.ofList, Multiset.powersetCard, rfl
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
a : α
s : Multiset α
l : List α
⊢ powersetCard (n + 1) (a ::ₘ ⟦l⟧) = powersetCard (n + 1) ⟦l⟧ + map (cons a) (powersetCard n ⟦l⟧)

Tactic:
simp [powersetCard_coe']

Premises used: Multiset.powersetCard_coe'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
⊢ powersetCard 1 ⟦l⟧ = map singleton ⟦l⟧

Tactic:
simp [powersetCard_coe, sublistsLen_one, map_reverse, Function.comp_def]

Premises used: List.sublistsLen_one, Multiset.powersetCard_coe, Function.comp_def, List.map_reverse
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
l : List α
⊢ s ∈ powersetCard n ⟦l⟧ ↔ s ≤ ⟦l⟧ ∧ s.card = n

Tactic:
simp [powersetCard_coe']

Premises used: Multiset.powersetCard_coe'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Multiset α
⊢ ∀ (a : List α), (powersetCard n ⟦a⟧).card = (card ⟦a⟧).choose n

Tactic:
simp [powersetCard_coe]

Premises used: Multiset.powersetCard_coe
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Multiset α
l : List α
simp : List.map ofList (sublistsLen n l) <+~ List.map ofList l.sublists'
⊢ powersetCard n ⟦l⟧ ≤ powerset ⟦l⟧

Tactic:
simp only [quot_mk_to_coe, powersetCard_coe, powerset_coe', coe_le]

Premises used: Multiset.coe_le, Multiset.powerset_coe', Multiset.quot_mk_to_coe, Multiset.powersetCard_coe
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ List.map ofList (sublistsLen n l) <+~ List.map ofList l.sublists'

Tactic:
((sublistsLen_sublist_sublists' _ _).map _).subperm

Premises used: List.Sublist.map, List.Sublist.subperm, List.sublistsLen_sublist_sublists'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ List.map ofList (sublistsLen n l) <+~ List.map ofList l.sublists'

Tactic:
exact ((sublistsLen_sublist_sublists' _ _).map _).subperm

Premises used: List.Sublist.map, List.Sublist.subperm, List.sublistsLen_sublist_sublists'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
h_1 : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
simp : List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)
⊢ powersetCard n (↑l₁ : Multiset α) ≤ powersetCard n (↑l₂ : Multiset α)

Tactic:
simp only [powersetCard_coe, coe_le]

Premises used: Multiset.coe_le, Multiset.powersetCard_coe
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
h_1 : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)

Tactic:
((sublistsLen_sublist_of_sublist _ h).map _).subperm

Premises used: List.Sublist.map, List.sublistsLen_sublist_of_sublist, List.Sublist.subperm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
h_1 : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)

Tactic:
exact ((sublistsLen_sublist_of_sublist _ h).map _).subperm

Premises used: List.Sublist.map, List.sublistsLen_sublist_of_sublist, List.Sublist.subperm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
n : ℕ
s : Multiset α
h : s.card < n
⊢ powersetCard n s = 0

Tactic:
card_eq_zero.mp (Nat.choose_eq_zero_of_lt h ▸ card_powersetCard _ _)

Premises used: Multiset.card_eq_zero, Eq.rec, Multiset.card_powersetCard, Nat.choose_eq_zero_of_lt, Iff.mp
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
i : ℕ
hi : 0 < i
⊢ powersetCard (s.card + i) s = 0

Tactic:
simp [hi]
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
⊢ Eq (α := Multiset (Multiset α)) (powersetCard (card.{u_1} (α := α) 0) 0) {0}

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
a : α
s : Multiset α
ih : powersetCard s.card s = {s}
⊢ powersetCard (a ::ₘ s).card (a ::ₘ s) = {a ::ₘ s}

Tactic:
simp [ih]
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
empty : Eq (α := Multiset (Multiset α)) (powersetCard (card.{u_1} (α := α) 0) 0) {0}
cons : ∀ (a : α) (s : Multiset α) (ih : powersetCard s.card s = {s}), powersetCard (a ::ₘ s).card (a ::ₘ s) = {a ::ₘ s}
⊢ powersetCard s.card s = {s}

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
empty : powersetCard 0 (map f 0) = map (map f) (powersetCard 0 0)
empty₁ : ∀ (n : ℕ), powersetCard (n + 1) (map f 0) = map (map f) (powersetCard (n + 1) 0)
⊢ powersetCard n (map f 0) = map (map f) (powersetCard n 0)

Tactic:
cases n
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ powersetCard 0 (map f 0) = map (map f) (powersetCard 0 0)

Tactic:
simp [powersetCard_zero_left]

Premises used: Multiset.powersetCard_zero_left
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
⊢ powersetCard (n + 1) (map f 0) = map (map f) (powersetCard (n + 1) 0)

Tactic:
simp [powersetCard_zero_left]

Premises used: Multiset.powersetCard_zero_left
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n : ℕ
cons : powersetCard 0 (map f (t ::ₘ s)) = map (map f) (powersetCard 0 (t ::ₘ s))
cons₁ : ∀ (n : ℕ), powersetCard (n + 1) (map f (t ::ₘ s)) = map (map f) (powersetCard (n + 1) (t ::ₘ s))
⊢ powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))

Tactic:
cases n
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
⊢ powersetCard 0 (map f (t ::ₘ s)) = map (map f) (powersetCard 0 (t ::ₘ s))

Tactic:
simp [ih]
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n : ℕ
⊢ powersetCard (n + 1) (map f (t ::ₘ s)) = map (map f) (powersetCard (n + 1) (t ::ₘ s))

Tactic:
simp [ih]
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
empty : ∀ (n : ℕ), powersetCard n (map f 0) = map (map f) (powersetCard n 0)
cons :
  ∀ (t : α) (s : Multiset α) (ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)) (n : ℕ),
    powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))
⊢ powersetCard n (map f s) = map (map f) (powersetCard n s)

Tactic:
induction s using Multiset.induction generalizing n with
  | empty => cases n <;> simp [powersetCard_zero_left]
  | cons t s ih => cases n <;> simp [ih]

Premises used: Multiset.powersetCard_zero_left, Multiset.cons
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
⊢ _root_.Pairwise fun (i j : ℕ) ↦ _root_.Disjoint (powersetCard i s) (powersetCard j s)

Tactic:
fun _ _ h ↦ disjoint_left.mpr fun hi hj ↦
    h ((Multiset.mem_powersetCard.mp hi).2.symm.trans (Multiset.mem_powersetCard.mp hj).2)

Premises used: Iff.mpr, Multiset.mem_powersetCard, Multiset.disjoint_left, And.right, Pairwise, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
S : Multiset α
h : ∀ (a : List α), ((range (card ⟦a⟧ + 1)).bind fun (k : ℕ) ↦ powersetCard k ⟦a⟧) = powerset ⟦a⟧
⊢ ((range (S.card + 1)).bind fun (k : ℕ) ↦ powersetCard k S) = S.powerset

Tactic:
induction S using Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
a : List α
h :
  (↑(List.map ofList (flatMap (fun (a_1 : ℕ) ↦ sublistsLen a_1 a) (List.range (a.length + 1)))) :
      Multiset (Multiset α)) =
    (↑(List.map ofList a.sublists') : Multiset (Multiset α))
⊢ ((range (card ⟦a⟧ + 1)).bind fun (k : ℕ) ↦ powersetCard k ⟦a⟧) = powerset ⟦a⟧

Tactic:
simp_rw [quot_mk_to_coe, powerset_coe', powersetCard_coe, ← coe_range, coe_bind,
    ← List.map_flatMap, coe_card]

Premises used: Multiset.powerset_coe', Multiset.coe_bind, Multiset.quot_mk_to_coe, Multiset.powersetCard_coe, Multiset.coe_range, Multiset.coe_card, List.map_flatMap
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
a : List α
⊢ (↑(List.map ofList (flatMap (fun (a_1 : ℕ) ↦ sublistsLen a_1 a) (List.range (a.length + 1)))) :
      Multiset (Multiset α)) =
    (↑(List.map ofList a.sublists') : Multiset (Multiset α))

Tactic:
coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)

Premises used: Iff.mpr, List.range_bind_sublistsLen_perm, Multiset.coe_eq_coe, List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
a : List α
⊢ (↑(List.map ofList (flatMap (fun (a_1 : ℕ) ↦ sublistsLen a_1 a) (List.range (a.length + 1)))) :
      Multiset (Multiset α)) =
    (↑(List.map ofList a.sublists') : Multiset (Multiset α))

Tactic:
exact coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)

Premises used: Iff.mpr, List.range_bind_sublistsLen_perm, Multiset.coe_eq_coe, List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
simp : (List.map ofList l.sublists').Nodup
⊢ (powerset ⟦l⟧).Nodup

Tactic:
simp only [quot_mk_to_coe, powerset_coe', coe_nodup]

Premises used: Multiset.powerset_coe', Multiset.quot_mk_to_coe, Multiset.coe_nodup
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (List.map ofList l.sublists').Nodup

Tactic:
(nodup_sublists'.2 h).map_on ?_

Premises used: Iff.mpr, List.Nodup.map_on, List.nodup_sublists'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
refine :
  ∀ (x : List α), x ∈ l.sublists' → ∀ (y : List α), y ∈ l.sublists' → (↑x : Multiset α) = (↑y : Multiset α) → x = y
⊢ (List.map ofList l.sublists').Nodup

Tactic:
refine (nodup_sublists'.2 h).map_on ?_

Premises used: Iff.mpr, List.Nodup.map_on, List.nodup_sublists'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ ∀ (x : List α), x ∈ l.sublists' → ∀ (y : List α), y ∈ l.sublists' → (↑x : Multiset α) = (↑y : Multiset α) → x = y

Tactic:
fun x sx y sy e =>
        (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)

Premises used: List.mem_sublists', Quotient.exact, Iff.mp, List.Nodup.perm_iff_eq_of_sublist
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ ∀ (x : List α), x ∈ l.sublists' → ∀ (y : List α), y ∈ l.sublists' → (↑x : Multiset α) = (↑y : Multiset α) → x = y

Tactic:
exact fun x sx y sy e =>
        (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)

Premises used: List.mem_sublists', Iff.mp, List.Nodup.perm_iff_eq_of_sublist
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
s : Multiset α
h : s.Nodup
⊢ (powersetCard n s).Nodup

Tactic:
nodup_of_le (powersetCard_le_powerset _ _) (nodup_powerset.2 h)

Premises used: Multiset.nodup_of_le, Iff.mpr, Multiset.nodup_powerset, Multiset.powersetCard_le_powerset
-- Module: Mathlib.Data.Multiset.Range
Goal:
n : ℕ
⊢ (↑(List.range n) : Multiset ℕ) = range n

Tactic:
rfl

Premises used: Multiset.range, rfl
-- Module: Mathlib.Data.Multiset.Range
Goal:
⊢ range 0 = 0

Tactic:
rfl

Premises used: Multiset.zero, List.range, Multiset.ofList, Multiset.range, rfl, List.range.loop
-- Module: Mathlib.Data.Multiset.Range
Goal:
n : ℕ
rw : (↑(List.range n.succ) : Multiset ℕ) = n ::ₘ range n
rw₁ : (↑(List.range n ++ [n]) : Multiset ℕ) = n ::ₘ range n
rw₂ : (↑(List.range n) : Multiset ℕ) + (↑[n] : Multiset ℕ) = n ::ₘ range n
rw₃ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ range n
rw₄ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
rw₅ : {n} + (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
rw₆ rw₇ : n ::ₘ (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
⊢ range n.succ = n ::ₘ range n

Tactic:
rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]

Premises used: Multiset.coe_add, Multiset.singleton_add, Multiset.add_comm, Multiset.range, Multiset.coe_singleton, List.range_succ
-- Module: Mathlib.Data.Multiset.Range
Goal:
n : ℕ
⊢ (range n).card = n

Tactic:
length_range

Premises used: List.length_range, Multiset.card
-- Module: Mathlib.Data.Multiset.Range
Goal:
m n : ℕ
⊢ range m ⊆ range n ↔ m ≤ n

Tactic:
List.range_subset

Premises used: List.Subset, Multiset.Mem, List.range_subset, Multiset.Subset
-- Module: Mathlib.Data.Multiset.Range
Goal:
m n : ℕ
⊢ m ∈ range n ↔ m < n

Tactic:
List.mem_range

Premises used: List.mem_range, Multiset.Mem
-- Module: Mathlib.Data.Multiset.Range
Goal:
n : ℕ
⊢ ¬n ∈ range n

Tactic:
List.not_mem_range_self

Premises used: List.not_mem_range_self, Multiset.Mem
-- Module: Mathlib.Data.Multiset.Range
Goal:
n : ℕ
⊢ n ∈ range (n + 1)

Tactic:
List.self_mem_range_succ

Premises used: Multiset.Mem, List.self_mem_range_succ
-- Module: Mathlib.Data.Multiset.Range
Goal:
a b : ℕ
⊢ range (a + b) = range a + map (fun (x : ℕ) ↦ a + x) (range b)

Tactic:
congr_arg ((↑) : List ℕ → Multiset ℕ) List.range_add

Premises used: Multiset.add, List.range_add, congr_arg, Multiset.ofList, Multiset.range
-- Module: Mathlib.Data.Multiset.Range
Goal:
a : ℕ
m : Multiset ℕ
rw : ∀ {a_1 : ℕ}, a_1 ∈ range a → ¬Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) a_1
⊢ _root_.Disjoint (range a) (map (fun (x : ℕ) ↦ a + x) m)

Tactic:
rw [disjoint_left]

Premises used: Multiset.disjoint_left
-- Module: Mathlib.Data.Multiset.Range
Goal:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) x
⊢ x < a

Tactic:
rw [range, mem_coe, List.mem_range] at hxa

Premises used: List.mem_range, Multiset.mem_coe, Multiset.range
-- Module: Mathlib.Data.Multiset.Range
Goal:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) x
hxa₁ : x < a
⊢ Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) x

Tactic:
rw [range, mem_coe, List.mem_range] at hxa

Premises used: List.mem_range, Multiset.mem_coe, Multiset.range
-- Module: Mathlib.Data.Multiset.Range
Goal:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) x
obtain :
  ∀ (c : ℕ),
    c ∈ m → ∀ (hxa : a + c < a) (hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) (a + c)), False
⊢ False

Tactic:
obtain ⟨c, _, rfl⟩ := mem_map.1 hxb

Premises used: Multiset.mem_map, Iff.mp, rfl