α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
⊢ m₁ ≤ m₂
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
⊢ toEnumFinset m₁ ⊆ toEnumFinset m₂ ↔ m₁ ≤ m₂
refine' ⟨fun h ↦ _, Multiset.toEnumFinset_mono⟩
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
⊢ ∀ (a : α), count a m₁ ≤ count a m₂
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
⊢ m₁ ≤ m₂
rw [Multiset.le_iff_count]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
⊢ count x m₁ ≤ count x m₂
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
⊢ ∀ (a : α), count a m₁ ≤ count a m₂
intro x
case pos
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ count x m₁ ≤ count x m₂

case neg
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : ¬x ∈ m₁
⊢ count x m₁ ≤ count x m₂
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
⊢ count x m₁ ≤ count x m₂
by_cases hx : x ∈ m₁
case pos.a
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ Nat.pred (count x m₁) < count x m₂
case pos
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ count x m₁ ≤ count x m₂
apply Nat.le_of_pred_lt
case pos.a
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
this : (x, count x m₁ - 1) ∈ toEnumFinset m₁
⊢ Nat.pred (count x m₁) < count x m₂
case pos.a
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ Nat.pred (count x m₁) < count x m₂
have : (x, m₁.count x - 1) ∈ m₁.toEnumFinset := by
  rw [Multiset.mem_toEnumFinset]
  exact Nat.pred_lt (ne_of_gt (Multiset.count_pos.mpr hx))
no goals
case pos.a
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
this : (x, count x m₁ - 1) ∈ toEnumFinset m₁
⊢ Nat.pred (count x m₁) < count x m₂
simpa only [Multiset.mem_toEnumFinset] using h this
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ (x, count x m₁ - 1).snd < count (x, count x m₁ - 1).fst m₁
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ (x, count x m₁ - 1) ∈ toEnumFinset m₁
rw [Multiset.mem_toEnumFinset]
no goals
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : x ∈ m₁
⊢ (x, count x m₁ - 1).snd < count (x, count x m₁ - 1).fst m₁
exact Nat.pred_lt (ne_of_gt (Multiset.count_pos.mpr hx))
no goals
case neg
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
hx : ¬x ∈ m₁
⊢ count x m₁ ≤ count x m₂
simp [hx]