awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
nil : Perm.{u_1} (α := Multiset α) (powersetAux' []) (powersetAux' [])
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ → ∀ (IH : powersetAux' l₁ ~ powersetAux' l₂), powersetAux' (x :: l₁) ~ powersetAux' (x :: l₂)
swap : ∀ (a b : α) (l : List α), powersetAux' (b :: a :: l) ~ powersetAux' (a :: b :: l)
trans :
  ∀ {l₁ l₂ l₃ : List α},
    l₁ ~ l₂ →
      l₂ ~ l₃ →
        ∀ (IH₁ : powersetAux' l₁ ~ powersetAux' l₂) (IH₂ : powersetAux' l₂ ~ powersetAux' l₃),
          powersetAux' l₁ ~ powersetAux' l₃
⊢ powersetAux' l₁ ~ powersetAux' l₂

Tactic:
induction p with
  | nil => simp
  | cons _ _ IH =>
    simp only [powersetAux'_cons]
    exact IH.append (IH.map _)
  | swap a b =>
    simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
    apply Perm.append_left
    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_append_comm, Multiset.powersetAux'_cons, List.map_append, List.Perm.append_right, List.nil
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetAux l₁ ~ powersetAux l₂

Tactic:
powersetAux_perm_powersetAux'.trans <|
    (powerset_aux'_perm p).trans powersetAux_perm_powersetAux'.symm

Premises used: Multiset.powersetAux_perm_powersetAux', List.Perm.trans, Multiset.powerset_aux'_perm, List.Perm.symm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α).powerset = (↑(List.map ofList l.sublists) : Multiset (Multiset α))

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

Premises used: Multiset.powerset, congr_arg, Multiset.ofList, Multiset.powersetAux_eq_map_coe
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α).powerset = (↑(List.map ofList l.sublists') : Multiset (Multiset α))

Tactic:
Quot.sound powersetAux_perm_powersetAux'

Premises used: Multiset.powersetAux_perm_powersetAux', Quot.sound, Multiset.powerset, Multiset, Multiset.ofList, Quotient
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
⊢ Eq (α := Multiset (Multiset α)) (powerset 0) {0}

Tactic:
rfl

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

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s t : Multiset α
⊢ ∀ (a b : List α), ⟦a⟧ ∈ powerset ⟦b⟧ ↔ ⟦a⟧ ≤ ⟦b⟧

Tactic:
simp [Subperm, and_comm]

Premises used: and_comm, List.Subperm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
rw : List.map ofList (List.map pure l) <+~ List.map ofList l.sublists
⊢ List.map (ofList ∘ pure) l <+~ List.map ofList l.sublists

Tactic:
rw [← List.map_map]

Premises used: List.map_map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map ofList (List.map pure l) <+~ List.map ofList l.sublists

Tactic:
((map_pure_sublist_sublists _).map _).subperm

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

Tactic:
exact ((map_pure_sublist_sublists _).map _).subperm

Premises used: List.map_pure_sublist_sublists, List.Sublist.map, List.Sublist.subperm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
⊢ 0 ∈ s.powerset

Tactic:
Multiset.mem_powerset.mpr s.zero_le

Premises used: Iff.mpr, Multiset.mem_powerset, Multiset.zero_le
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
⊢ s ∈ s.powerset

Tactic:
Multiset.mem_powerset.mpr le_rfl

Premises used: Iff.mpr, le_rfl, Multiset.mem_powerset
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
⊢ ∀ (a : List α), (powerset ⟦a⟧).card = HPow.hPow (α := ℕ) 2 (card ⟦a⟧)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s : Multiset α
powerset : s.powerset = {0}
⊢ s = 0

Tactic:
simpa using congr(card $powerset)
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
⊢ Eq (α := Multiset (Multiset α)) (powerset 0) {0}

Tactic:
powerset_zero

Premises used: Multiset.powerset_zero
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
⊢ Eq (α := Multiset (Multiset α)) (powerset 0) {0}

Tactic:
exact powerset_zero

Premises used: Multiset.powerset_zero
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux l).revzip
⊢ ∃ (a : List α × List α), a ∈ l.sublists.revzip ∧ Prod.map ofList ofList a = x

Tactic:
rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h

Premises used: List.revzip, List.zip_map, Multiset.powersetAux_eq_map_coe, List.map_reverse, List.mem_map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ (a : List α × List α), a ∈ l.sublists.revzip ∧ Prod.map ofList ofList a = x
⊢ ∃ (a : List α), ∃ (b : List α), (a, b) ∈ l.sublists.revzip ∧ ((↑a : Multiset α), (↑b : Multiset α)) = x

Tactic:
simp only [Prod.map_apply, Prod.exists] at h

Premises used: Prod.map_apply, Prod.exists
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ (a : List α), ∃ (b : List α), (a, b) ∈ l.sublists.revzip ∧ ((↑a : Multiset α), (↑b : Multiset α)) = x
rcases :
  ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists.revzip),
    ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).1 + ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).2 = (↑l : Multiset α)
⊢ x.1 + x.2 = (↑l : Multiset α)

Tactic:
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).1 + ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).2 = (↑l : Multiset α)

Tactic:
Quot.sound (revzip_sublists _ _ _ h)

Premises used: Multiset.add, Quot.sound, Multiset, List.revzip_sublists, Multiset.ofList, Quotient
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).1 + ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).2 = (↑l : Multiset α)

Tactic:
exact Quot.sound (revzip_sublists _ _ _ h)

Premises used: Quot.sound, List.revzip_sublists
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux' l).revzip
⊢ ∃ (a : List α × List α), a ∈ l.sublists'.revzip ∧ Prod.map ofList ofList a = x

Tactic:
rw [revzip, powersetAux', ← map_reverse, zip_map, ← revzip, List.mem_map] at h

Premises used: Multiset.powersetAux', List.revzip, List.zip_map, List.map_reverse, List.mem_map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ (a : List α × List α), a ∈ l.sublists'.revzip ∧ Prod.map ofList ofList a = x
⊢ ∃ (a : List α), ∃ (b : List α), (a, b) ∈ l.sublists'.revzip ∧ ((↑a : Multiset α), (↑b : Multiset α)) = x

Tactic:
simp only [Prod.map_apply, Prod.exists] at h

Premises used: Prod.map_apply, Prod.exists
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ (a : List α), ∃ (b : List α), (a, b) ∈ l.sublists'.revzip ∧ ((↑a : Multiset α), (↑b : Multiset α)) = x
rcases :
  ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.revzip),
    ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).1 + ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).2 = (↑l : Multiset α)
⊢ x.1 + x.2 = (↑l : Multiset α)

Tactic:
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).1 + ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).2 = (↑l : Multiset α)

Tactic:
Quot.sound (revzip_sublists' _ _ _ h)

Premises used: Multiset.add, List.revzip_sublists', Quot.sound, Multiset, Multiset.ofList, Quotient
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).1 + ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).2 = (↑l : Multiset α)

Tactic:
exact Quot.sound (revzip_sublists' _ _ _ h)

Premises used: List.revzip_sublists', Quot.sound
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
rw : ∀ (x : Multiset α × Multiset α), x ∈ l'.revzip → x = (x.1, (↑l : Multiset α) - x.1)
⊢ Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) ↦ p = (s, (↑l : Multiset α) - s)) l'.revzip
    (List.map Prod.fst l'.revzip)

Tactic:
rw [forall₂_map_right_iff, forall₂_same]

Premises used: List.forall₂_map_right_iff, List.forall₂_same
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
s t : Multiset α
h : (s, t) ∈ l'.revzip
dsimp : (s, t) = (s, (↑l : Multiset α) - s)
⊢ (s, t) = ((s, t).1, (↑l : Multiset α) - (s, t).1)

Tactic:
dsimp
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
s t : Multiset α
h : (s, t) ∈ l'.revzip
rw : (s, t) = (s, (s, t).1 + (s, t).2 - s)
rw₁ rw₂ : (s, t) = (s, (s, t).2)
⊢ (s, t) = (s, (↑l : Multiset α) - s)

Tactic:
rw [← H h, add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
⊢ Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) ↦ p = (s, (↑l : Multiset α) - s)) l'.revzip
    (List.map Prod.fst l'.revzip)

Tactic:
have :
    Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) => p = (s, ↑l - s)) (revzip l')
      ((revzip l').map Prod.fst) := by
    rw [forall₂_map_right_iff, forall₂_same]
    rintro ⟨s, t⟩ h
    dsimp
    rw [← H h, add_tsub_cancel_left]
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
this :
  Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) ↦ p = (s, (↑l : Multiset α) - s)) l'.revzip
    (List.map Prod.fst l'.revzip)
rw : Forall₂ (fun (a : Multiset α × Multiset α) (c : Multiset α) ↦ a = (c, (↑l : Multiset α) - c)) l'.revzip l'
⊢ l'.revzip = List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) l'

Tactic:
rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]

Premises used: List.forall₂_map_right_iff, List.forall₂_eq_eq_eq
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
this :
  Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) ↦ p = (s, (↑l : Multiset α) - s)) l'.revzip
    (List.map Prod.fst l'.revzip)
⊢ Forall₂ (fun (a : Multiset α × Multiset α) (c : Multiset α) ↦ a = (c, (↑l : Multiset α) - c)) l'.revzip l'

Tactic:
simpa using this
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
haveI : ∀ (this : DecidableEq α), (powersetAux l).revzip ~ (powersetAux' l).revzip
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
haveI := Classical.decEq α
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
this : DecidableEq α
rw :
  Perm (α := Multiset α × Multiset α) (List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) (powersetAux l))
    (List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) (powersetAux' l))
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']

Premises used: Multiset.revzip_powersetAux_lemma, Multiset.revzip_powersetAux, Multiset.revzip_powersetAux'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
this : DecidableEq α
⊢ Perm (α := Multiset α × Multiset α) (List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) (powersetAux l))
    (List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) (powersetAux' l))

Tactic:
powersetAux_perm_powersetAux'.map _

Premises used: Multiset.powersetAux_perm_powersetAux', List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
this : DecidableEq α
⊢ Perm (α := Multiset α × Multiset α) (List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) (powersetAux l))
    (List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) (powersetAux' l))

Tactic:
exact powersetAux_perm_powersetAux'.map _

Premises used: Multiset.powersetAux_perm_powersetAux', List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
haveI : ∀ (this : DecidableEq α), (powersetAux l₁).revzip ~ (powersetAux l₂).revzip
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip

Tactic:
haveI := Classical.decEq α
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
simp :
  Perm (α := Multiset α × Multiset α) (List.map (fun (x : Multiset α) ↦ (x, (↑l₂ : Multiset α) - x)) (powersetAux l₁))
    (List.map (fun (x : Multiset α) ↦ (x, (↑l₂ : Multiset α) - x)) (powersetAux l₂))
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip

Tactic:
simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]

Premises used: Iff.mpr, Multiset.revzip_powersetAux_lemma, Multiset.revzip_powersetAux, Multiset.coe_eq_coe
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ Perm (α := Multiset α × Multiset α) (List.map (fun (x : Multiset α) ↦ (x, (↑l₂ : Multiset α) - x)) (powersetAux l₁))
    (List.map (fun (x : Multiset α) ↦ (x, (↑l₂ : Multiset α) - x)) (powersetAux l₂))

Tactic:
(powersetAux_perm p).map _

Premises used: Multiset.powersetAux_perm, List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ Perm (α := Multiset α × Multiset α) (List.map (fun (x : Multiset α) ↦ (x, (↑l₂ : Multiset α) - x)) (powersetAux l₁))
    (List.map (fun (x : Multiset α) ↦ (x, (↑l₂ : Multiset α) - x)) (powersetAux l₂))

Tactic:
exact (powersetAux_perm p).map _

Premises used: Multiset.powersetAux_perm, List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁ l₂ : List α
hsub : l₁ <+ l₂
rw : List.map ofList l₁.sublists' <+~ List.map ofList l₂.sublists'
⊢ (↑l₁ : Multiset α).powerset ≤ (↑l₂ : Multiset α).powerset

Tactic:
rw [powerset_coe', powerset_coe', coe_le]

Premises used: Multiset.coe_le, Multiset.powerset_coe'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁ l₂ : List α
hsub : l₁ <+ l₂
s₁ : List.map ofList l₁.sublists' <+ List.map ofList l₂.sublists'
⊢ List.map ofList l₁.sublists' <+~ List.map ofList l₂.sublists'

Tactic:
apply Sublist.subperm

Premises used: List.Sublist.subperm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁ l₂ : List α
hsub : l₁ <+ l₂
s₁ : l₁.sublists' <+ l₂.sublists'
⊢ List.map ofList l₁.sublists' <+ List.map ofList l₂.sublists'

Tactic:
apply Sublist.map

Premises used: List.Sublist.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁ l₂ : List α
hsub : l₁ <+ l₂
⊢ l₁.sublists' <+ l₂.sublists'

Tactic:
Sublist.sublists' hsub

Premises used: List.Sublist.sublists'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁ l₂ : List α
hsub : l₁ <+ l₂
⊢ l₁.sublists' <+ l₂.sublists'

Tactic:
exact Sublist.sublists' hsub

Premises used: List.Sublist.sublists'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
a₁ a₂ : Multiset α
a : a₁.powerset = a₂.powerset
⊢ a₁ = a₂

Tactic:
le_antisymm
    (powerset_le_powerset_iff_le.mp (le_of_eq a))
    (powerset_le_powerset_iff_le.mp (le_of_eq a.symm))

Premises used: Multiset.powerset_le_powerset_iff_le, le_antisymm, Iff.mp, le_of_eq, Eq.symm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
a₁ a₂ : Multiset α
a : a₁.powerset = a₂.powerset
⊢ a₁ = a₂

Tactic:
exact le_antisymm
    (powerset_le_powerset_iff_le.mp (le_of_eq a))
    (powerset_le_powerset_iff_le.mp (le_of_eq a.symm))

Premises used: Multiset.powerset_le_powerset_iff_le, le_antisymm, Iff.mp, le_of_eq, Eq.symm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
⊢ StrictMono.{u_1, u_1} (α := Multiset α) powerset

Tactic:
strictMono_of_le_iff_le (fun _ _ ↦ powerset_le_powerset_iff_le.symm)

Premises used: Multiset.powerset_le_powerset_iff_le, strictMono_of_le_iff_le, Iff.symm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := Multiset α) powerset

Tactic:
powerset_strictMono.monotone

Premises used: StrictMono.monotone, Multiset.powerset_strictMono
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
l : List α
rw : sublistsLenAux n l ofList [] = List.map ofList (sublistsLen n l)
rw₁ : List.map ofList (sublistsLen n l) ++ [] = List.map ofList (sublistsLen n l)
rw₂ rw₃ : List.map ofList (sublistsLen n l) = List.map ofList (sublistsLen n l)
⊢ powersetCardAux n l = List.map ofList (sublistsLen n l)

Tactic:
rw [powersetCardAux, sublistsLenAux_eq, append_nil]

Premises used: List.sublistsLenAux_eq, Multiset.powersetCardAux, List.append_nil
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
l : List α
s : Multiset α
simp :
  ∀ (a : List α),
    (∃ (a_1 : List α), (a_1 <+ l ∧ a_1.length = n) ∧ a_1 ~ a) ↔ (∃ (l_1 : List α), l_1 ~ a ∧ l_1 <+ l) ∧ a.length = n
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetCardAux n l ↔ ⟦a⟧ ≤ (↑l : Multiset α) ∧ card ⟦a⟧ = n

Tactic:
simp only [quot_mk_to_coe, powersetCardAux_eq_map_coe, List.mem_map, mem_sublistsLen,
      coe_eq_coe, coe_le, Subperm, coe_card]

Premises used: Multiset.powersetCardAux_eq_map_coe, Multiset.coe_le, Multiset.quot_mk_to_coe, List.mem_sublistsLen, Multiset.coe_eq_coe, List.Subperm, Multiset.coe_card, List.mem_map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α),
    (∃ (a_1 : List α), (a_1 <+ l ∧ a_1.length = n) ∧ a_1 ~ a) ↔ (∃ (l_1 : List α), l_1 ~ a ∧ l_1 <+ l) ∧ a.length = n

Tactic:
fun l₁ =>
      ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩,
       fun ⟨⟨l₂, p, s⟩, e⟩ => ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩

Premises used: Exists, _private.0.Multiset.mem_powersetCardAux.match_4, List.Perm, List.Perm.length_eq, And, And.intro, Iff.intro, Exists.intro, List.Sublist, List.Perm.symm, _private.0.Multiset.mem_powersetCardAux.match_3, Eq, List.length, Eq.trans
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α),
    (∃ (a_1 : List α), (a_1 <+ l ∧ a_1.length = n) ∧ a_1 ~ a) ↔ (∃ (l_1 : List α), l_1 ~ a ∧ l_1 <+ l) ∧ a.length = n

Tactic:
exact fun l₁ =>
      ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩,
       fun ⟨⟨l₂, p, s⟩, e⟩ => ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
⊢ powersetCardAux 0 l = [0]

Tactic:
simp [powersetCardAux_eq_map_coe]

Premises used: Multiset.powersetCardAux_eq_map_coe
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
⊢ Eq.{u_1 + 1} (α := List (Multiset α)) (powersetCardAux (n + 1) []) []

Tactic:
rfl

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

Tactic:
simp [powersetCardAux_eq_map_coe]

Premises used: Multiset.powersetCardAux_eq_map_coe
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂

Tactic:
simp
-- 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₂
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂

Tactic:
?_
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
n : ℕ
l₁ l₂ : List α
p : l₁ ~ l₂
succ :
  ∀ (n : ℕ) (IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂) {l₁ l₂ : List α}
    (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
⊢ powersetCardAux n l₁ ~ powersetCardAux n l₂

Tactic:
induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_
-- 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 α
⊢ Perm.{u_1} (α := Multiset α) (powersetCardAux (n + 1) []) (powersetCardAux (n + 1) [])

Tactic:
rfl
-- 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 α
x : α
l₁_1 l₂_1 : List α
p : l₁_1 ~ l₂_1
IH : powersetCardAux (n + 1) l₁_1 ~ powersetCardAux (n + 1) l₂_1
succ :
  powersetCardAux (n + 1) l₁_1 ++ List.map (cons x) (powersetCardAux n l₁_1) ~
    powersetCardAux (n + 1) l₂_1 ++ List.map (cons x) (powersetCardAux n l₂_1)
⊢ powersetCardAux (n + 1) (x :: l₁_1) ~ powersetCardAux (n + 1) (x :: l₂_1)

Tactic:
simp only [powersetCardAux_cons]

Premises used: Multiset.powersetCardAux_cons
-- 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 α
x : α
l₁_1 l₂_1 : List α
p : l₁_1 ~ l₂_1
IH : powersetCardAux (n + 1) l₁_1 ~ powersetCardAux (n + 1) l₂_1
⊢ powersetCardAux (n + 1) l₁_1 ++ List.map (cons x) (powersetCardAux n l₁_1) ~
    powersetCardAux (n + 1) l₂_1 ++ List.map (cons x) (powersetCardAux n l₂_1)

Tactic:
IH.append ((IHn p).map _)

Premises used: List.Perm.append, List.Perm.map
-- 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 α
x : α
l₁_1 l₂_1 : List α
p : l₁_1 ~ l₂_1
IH : powersetCardAux (n + 1) l₁_1 ~ powersetCardAux (n + 1) l₂_1
⊢ powersetCardAux (n + 1) l₁_1 ++ List.map (cons x) (powersetCardAux n l₁_1) ~
    powersetCardAux (n + 1) l₂_1 ++ List.map (cons x) (powersetCardAux n l₂_1)

Tactic:
exact IH.append ((IHn p).map _)

Premises used: List.Perm.append, List.Perm.map
-- 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 :
  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)))
⊢ powersetCardAux (n + 1) (b :: a :: l) ~ powersetCardAux (n + 1) (a :: b :: l)

Tactic:
simp only [powersetCardAux_cons, append_assoc]

Premises used: List.append_assoc, Multiset.powersetCardAux_cons