awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ ∃ (bs₀_1 : Multiset β),
    ∃ (bs₁_1 : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀_1 = b ::ₘ bs') ∧
        Rel r as₁ bs₁_1 ∧ b ::ₘ (bs₀ + bs₁) = bs₀_1 + bs₁_1

Tactic:
exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
h :
  ∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
mpr :
  ∀ (bs₀ bs₁ : Multiset β) (h : ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs')
    (h₁ : Rel r as₁ bs₁),
    ∃ (b : β),
      ∃ (bs' : Multiset β),
        r a b ∧
          (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
            bs₀ + bs₁ = b ::ₘ bs'
⊢ ∃ (b : β),
    ∃ (bs' : Multiset β),
      r a b ∧
        (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'

Tactic:
rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₀ bs₁ : Multiset β
h : ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs'
h₁ : Rel r as₁ bs₁
mpr :
  ∀ (b : β) (bs : Multiset β) (hab : r a b) (h₀ : Rel r s bs),
    ∃ (b_1 : β),
      ∃ (bs' : Multiset β),
        r a b_1 ∧
          (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
            b ::ₘ bs + bs₁ = b_1 ::ₘ bs'
⊢ ∃ (b : β),
    ∃ (bs' : Multiset β),
      r a b ∧
        (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
          bs₀ + bs₁ = b ::ₘ bs'

Tactic:
rcases h with ⟨b, bs, hab, h₀, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₁ : Multiset β
h₁ : Rel r as₁ bs₁
b : β
bs : Multiset β
hab : r a b
h₀ : Rel r s bs
⊢ b ::ₘ bs + bs₁ = b ::ₘ (bs + bs₁)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₁ : Multiset β
h₁ : Rel r as₁ bs₁
b : β
bs : Multiset β
hab : r a b
h₀ : Rel r s bs
⊢ ∃ (b_1 : β),
    ∃ (bs' : Multiset β),
      r a b_1 ∧
        (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
          b ::ₘ bs + bs₁ = b_1 ::ₘ bs'

Tactic:
exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
rw :
  (∃ (bs₀_1 : Multiset α),
      ∃ (bs₁_1 : Multiset α), Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ (as₀ : Multiset α), ∃ (as₁ : Multiset α), Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
⊢ Rel r as (bs₀ + bs₁) ↔ ∃ (as₀ : Multiset α), ∃ (as₁ : Multiset α), Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
rw [← rel_flip, rel_add_left]

Premises used: Multiset.rel_flip, Multiset.rel_add_left
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ (bs₀_1 : Multiset α),
      ∃ (bs₁_1 : Multiset α), Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ (as₀ : Multiset α), ∃ (as₁ : Multiset α), Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
simp [rel_flip]

Premises used: Multiset.rel_flip
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
⊢ ∀ (a : α), Nodup (α := α) {a}

Tactic:
List.nodup_singleton

Premises used: Multiset.Nodup, List.nodup_singleton
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
⊢ ∀ (a : α), ¬(a ::ₘ a ::ₘ 0).Nodup

Tactic:
List.not_nodup_pair

Premises used: Multiset.Nodup, List.not_nodup_pair
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : Multiset α
⊢ l.Nodup → (l.erase a).Nodup

Tactic:
nodup_of_le (erase_le _ _)

Premises used: Multiset.nodup_of_le, Multiset.erase_le
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ False

Tactic:
count_eq_zero.1 ?_ h

Premises used: Iff.mp, Multiset.count_eq_zero
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
refine : count a (s - t) = 0
⊢ False

Tactic:
refine count_eq_zero.1 ?_ h

Premises used: Iff.mp, Multiset.count_eq_zero
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
rw : count a s ≤ count a t
⊢ count a (s - t) = 0

Tactic:
rw [count_sub a s t, Nat.sub_eq_zero_iff_le]

Premises used: Nat.sub_eq_zero_iff_le, Multiset.count_sub
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t

Tactic:
le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')

Premises used: Iff.mpr, Multiset.nodup_iff_count_le_one, Multiset.count_pos, Iff.mp, le_trans
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t

Tactic:
exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')

Premises used: Iff.mpr, Multiset.nodup_iff_count_le_one, Multiset.count_pos, Iff.mp, le_trans
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α).antidiagonal = (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))

Tactic:
rfl

Premises used: Multiset.antidiagonal, rfl
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α).antidiagonal = (↑(powersetAux' l).revzip : Multiset (Multiset α × Multiset α))

Tactic:
Quot.sound revzip_powersetAux_perm_aux'

Premises used: Quot.sound, Multiset.revzip_powersetAux_perm_aux', Multiset, Multiset.ofList, Quotient, Multiset.antidiagonal
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α)) ↔ x.1 + x.2 = (↑l : Multiset α)

Tactic:
⟨fun h => revzip_powersetAux h, fun h ↦ ?_⟩

Premises used: Multiset.revzip_powersetAux, Iff.intro
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
refine : ∀ (h : x.1 + x.2 = (↑l : Multiset α)), x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))
⊢ x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α)) ↔ x.1 + x.2 = (↑l : Multiset α)

Tactic:
refine ⟨fun h => revzip_powersetAux h, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = (↑l : Multiset α)
have : ∀ (x_1 : DecidableEq α), x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))
⊢ x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))

Tactic:
have _ := Classical.decEq α
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = (↑l : Multiset α)
x_1 : DecidableEq α
simp : ∃ (a : Multiset α), a ≤ x.1 + x.2 ∧ (a, x.1 + x.2 - a) = x
⊢ x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))

Tactic:
simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, mem_coe,
      List.mem_map, mem_powersetAux]

Premises used: Multiset.revzip_powersetAux_lemma, Multiset.revzip_powersetAux, Multiset.mem_coe, Eq.symm, List.mem_map, Multiset.mem_powersetAux
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = (↑l : Multiset α)
x_1 : DecidableEq α
obtain :
  ∀ (x₁ x₂ : Multiset α) (h : (x₁, x₂).1 + (x₁, x₂).2 = (↑l : Multiset α)),
    ∃ (a : Multiset α), a ≤ (x₁, x₂).1 + (x₁, x₂).2 ∧ (a, (x₁, x₂).1 + (x₁, x₂).2 - a) = (x₁, x₂)
⊢ ∃ (a : Multiset α), a ≤ x.1 + x.2 ∧ (a, x.1 + x.2 - a) = x

Tactic:
obtain ⟨x₁, x₂⟩ := x
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
l : List α
x : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = (↑l : Multiset α)
rw rw₁ : (x₁, x₂) = (x₁, x₂)
⊢ (x₁, (x₁, x₂).1 + (x₁, x₂).2 - x₁) = (x₁, x₂)

Tactic:
rw [add_tsub_cancel_left x₁ x₂]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
l : List α
x : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = (↑l : Multiset α)
⊢ ∃ (a : Multiset α), a ≤ (x₁, x₂).1 + (x₁, x₂).2 ∧ (a, (x₁, x₂).1 + (x₁, x₂).2 - a) = (x₁, x₂)

Tactic:
exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
l : List α
⊢ map Prod.fst (antidiagonal ⟦l⟧) = powerset ⟦l⟧

Tactic:
simp [powersetAux']

Premises used: Multiset.powersetAux'
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
l : List α
⊢ map Prod.snd (antidiagonal ⟦l⟧) = powerset ⟦l⟧

Tactic:
simp [powersetAux']

Premises used: Multiset.powersetAux'
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
⊢ Eq (α := Multiset (Multiset α × Multiset α)) (antidiagonal 0) {(0, 0)}

Tactic:
rfl

Premises used: List.zipWith, List.revzip, Multiset.cons, Multiset.zero, List.zip, Multiset.ofList, Multiset.antidiagonal, rfl
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
a : α
s : Multiset α
l : List α
simp :
  (powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip
      ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~
    HAppend.hAppend (α := List (Multiset α × Multiset α))
      (List.map (fun (x : Multiset α × Multiset α) ↦ Prod.map id (cons a) x)
        ((powersetAux' l).zip (powersetAux' l).reverse))
      (List.map (fun (x : Multiset α × Multiset α) ↦ Prod.map (cons a) id x)
        ((powersetAux' l).zip (powersetAux' l).reverse))
⊢ (a ::ₘ ⟦l⟧).antidiagonal =
    map (Prod.map id (cons a)) (antidiagonal ⟦l⟧) + map (Prod.map (cons a) id) (antidiagonal ⟦l⟧)

Tactic:
simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
      map_coe, antidiagonal_coe', coe_add]

Premises used: Multiset.coe_add, Multiset.antidiagonal_coe', List.revzip, Multiset.quot_mk_to_coe, Multiset.coe_eq_coe, Multiset.powersetAux'_cons, Multiset.cons_coe, Multiset.map_coe, List.reverse_append
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
a : α
s : Multiset α
l : List α
rw :
  (powersetAux' l).zip (List.map (cons a) (powersetAux' l)).reverse ++
      (List.map (cons a) (powersetAux' l)).zip (powersetAux' l).reverse =
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)
rw₁ : (powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length
⊢ (powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip
      ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~
    HAppend.hAppend (α := List (Multiset α × Multiset α))
      (List.map (fun (x : Multiset α × Multiset α) ↦ Prod.map id (cons a) x)
        ((powersetAux' l).zip (powersetAux' l).reverse))
      (List.map (fun (x : Multiset α × Multiset α) ↦ Prod.map (cons a) id x)
        ((powersetAux' l).zip (powersetAux' l).reverse))

Tactic:
rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]

Premises used: List.zip_map, List.zip_append
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).zip (List.map (cons a) (powersetAux' l)).reverse ++
      (List.map (cons a) (powersetAux' l)).zip (powersetAux' l).reverse =
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Multiset (Multiset α × Multiset α)) (antidiagonal 0)
    (map (fun (t : Multiset α) ↦ (0 - t, t)) (powerset 0))

Tactic:
simp only [antidiagonal_zero, powerset_zero, Multiset.zero_sub, map_singleton]

Premises used: Multiset.map_singleton, Multiset.powerset_zero, Multiset.antidiagonal_zero, Multiset.zero_sub
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset
cons :
  HAdd.hAdd (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (s - x, a ::ₘ x)) s.powerset)
      (map (fun (x : Multiset α) ↦ (a ::ₘ (s - x), x)) s.powerset) =
    HAdd.hAdd (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ s - x, x)) s.powerset)
      (map (fun (x : Multiset α) ↦ (s - x, a ::ₘ x)) s.powerset)
⊢ (a ::ₘ s).antidiagonal = map (fun (t : Multiset α) ↦ (a ::ₘ s - t, t)) (a ::ₘ s).powerset

Tactic:
simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_apply,
      id, sub_cons, erase_cons_head]

Premises used: Multiset.antidiagonal_cons, Function.comp, id, Multiset.erase_cons_head, Multiset.sub_cons, Multiset.powerset_cons, Prod.map_apply, Multiset.map_map, Multiset.map_add
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset
cons :
  HAdd.hAdd (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ (s - x), x)) s.powerset)
      (map (fun (x : Multiset α) ↦ (s - x, a ::ₘ x)) s.powerset) =
    HAdd.hAdd (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ s - x, x)) s.powerset)
      (map (fun (x : Multiset α) ↦ (s - x, a ::ₘ x)) s.powerset)
⊢ HAdd.hAdd (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (s - x, a ::ₘ x)) s.powerset)
      (map (fun (x : Multiset α) ↦ (a ::ₘ (s - x), x)) s.powerset) =
    HAdd.hAdd (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ s - x, x)) s.powerset)
      (map (fun (x : Multiset α) ↦ (s - x, a ::ₘ x)) s.powerset)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset
cons :
  Eq (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ (s - x), x)) s.powerset)
    (map (fun (x : Multiset α) ↦ (a ::ₘ s - x, x)) s.powerset)
⊢ HAdd.hAdd (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ (s - x), x)) s.powerset)
      (map (fun (x : Multiset α) ↦ (s - x, a ::ₘ x)) s.powerset) =
    HAdd.hAdd (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ s - x, x)) s.powerset)
      (map (fun (x : Multiset α) ↦ (s - x, a ::ₘ x)) s.powerset)

Tactic:
congr 1
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset
⊢ Eq (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ (s - x), x)) s.powerset)
    (map (fun (x : Multiset α) ↦ (a ::ₘ s - x, x)) s.powerset)

Tactic:
Multiset.map_congr rfl fun x hx ↦ ?_

Premises used: Multiset.map_congr, rfl
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset
cons : ∀ (x : Multiset α) (hx : x ∈ s.powerset), (a ::ₘ (s - x), x) = (a ::ₘ s - x, x)
⊢ Eq (α := Multiset (Multiset α × Multiset α)) (map (fun (x : Multiset α) ↦ (a ::ₘ (s - x), x)) s.powerset)
    (map (fun (x : Multiset α) ↦ (a ::ₘ s - x, x)) s.powerset)

Tactic:
refine Multiset.map_congr rfl fun x hx ↦ ?_

Premises used: Multiset.map_congr, rfl
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset
x : Multiset α
hx : x ∈ s.powerset
cons cons₁ : (a ::ₘ (s - x), x) = (a ::ₘ (s - x), x)
⊢ (a ::ₘ (s - x), x) = (a ::ₘ s - x, x)

Tactic:
rw [cons_sub_of_le _ (mem_powerset.mp hx)]

Premises used: Multiset.mem_powerset, Multiset.cons_sub_of_le, Iff.mp
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
empty :
  Eq.{u_1 + 1} (α := Multiset (Multiset α × Multiset α)) (antidiagonal 0)
    (map (fun (t : Multiset α) ↦ (0 - t, t)) (powerset 0))
cons :
  ∀ (a : α) (s : Multiset α) (hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset),
    (a ::ₘ s).antidiagonal = map (fun (t : Multiset α) ↦ (a ::ₘ s - t, t)) (a ::ₘ s).powerset
⊢ s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset

Tactic:
induction s using Multiset.induction_on with
  | empty => simp only [antidiagonal_zero, powerset_zero, Multiset.zero_sub, map_singleton]
  | cons a s hs =>
    simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_apply,
      id, sub_cons, erase_cons_head]
    rw [add_comm]
    congr 1
    refine Multiset.map_congr rfl fun x hx ↦ ?_
    rw [cons_sub_of_le _ (mem_powerset.mp hx)]

Premises used: Multiset.map_singleton, Multiset.antidiagonal_cons, Multiset.powerset_zero, Function.comp, Multiset.cons, id, add_comm, Multiset.erase_cons_head, Multiset.sub_cons, Multiset.antidiagonal_zero, Multiset.zero_sub, Multiset.powerset_cons, Multiset.map_congr, Prod.map_apply, Multiset.map_map, Multiset.map_add, rfl
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
⊢ s.powerset.card = HPow.hPow (α := ℕ) 2 s.card

Tactic:
have := card_powerset s
-- Module: Mathlib.Data.Multiset.Antidiagonal
Goal:
α : Type u_1
s : Multiset α
this : s.powerset.card = HPow.hPow (α := ℕ) 2 s.card
rwa :
  ∀ (this : (map Prod.fst s.antidiagonal).card = HPow.hPow (α := ℕ) 2 s.card),
    s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card), s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card
⊢ s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card

Tactic:
rwa [← antidiagonal_map_fst, card_map] at this

Premises used: Multiset.antidiagonal_map_fst, Multiset.card_map
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
s : Multiset α
⊢ (↑s.toList : Multiset α) = s

Tactic:
s.out_eq'

Premises used: Quotient.out_eq', Multiset, Multiset.toList, Multiset.ofList
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
s : Multiset α
rw : (↑s.toList : Multiset α) = 0 ↔ s = 0
rw₁ rw₂ : s = 0 ↔ s = 0
⊢ s.toList = [] ↔ s = 0

Tactic:
rw [← coe_eq_zero, coe_toList]

Premises used: Multiset.coe_toList, Multiset.coe_eq_zero
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
s : Multiset α
⊢ s.toList.isEmpty = true ↔ s = 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) (toList 0) []

Tactic:
toList_eq_nil.mpr rfl

Premises used: Iff.mpr, Multiset.toList_eq_nil, rfl
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
a : α
s : Multiset α
rw : a ∈ (↑s.toList : Multiset α) ↔ a ∈ s
rw₁ rw₂ : a ∈ s ↔ a ∈ s
⊢ a ∈ s.toList ↔ a ∈ s

Tactic:
rw [← mem_coe, coe_toList]

Premises used: Multiset.coe_toList, Multiset.mem_coe
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
a : α
m : Multiset α
rw : m.toList ~ [a] ↔ m = {a}
rw₁ : (↑m.toList : Multiset α) = (↑[a] : Multiset α) ↔ m = {a}
rw₂ : m = (↑[a] : Multiset α) ↔ m = {a}
rw₃ rw₄ : m = {a} ↔ m = {a}
⊢ m.toList = [a] ↔ m = {a}

Tactic:
rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]

Premises used: Multiset.coe_toList, List.perm_singleton, Multiset.coe_eq_coe, Multiset.coe_singleton
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
a : α
⊢ toList {a} = [a]

Tactic:
Multiset.toList_eq_singleton_iff.2 rfl

Premises used: Iff.mpr, Multiset.toList_eq_singleton_iff, rfl
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
s : Multiset α
rw : (↑s.toList : Multiset α).card = s.card
rw₁ rw₂ : s.card = s.card
⊢ s.toList.length = s.card

Tactic:
rw [← coe_card, coe_toList]

Premises used: Multiset.coe_toList, Multiset.coe_card
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
s t : Multiset α
_h : t < s
⊢ t.card < s.card

Tactic:
card_lt_card _h

Premises used: Multiset.card_lt_card
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
s t : Multiset α
_h : t < s
⊢ t.card < s.card

Tactic:
exact card_lt_card _h

Premises used: Multiset.card_lt_card
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
s t : Multiset α
_h : t < s
⊢ t.card < s.card

Tactic:
decreasing_by exact card_lt_card _h

Premises used: Multiset.card_lt_card
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
rw rw₁ :
  (H s fun (t : Multiset α) (_h : t < s) ↦ t.strongInductionOn (p := p) H) =
    H s fun (t : Multiset α) (_h : t < s) ↦ t.strongInductionOn (p := p) H
⊢ s.strongInductionOn (p := p) H = H s fun (t : Multiset α) (_h : t < s) ↦ t.strongInductionOn (p := p) H

Tactic:
rw [strongInductionOn]
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
p : Multiset α → Prop
s : Multiset α
h₀ : p 0
h₁ : ∀ (a : α) (s : Multiset α), (∀ (t : Multiset α), t ≤ s → p t) → p (a ::ₘ s)
⊢ p s

Tactic:
Multiset.strongInductionOn s fun s =>
    Multiset.induction_on s (fun _ => h₀) fun _a _s _ ih =>
      (h₁ _ _) fun _t h => ih _ <| lt_of_le_of_lt h <| lt_cons_self _ _

Premises used: Multiset.strongInductionOn
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
⊢ s.card < t.card

Tactic:
have := (card_lt_card _h)
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
this : s.card < t.card
⊢ n - t.card < n - s.card

Tactic:
lia
-- Module: Mathlib.Data.Multiset.Basic
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
decreasing_by decreasing_by₁ decreasing_by₂ decreasing_by₃ : ∀ (this : s.card < t.card), n - t.card < n - s.card
⊢ n - t.card < n - s.card

Tactic:
decreasing_by have := (card_lt_card _h); lia