awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s + t - t = s
have a : ∀ (a : α), count a (s + t - t) = count a s
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
hstu : s + t = u
⊢ s = u - t
have rw : s = s + t - t
Tactic: rw [← hstu, Multiset.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
hstu : s + t = u
rw : s = s + t - t
⊢ s = u - t
have rw₁ : s = s
Tactic: rw [← hstu, Multiset.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ a ::ₘ s - t = a ::ₘ (s - t)
have rw : {a} + s - t = a ::ₘ (s - t)
Tactic: rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
rw : {a} + s - t = a ::ₘ (s - t)
⊢ a ::ₘ s - t = a ::ₘ (s - t)
have rw₁ : {a} + s - t = {a} + (s - t)
Tactic: rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
rw : {a} + s - t = a ::ₘ (s - t)
rw₁ : {a} + s - t = {a} + (s - t)
⊢ a ::ₘ s - t = a ::ₘ (s - t)
have rw₂ : {a} + (s - t) = {a} + (s - t)
Tactic: rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ (s - t).card + t.card = s.card
have rw : (s - t + t).card = s.card
Tactic: rw [← card_add, Multiset.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : t ≤ s
rw : (s - t + t).card = s.card
⊢ (s - t).card + t.card = s.card
have rw₁ : s.card = s.card
Tactic: rw [← card_add, Multiset.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ s - {a} = s.erase a
have a₁ : ∀ (a_1 : α), count a_1 (s - {a}) = count a_1 (s.erase a)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
a_1 : α
⊢ count a_1 (s - {a}) = count a_1 (s.erase a)
have a₁ : (count a_1 s - if a_1 = a then 1 else 0) = count a_1 (s.erase a)
Tactic: simp only [count_sub, count_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
a_1 : α
⊢ (count a_1 s - if a_1 = a then 1 else 0) = count a_1 (s.erase a)
have a₁ : a_1 = a → count a_1 s - 1 = count a_1 (s.erase a)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
a_1 : α
a₁ : a_1 = a → count a_1 s - 1 = count a_1 (s.erase a)
⊢ (count a_1 s - if a_1 = a then 1 else 0) = count a_1 (s.erase a)
have a₂ : ¬a_1 = a → count a_1 s - 0 = count a_1 (s.erase a)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ a ∈ s - t ↔ count a t < count a s
have rw : 0 < count a (s - t) ↔ count a t < count a s
Tactic: rw [← count_pos, count_sub, Nat.sub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
rw : 0 < count a (s - t) ↔ count a t < count a s
⊢ a ∈ s - t ↔ count a t < count a s
have rw₁ : 0 < count a s - count a t ↔ count a t < count a s
Tactic: rw [← count_pos, count_sub, Nat.sub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
rw : 0 < count a (s - t) ↔ count a t < count a s
rw₁ : 0 < count a s - count a t ↔ count a t < count a s
⊢ a ∈ s - t ↔ count a t < count a s
have rw₂ : count a t < count a s ↔ count a t < count a s
Tactic: rw [← count_pos, count_sub, Nat.sub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
⊢ Rel r (s + u) (t + v)
have zero : Rel r (0 + u) (0 + v)
Tactic: induction hst with
  | zero => simpa using huv
  | cons hab hst ih => simpa using ih.cons hab
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
zero : Rel r (0 + u) (0 + v)
⊢ Rel r (s + u) (t + v)
have cons : ∀ {a : α} {b : β} {as : Multiset α} {bs : Multiset β} (hab : r a b) (hst : Rel r as bs) (ih : Rel r (as + u) (bs + v)),
  Rel r (a ::ₘ as + u) (b ::ₘ bs + v)
Tactic: induction hst with
  | zero => simpa using huv
  | cons hab hst ih => simpa using ih.cons hab
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
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 β
⊢ Rel r (a ::ₘ s + as₁) bs ↔
    ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r (a ::ₘ s) bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
have simp : (∃ (b : β),
    ∃ (bs' : Multiset β),
      r a b ∧
        (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') ↔
  ∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
Tactic: simp only [ih, cons_add, rel_cons_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
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 β
⊢ (∃ (b : β),
      ∃ (bs' : Multiset β),
        r a b ∧
          (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
            bs = b ::ₘ bs') ↔
    ∃ (bs₀ : Multiset β),
      ∃ (bs₁ : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
have mp : (∃ (b : β),
    ∃ (bs' : Multiset β),
      r a b ∧
        (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') →
  ∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
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 β
mp :
  (∃ (b : β),
      ∃ (bs' : Multiset β),
        r a b ∧
          (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
            bs = b ::ₘ bs') →
    ∃ (bs₀ : Multiset β),
      ∃ (bs₁ : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + 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') ↔
    ∃ (bs₀ : Multiset β),
      ∃ (bs₁ : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
have mpr : (∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + 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: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
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 :
  ∃ (b : β),
    ∃ (bs' : Multiset β),
      r a b ∧
        (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
⊢ ∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
have mp : ∀ (b : β) (bs' : Multiset β) (hab : r a b)
  (h : ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁),
  ∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ b ::ₘ bs' = bs₀ + bs₁
Tactic: rcases h with ⟨b, bs', hab, h, rfl⟩
Cleared hypotheses: bs, h
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
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 : β
bs' : Multiset β
hab : r a b
h : ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁
⊢ ∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ b ::ₘ bs' = bs₀ + bs₁
have mp : ∀ (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: rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩
Cleared hypotheses: bs', h
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
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₁
⊢ ∃ (b : β),
    ∃ (bs' : Multiset β),
      r a b ∧
        (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
have 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'
Tactic: rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
Cleared hypotheses: bs, h
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
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₁
⊢ ∃ (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'
have 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'
Tactic: rcases h with ⟨b, bs, hab, h₀, rfl⟩
Cleared hypotheses: bs₀, h
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ Rel r as (bs₀ + bs₁) ↔ ∃ (as₀ : Multiset α), ∃ (as₁ : Multiset α), Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
have 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₁
Tactic: rw [← rel_flip, rel_add_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ False
have refine : count a (s - t) = 0
Tactic: refine count_eq_zero.1 ?_ h
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a (s - t) = 0
have rw : count a s ≤ count a t
Tactic: rw [count_sub a s t, Nat.sub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α)) ↔ x.1 + x.2 = (↑l : Multiset α)
have refine : ∀ (h : x.1 + x.2 = (↑l : Multiset α)), x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))
Tactic: refine ⟨fun h => revzip_powersetAux h, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = (↑l : Multiset α)
⊢ x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))
have have : ∀ (x_1 : DecidableEq α), x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))
Tactic: have _ := Classical.decEq α
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = (↑l : Multiset α)
x_1 : DecidableEq α
⊢ x ∈ (↑(powersetAux l).revzip : Multiset (Multiset α × Multiset α))
have simp : ∃ (a : Multiset α), a ≤ x.1 + x.2 ∧ (a, x.1 + x.2 - a) = x
Tactic: simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, mem_coe,
      List.mem_map, mem_powersetAux]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = (↑l : Multiset α)
x_1 : DecidableEq α
⊢ ∃ (a : Multiset α), a ≤ x.1 + x.2 ∧ (a, x.1 + x.2 - a) = x
have 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₂)
Tactic: obtain ⟨x₁, x₂⟩ := x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
s : Multiset α
l : List α
x : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = (↑l : Multiset α)
⊢ (x₁, (x₁, x₂).1 + (x₁, x₂).2 - x₁) = (x₁, x₂)
have rw : (x₁, x₂) = (x₁, x₂)
Tactic: rw [add_tsub_cancel_left x₁ x₂]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (a ::ₘ ⟦l⟧).antidiagonal =
    map (Prod.map id (cons a)) (antidiagonal ⟦l⟧) + map (Prod.map (cons a) id) (antidiagonal ⟦l⟧)
have 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))
Tactic: simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
      map_coe, antidiagonal_coe', coe_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (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))
have 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)
Tactic: rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
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)
⊢ (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))
have rw₁ : (powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length
Tactic: rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
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
have 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)
Tactic: simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_apply,
      id, sub_cons, erase_cons_head]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) 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)
have 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)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) 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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
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)
have cons : ∀ (x : Multiset α) (hx : x ∈ s.powerset), (a ::ₘ (s - x), x) = (a ::ₘ s - x, x)
Tactic: refine Multiset.map_congr rfl fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
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
⊢ (a ::ₘ (s - x), x) = (a ::ₘ s - x, x)
have cons : (a ::ₘ (s - x), x) = (a ::ₘ (s - x), x)
Tactic: rw [cons_sub_of_le _ (mem_powerset.mp hx)]
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset
have empty : Eq.{u_1 + 1} (α := Multiset (Multiset α × Multiset α)) (antidiagonal 0)
  (map (fun (t : Multiset α) ↦ (0 - t, t)) (powerset 0))
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)]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
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))
⊢ s.antidiagonal = map (fun (t : Multiset α) ↦ (s - t, t)) s.powerset
have 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
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)]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (hypothesis)
Goal:
α : Type u_1
s : Multiset α
⊢ s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card
have this : s.powerset.card = HPow.hPow (α := ℕ) 2 s.card
Tactic: have := card_powerset s
-- Lean 4 proof step from Mathlib.Data.Multiset.Antidiagonal (goal)
Goal:
α : Type u_1
s : Multiset α
this : s.powerset.card = HPow.hPow (α := ℕ) 2 s.card
⊢ s.antidiagonal.card = HPow.hPow (α := ℕ) 2 s.card
have rwa : ∀ (this : (map Prod.fst 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
Cleared hypotheses: this