-- Mathlib/Data/Multiset/Fintype.lean
@[simp] lemma map_fst_le_of_subset_toEnumFinset {s : Finset (α × ℕ)} (hsm : s ⊆ m.toEnumFinset) :
    s.1.map Prod.fst ≤ m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
⊢ map Prod.fst s.val ≤ m

Tactic:
simp_rw [le_iff_count, count_map]

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
⊢ ∀ (a : α), (filter (fun a_1 => a = a_1.1) s.val).card ≤ count a m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
h : Finset.filter (fun x => x.1 = a) s ⊆ {a} ×ˢ Finset.range ((filter (fun x => a = x.1) s.val).card - 1)
⊢ False

Tactic:
have : card (s.1.filter fun x ↦ a = x.1) ≤ card (s.1.filter fun x ↦ a = x.1) - 1 := by
  simpa [Finset.card, eq_comm] using Finset.card_mono h

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
h : Finset.filter (fun x => x.1 = a) s ⊆ {a} ×ˢ Finset.range ((filter (fun x => a = x.1) s.val).card - 1)
this : (filter (fun x => a = x.1) s.val).card ≤ (filter (fun x => a = x.1) s.val).card - 1
⊢ False

Proof state:
case inr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
n : ℕ
han : n ≥ (filter (fun x => a = x.1) s.val).card - 1
hn : (a, n) ∈ s
⊢ (filter (fun a_1 => a = a_1.1) s.val).card ≤ count a m

Tactic:
exact Nat.le_of_pred_lt (han.trans_lt <| by simpa using hsm hn)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
⊢ (filter (fun a_1 => a = a_1.1) s.val).card ≤ count a m

Tactic:
obtain ha | ha := (s.1.filter fun x ↦ a = x.1).card.eq_zero_or_pos

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card = 0
⊢ (filter (fun a_1 => a = a_1.1) s.val).card ≤ count a m

case inr
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
⊢ (filter (fun a_1 => a = a_1.1) s.val).card ≤ count a m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
⊢ ∃ n ≥ (filter (fun x => a = x.1) s.val).card - 1, (a, n) ∈ s

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
h : ∀ n ≥ (filter (fun x => a = x.1) s.val).card - 1, (a, n) ∉ s
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
n : ℕ
han : n ≥ (filter (fun x => a = x.1) s.val).card - 1
hn : (a, n) ∈ s
⊢ n < count a m

Tactic:
simpa using hsm hn

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card = 0
⊢ (filter (fun a_1 => a = a_1.1) s.val).card ≤ count a m

Tactic:
rw [ha]

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card = 0
⊢ 0 ≤ count a m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
⊢ ∀ (a : α), (filter (fun a_1 => a = a_1.1) s.val).card ≤ count a m

Tactic:
rintro a

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
⊢ (filter (fun a_1 => a = a_1.1) s.val).card ≤ count a m

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card = 0
⊢ 0 ≤ count a m

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
h : Finset.filter (fun x => x.1 = a) s ⊆ {a} ×ˢ Finset.range ((filter (fun x => a = x.1) s.val).card - 1)
this : (filter (fun x => a = x.1) s.val).card ≤ (filter (fun x => a = x.1) s.val).card - 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
h : Finset.filter (fun x => x.1 = a) s ⊆ {a} ×ˢ Finset.range ((filter (fun x => a = x.1) s.val).card - 1)
⊢ (filter (fun x => a = x.1) s.val).card ≤ (filter (fun x => a = x.1) s.val).card - 1

Tactic:
simpa [Finset.card, eq_comm] using Finset.card_mono h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x => a = x.1) s.val).card > 0
h : ∀ n ≥ (filter (fun x => a = x.1) s.val).card - 1, (a, n) ∉ s
⊢ Finset.filter (fun x => x.1 = a) s ⊆ {a} ×ˢ Finset.range ((filter (fun x => a = x.1) s.val).card - 1)

Tactic:
simpa (config := { contextual := true }) [forall_swap (β := _ = a), Finset.subset_iff,
  imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using h

Result:
no goals