awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
rw rw₁ rw₂ :
  HSub.hSub (α := G) (∑ a ∈ s.biUnion S, f a)
      (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (#(↑t : Finset ι) + 1)) (∑ a ∈ (↑t : Finset ι).inf' ⋯ S, f a)) =
    0
⊢ Eq.{u_3 + 1} (α := G) (∑ a ∈ s.biUnion S, f a)
    (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
      HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (#(↑t : Finset ι) + 1)) (∑ a ∈ (↑t : Finset ι).inf' ⋯ S, f a))

Tactic:
classical
  rw [← sub_eq_zero]
  calc
    ∑ a ∈ s.biUnion S, f a - ∑ t : s.powerset.filter (·.Nonempty),
      (-1) ^ (#t.1 + 1) • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a
      = ∑ t : s.powerset.filter (·.Nonempty),
          (-1) ^ #t.1 • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a +
          ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ s.biUnion S, f a := by
      simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t •
          if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a := by
      rw [← sum_attach (filter ..)]; simp [sum_dite]
    _ = ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - Set.indicator (S i) 1 a : ℤ)) • f a := by
      simp only [Int.reduceNeg, prod_sub, sum_comm (s := s.biUnion S), sum_smul, mul_assoc]
      congr! with t
      split_ifs with ht
      · obtain ⟨i, hi⟩ := ht
        simp only [prod_const_one, prod_indicator_apply]
        simp only [smul_sum, Set.indicator, Set.mem_iInter, mem_coe, Pi.one_apply, mul_ite, mul_one,
          mul_zero, ite_smul, zero_smul, sum_ite, not_forall, sum_const_zero, add_zero]
        congr
        aesop
      · obtain rfl := not_nonempty_iff_eq_empty.1 ht
        simp
    _ = ∑ a ∈ s.biUnion S, (∏ i ∈ s,
          (Set.indicator (s.biUnion S) 1 a - Set.indicator (S i) 1 a) : ℤ) • f a := by
      congr! with t; rw [Set.indicator_of_mem ‹_›, Pi.one_apply]
    _ = 0 := by
      obtain rfl | hs := s.eq_empty_or_nonempty <;>
        simp [-coe_biUnion, prod_indicator_biUnion_finset_sub_indicator, *]

Premises used: sub_eq_zero, Finset.biUnion, Finset.powerset, OfNat.ofNat, Finset.filter, Not, Neg.neg
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
S : ι → Finset α
⊢ Eq (α := ℤ) (↑(#(s.biUnion S)) : ℤ)
    (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
      HPow.hPow (α := ℤ) (-1) (#(↑t : Finset ι) + 1) * (↑(#((↑t : Finset ι).inf' ⋯ S)) : ℤ))

Tactic:
simpa using inclusion_exclusion_sum_biUnion (G := ℤ) s S (f := 1)

Premises used: Finset.inclusion_exclusion_sum_biUnion, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
rw : ∑ a ∈ (s.sup S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
rw₁ : ∑ a ∈ (s.biUnion S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
rw₂ : HAdd.hAdd (α := G) (∑ a ∈ (s.biUnion S)ᶜ, f a) (∑ a ∈ s.biUnion S, f a) = ∑ a : α, f a
rw₃ rw₄ : Eq.{u_3 + 1} (α := G) (∑ i : α, f i) (∑ a : α, f a)
⊢ ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)

Tactic:
rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]

Premises used: Finset.compl_sup, eq_sub_iff_add_eq, Finset.sum_compl_add_sum, Finset.sup_eq_biUnion
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a) =
    HAdd.hAdd (α := G)
      (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
      (∑ t ∈ s.powerset with t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))

Tactic:
simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]

Premises used: pow_succ, sub_eq_add_neg, Finset.sum_attach, Finset.filter_eq', Finset.inclusion_exclusion_sum_biUnion, Finset.inf'_eq_inf, Finset.filter
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ HAdd.hAdd (α := G)
      (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
      (∑ t ∈ s.powerset with t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a)) =
    ∑ t ∈ s.powerset, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a)

Tactic:
sum_filter_not_add_sum_filter ..

Premises used: Finset.sum_filter_not_add_sum_filter
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
a : ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
a₁ :
  HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a) =
    HAdd.hAdd (α := G)
      (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
      (∑ t ∈ s.powerset with t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
⊢ Eq.{u_3 + 1} (α := G) (∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a)
    (∑ t ∈ s.powerset, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))

Tactic:
calc
    ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a
      = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
    _ = ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a
          + ∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
      simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..

Premises used: Compl.compl, Finset.biUnion, Finset.powerset, Finset.sum_filter_not_add_sum_filter, Finset.inf, OfNat.ofNat, Finset.filter, Not, Neg.neg
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
a : ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
a₁ :
  HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a) =
    HAdd.hAdd (α := G)
      (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
      (∑ t ∈ s.powerset with t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
⊢ Eq.{u_3 + 1} (α := G) (∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a)
    (∑ t ∈ s.powerset, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))

Tactic:
classical
  calc
    ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a
      = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
    _ = ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a
          + ∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
      simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..

Premises used: Compl.compl, Finset.biUnion, Finset.powerset, Finset.sum_filter_not_add_sum_filter, Finset.inf, OfNat.ofNat, Finset.filter, Not, Neg.neg
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
s : Finset ι
S : ι → Finset α
⊢ Eq (α := ℤ) (↑(card.{u_2} (α := α) (s.inf fun (i : ι) ↦ (S i)ᶜ)) : ℤ)
    (∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t * (↑(#(t.inf S)) : ℤ))

Tactic:
simpa using inclusion_exclusion_sum_inf_compl (G := ℤ) s S (f := 1)

Premises used: Finset.inclusion_exclusion_sum_inf_compl, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
m : ℕ
h : m ∈ p.parts
⊢ m ≤ n

Tactic:
simpa [p.parts_sum] using Multiset.le_sum_of_mem h

Premises used: Nat.Partition.parts_sum, Multiset.le_sum_of_mem
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
c : Composition n
rw : c.blocks.sum = n
rw₁ rw₂ : n = n
⊢ (↑c.blocks : Multiset ℕ).sum = n

Tactic:
rw [Multiset.sum_coe, c.blocks_sum]

Premises used: Multiset.sum_coe, Composition.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ ∃ (a : Composition n), ofComposition n a = { parts := ⟦b⟧, parts_pos := @hb₁, parts_sum := hb₂ }

Tactic:
?_
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
b : Multiset ℕ
hb₁ : ∀ {i : ℕ}, i ∈ b → 0 < i
hb₂ : b.sum = n
h :
  ∀ (b : List ℕ) (hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i) (hb₂ : sum ⟦b⟧ = n),
    ∃ (a : Composition n), ofComposition n a = { parts := ⟦b⟧, parts_pos := @hb₁, parts_sum := hb₂ }
⊢ ∃ (a : Composition n), ofComposition n a = { parts := b, parts_pos := @hb₁, parts_sum := hb₂ }

Tactic:
induction b using Quotient.inductionOn with | _ b => ?_
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ b.sum = n

Tactic:
simpa using hb₂
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ ∃ (a : Composition n), ofComposition n a = { parts := ⟦b⟧, parts_pos := @hb₁, parts_sum := hb₂ }

Tactic:
exact ⟨⟨b, hb₁, by simpa using hb₂⟩, Partition.ext rfl⟩
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
⊢ (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0

Tactic:
simp [sum_eq_zero_iff]

Premises used: Multiset.sum_eq_zero_iff
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
⊢ (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0

Tactic:
have lz : (l.filter (· = 0)).sum = 0 := by simp [sum_eq_zero_iff]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0
rwa :
  ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l + filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
    (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
rwa₁ :
  ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l).sum + (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
    (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
rwa₂ :
  ∀ (hl : 0 + (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n) (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0),
    (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (hl : (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n) (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0),
    (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
⊢ (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n

Tactic:
rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl

Premises used: Multiset.sum_add, zero_add, Multiset.filter_add_not, OfNat.ofNat, Eq
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
s : Sym σ n
inst : DecidableEq σ
⊢ ∀ {i : ℕ},
    Membership.mem (γ := Multiset ℕ) (map (fun (a : σ) ↦ count a (↑s : Multiset σ)) (↑s : Multiset σ).dedup) i → 0 < i

Tactic:
simp [Multiset.count_pos]

Premises used: Multiset.count_pos
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
s : Sym σ n
inst : DecidableEq σ
change : ∑ a ∈ (↑s : Multiset σ).toFinset, count a (↑s : Multiset σ) = n
⊢ sum (map (fun (a : σ) ↦ count a (↑s : Multiset σ)) (↑s : Multiset σ).dedup) = n

Tactic:
change ∑ a ∈ s.1.toFinset, count a s.1 = n

Premises used: Multiset.toFinset, Subtype.val
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
s : Sym σ n
inst : DecidableEq σ
rw : (↑s : Multiset σ).card = n
⊢ ∑ a ∈ (↑s : Multiset σ).toFinset, count a (↑s : Multiset σ) = n

Tactic:
rw [toFinset_sum_count_eq]

Premises used: Multiset.toFinset_sum_count_eq
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
s : Sym σ n
inst : DecidableEq σ
⊢ (↑s : Multiset σ).card = n

Tactic:
s.2

Premises used: Subtype.property
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
s : Sym σ n
inst : DecidableEq σ
⊢ (↑s : Multiset σ).card = n

Tactic:
exact s.2

Premises used: Subtype.property
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
simp :
  Eq (α := Multiset ℕ)
    (map (fun (x : τ) ↦ count x (map (⇑e : (a : σ) → τ) (↑s : Multiset σ)))
      (dedup (map (⇑e : (a : σ) → τ) (↑s : Multiset σ))))
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
⊢ ofSym.{u_2} (σ := τ) (Sym.map (⇑e : (a : σ) → τ) s) = ofSym s

Tactic:
simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, mk.injEq]

Premises used: Sym.val_eq_coe, Nat.Partition.mk.injEq, Nat.Partition.ofSym, Sym.coe_map
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
rw :
  Eq (α := Multiset ℕ)
    (map (fun (x : τ) ↦ count x (map (⇑e : (a : σ) → τ) (↑s : Multiset σ)))
      (map (⇑e : (a : σ) → τ) (↑s : Multiset σ).dedup))
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
⊢ Eq (α := Multiset ℕ)
    (map (fun (x : τ) ↦ count x (map (⇑e : (a : σ) → τ) (↑s : Multiset σ)))
      (dedup (map (⇑e : (a : σ) → τ) (↑s : Multiset σ))))
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)

Tactic:
rw [Multiset.dedup_map_of_injective e.injective]

Premises used: Multiset.dedup_map_of_injective, Equiv.injective
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
simp :
  Eq (α := Multiset ℕ)
    (map
      (fun (x : σ) ↦
        count.{u_2} (α := τ) ((e : (a : σ) → τ) x : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ))
      (↑s : Multiset σ).dedup)
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
⊢ Eq (α := Multiset ℕ)
    (map (fun (x : τ) ↦ count x (map (⇑e : (a : σ) → τ) (↑s : Multiset σ)))
      (map (⇑e : (a : σ) → τ) (↑s : Multiset σ).dedup))
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)

Tactic:
simp only [map_map, Function.comp_apply]

Premises used: Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
e_f :
  Eq.{u_1 + 1} (α := σ → ℕ)
    (fun (x : σ) ↦
      count.{u_2} (α := τ) ((e : (a : σ) → τ) x : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ))
    fun (x : σ) ↦ count x (↑s : Multiset σ)
⊢ Eq (α := Multiset ℕ)
    (map
      (fun (x : σ) ↦
        count.{u_2} (α := τ) ((e : (a : σ) → τ) x : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ))
      (↑s : Multiset σ).dedup)
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)

Tactic:
congr
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
e_f :
  ∀ (i : σ),
    count.{u_2} (α := τ) ((e : (a : σ) → τ) i : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ) =
      count i (↑s : Multiset σ)
⊢ Eq.{u_1 + 1} (α := σ → ℕ)
    (fun (x : σ) ↦
      count.{u_2} (α := τ) ((e : (a : σ) → τ) x : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ))
    fun (x : σ) ↦ count x (↑s : Multiset σ)

Tactic:
funext i
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
i : σ
e_f e_f₁ :
  count.{u_2} (α := τ) ((e : (a : σ) → τ) i : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ) =
    count.{u_2} (α := τ) ((e : (a : σ) → τ) i : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ)
⊢ count.{u_2} (α := τ) ((e : (a : σ) → τ) i : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ) =
    count i (↑s : Multiset σ)

Tactic:
rw [← Multiset.count_map_eq_count' e _ e.injective]

Premises used: Equiv.injective, DFunLike.coe, Multiset.count_map_eq_count'
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x : Sym σ n // ofSym x = μ }
⊢ ofSym.{u_2} (σ := τ)
      (((Sym.equivCongr e : Equiv.{u_1 + 1, u_2 + 1} (Sym σ n) (Sym τ n)) : (a : Sym σ n) → Sym τ n) (↑x : Sym σ n)) =
    μ

Tactic:
simp [ofSym_map, x.2]

Premises used: Nat.Partition.ofSym_map, Subtype.property
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x : Sym τ n // ofSym x = μ }
⊢ ofSym.{u_1} (σ := σ)
      (((Sym.equivCongr e.symm : Equiv.{u_2 + 1, u_1 + 1} (Sym τ n) (Sym σ n)) : (a : Sym τ n) → Sym σ n)
        (↑x : Sym τ n)) =
    μ

Tactic:
simp [ofSym_map, x.2]

Premises used: Nat.Partition.ofSym_map, Subtype.property
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x : Sym σ n // ofSym x = μ }
⊢ (fun (x : { x : Sym τ n // ofSym x = μ }) ↦
        (Subtype.mk (p := fun (x : Sym σ n) ↦ ofSym x = μ)
            (((Sym.equivCongr e.symm : Equiv.{u_2 + 1, u_1 + 1} (Sym τ n) (Sym σ n)) : (a : Sym τ n) → Sym σ n)
              (↑x : Sym τ n))
            ⋯ :
          { x : Sym σ n // ofSym x = μ }))
      ((fun (x : { x : Sym σ n // ofSym x = μ }) ↦
          (Subtype.mk (p := fun (x : Sym τ n) ↦ ofSym x = μ)
              (((Sym.equivCongr e : Equiv.{u_1 + 1, u_2 + 1} (Sym σ n) (Sym τ n)) : (a : Sym σ n) → Sym τ n)
                (↑x : Sym σ n))
              ⋯ :
            { x : Sym τ n // ofSym x = μ }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x : Sym τ n // ofSym x = μ }
⊢ (fun (x : { x : Sym σ n // ofSym x = μ }) ↦
        (Subtype.mk (p := fun (x : Sym τ n) ↦ ofSym x = μ)
            (((Sym.equivCongr e : Equiv.{u_1 + 1, u_2 + 1} (Sym σ n) (Sym τ n)) : (a : Sym σ n) → Sym τ n)
              (↑x : Sym σ n))
            ⋯ :
          { x : Sym τ n // ofSym x = μ }))
      ((fun (x : { x : Sym τ n // ofSym x = μ }) ↦
          (Subtype.mk (p := fun (x : Sym σ n) ↦ ofSym x = μ)
              (((Sym.equivCongr e.symm : Equiv.{u_2 + 1, u_1 + 1} (Sym τ n) (Sym σ n)) : (a : Sym τ n) → Sym σ n)
                (↑x : Sym τ n))
              ⋯ :
            { x : Sym σ n // ofSym x = μ }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n_1 : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
this : m ∈ p.parts → m ≠ 0
⊢ m ∈ p.parts.toFinset ↔ count m p.parts * m ≠ 0

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n_1 : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
suffices : m ∈ p.parts → m ≠ 0
⊢ m ∈ p.parts.toFinset ↔ count m p.parts * m ≠ 0

Tactic:
suffices m ∈ p.parts → m ≠ 0 by simpa
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n_1 : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
⊢ m ∈ p.parts → m ≠ 0

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p q : n.Partition
h :
  Eq (α := ℕ →₀ ℕ)
    ((fun (p : n.Partition) ↦
        ({ support := p.parts.toFinset, toFun := fun (m : ℕ) ↦ count m p.parts * m, mem_support_toFun := ⋯ } : ℕ →₀ ℕ))
      p)
    ((fun (p : n.Partition) ↦
        ({ support := p.parts.toFinset, toFun := fun (m : ℕ) ↦ count m p.parts * m, mem_support_toFun := ⋯ } : ℕ →₀ ℕ))
      q)
⊢ p.parts.toFinset = q.parts.toFinset ∧
    Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m

Tactic:
rw [Finsupp.mk.injEq] at h

Premises used: Finsupp.mk.injEq
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p q : n.Partition
h :
  p.parts.toFinset = q.parts.toFinset ∧
    Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
⊢ p.parts.toFinset = q.parts.toFinset

Tactic:
obtain ⟨hfinset, hcount⟩ := h
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p q : n.Partition
h :
  p.parts.toFinset = q.parts.toFinset ∧
    Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
hfinset : p.parts.toFinset = q.parts.toFinset
⊢ Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m

Tactic:
obtain ⟨hfinset, hcount⟩ := h
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
rw : ∀ (a : ℕ), count a p.parts = count a q.parts
⊢ p = q

Tactic:
rw [Nat.Partition.ext_iff, Multiset.ext]

Premises used: Multiset.ext, Nat.Partition.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
m : ℕ
inl : count 0 p.parts = count 0 q.parts
inr : ∀ (h0 : m > 0), count m p.parts = count m q.parts
⊢ count m p.parts = count m q.parts

Tactic:
obtain rfl | h0 := Nat.eq_zero_or_pos m

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
⊢ count 0 p.parts = count 0 q.parts

Tactic:
grind [Multiset.count_eq_zero]

Premises used: Multiset.count_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
m : ℕ
h0 : m > 0
⊢ count m p.parts = count m q.parts

Tactic:
Nat.eq_of_mul_eq_mul_right h0 <| funext_iff.mp hcount m

Premises used: funext_iff, Nat.eq_of_mul_eq_mul_right, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
m : ℕ
h0 : m > 0
⊢ count m p.parts = count m q.parts

Tactic:
exact Nat.eq_of_mul_eq_mul_right h0 <| funext_iff.mp hcount m

Premises used: funext_iff, Nat.eq_of_mul_eq_mul_right, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
⊢ p.parts.toFinset ⊆ Finset.Icc 1 n

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
⊢ p.parts.toFinset ⊆ Finset.Icc 1 n

Tactic:
have hp : p.parts.toFinset ⊆ Finset.Icc 1 n := by
    grind