-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma map_sym_eq_piAntidiag [DecidableEq ι] (s : Finset ι) (n : ℕ) :
    (s.sym n).map ⟨fun m a ↦ m.1.count a, Multiset.count_injective.comp Sym.coe_injective⟩ =
      piAntidiag s n

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
⊢ map { toFun := fun m a => Multiset.count a ↑m, inj' := ⋯ } (s.sym n) = s.piAntidiag n

Tactic:
ext f

Result:
case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ f ∈ map { toFun := fun m a => Multiset.count a ↑m, inj' := ⋯ } (s.sym n) ↔ f ∈ s.piAntidiag n

Proof state:
case h.mpr.intro.refine_2
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ (∑ a ∈ s, f a • {a}).card = s.sum f ∧ ∀ (x : ι), Multiset.count x (∑ a ∈ s, f a • {a}) = f x

Tactic:
simpa [Multiset.count_sum', Multiset.count_singleton, not_imp_comm, eq_comm (a := 0)] using hf

Result:
no goals

Proof state:
case h.mp
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) →
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Tactic:
rintro ⟨m, hm, rfl, hf⟩

Result:
case h.mp.intro.intro.intro
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
m : Multiset ι
hm : ∀ a ∈ m, a ∈ s
hf : ∀ (x : ι), Multiset.count x m = f x
⊢ s.sum f = m.card ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Proof state:
case h.mpr.intro.refine_1
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∀ a ∈ ∑ a ∈ s, f a • {a}, a ∈ s

Tactic:
simp +contextual

Result:
no goals

Proof state:
case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ f ∈ map { toFun := fun m a => Multiset.count a ↑m, inj' := ⋯ } (s.sym n) ↔ f ∈ s.piAntidiag n

Tactic:
simp only [Sym.val_eq_coe, mem_map, mem_sym_iff, Embedding.coeFn_mk, funext_iff, Sym.exists,
  Sym.mem_mk, Sym.coe_mk, exists_and_left, exists_prop, mem_piAntidiag, ne_eq]

Result:
case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) ↔
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Proof state:
case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) ↔
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Tactic:
constructor

Result:
case h.mp
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) →
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

case h.mpr
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s) →
    ∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x

Proof state:
case h.mpr.intro
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = s.sum f ∧ ∀ (x : ι), Multiset.count x s_1 = f x

Tactic:
refine ⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩

Result:
case h.mpr.intro.refine_1
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∀ a ∈ ∑ a ∈ s, f a • {a}, a ∈ s

case h.mpr.intro.refine_2
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ (∑ a ∈ s, f a • {a}).card = s.sum f ∧ ∀ (x : ι), Multiset.count x (∑ a ∈ s, f a • {a}) = f x

Proof state:
case h.mpr
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s) →
    ∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x

Tactic:
rintro ⟨rfl, hf⟩

Result:
case h.mpr.intro
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = s.sum f ∧ ∀ (x : ι), Multiset.count x s_1 = f x

Proof state:
case h.mp.intro.intro.intro
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
m : Multiset ι
hm : ∀ a ∈ m, a ∈ s
hf : ∀ (x : ι), Multiset.count x m = f x
⊢ s.sum f = m.card ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Tactic:
simpa [← hf, Multiset.sum_count_eq_card hm]

Result:
no goals