[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x y : ToType m
⊢ x.fst = y.fst ↔ x.fst = y.fst
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
y : ToType m
fst✝ : α
snd✝ : Fin (count fst✝ m)
⊢ { fst := fst✝, snd := snd✝ }.fst = y.fst ↔ { fst := fst✝, snd := snd✝ }.fst = y.fst
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
fst✝¹ : α
snd✝¹ : Fin (count fst✝¹ m)
fst✝ : α
snd✝ : Fin (count fst✝ m)
⊢ { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst ↔
    { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ ∀ (x : α × ℕ),
    (x ∈
        Finset.biUnion (Multiset.toFinset m) fun x =>
          Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) }
            (Finset.range (Multiset.count x m))) ↔
      x ∈ {p | p.snd < Multiset.count p.fst m}
[PROOFSTEP]
rintro ⟨x, i⟩
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ ((x, i) ∈
      Finset.biUnion (Multiset.toFinset m) fun x =>
        Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) }
          (Finset.range (Multiset.count x m))) ↔
    (x, i) ∈ {p | p.snd < Multiset.count p.fst m}
[PROOFSTEP]
simp only [Finset.mem_biUnion, Multiset.mem_toFinset, Finset.mem_map, Finset.mem_range, Function.Embedding.coeFn_mk,
  Prod.mk.inj_iff, Set.mem_setOf_eq]
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ (∃ a, a ∈ m ∧ ∃ a_1, a_1 < Multiset.count a m ∧ a = x ∧ a_1 = i) ↔ i < Multiset.count x m
[PROOFSTEP]
simp only [← and_assoc, exists_eq_right, and_iff_right_iff_imp]
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ i < Multiset.count x m → x ∈ m
[PROOFSTEP]
exact fun h ↦ Multiset.count_pos.mp (pos_of_gt h)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
⊢ toEnumFinset m₁ ⊆ toEnumFinset m₂
[PROOFSTEP]
intro p
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ toEnumFinset m₁ → p ∈ toEnumFinset m₂
[PROOFSTEP]
simp only [Multiset.mem_toEnumFinset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.snd < count p.fst m₁ → p.snd < count p.fst m₂
[PROOFSTEP]
exact gt_of_ge_of_gt (Multiset.le_iff_count.mp h p.1)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
⊢ toEnumFinset m₁ ⊆ toEnumFinset m₂ ↔ m₁ ≤ m₂
[PROOFSTEP]
refine' ⟨fun h ↦ _, Multiset.toEnumFinset_mono⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
⊢ m₁ ≤ m₂
[PROOFSTEP]
rw [Multiset.le_iff_count]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
⊢ ∀ (a : α), count a m₁ ≤ count a m₂
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : toEnumFinset m₁ ⊆ toEnumFinset m₂
x : α
⊢ count x m₁ ≤ count x m₂
[PROOFSTEP]
by_cases hx : x ∈ m₁
[GOAL]
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₂
[PROOFSTEP]
apply Nat.le_of_pred_lt
[GOAL]
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₂
[PROOFSTEP]
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))
[GOAL]
α : 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₁
[PROOFSTEP]
rw [Multiset.mem_toEnumFinset]
[GOAL]
α : 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₁
[PROOFSTEP]
exact Nat.pred_lt (ne_of_gt (Multiset.count_pos.mpr hx))
[GOAL]
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₂
[PROOFSTEP]
simpa only [Multiset.mem_toEnumFinset] using h this
[GOAL]
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₂
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.Injective fun x => (x.fst, ↑x.snd)
[PROOFSTEP]
intro ⟨x, i, hi⟩ ⟨y, j, hj⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
hi : i < count x m
y : α
j : ℕ
hj : j < count y m
⊢ (fun x => (x.fst, ↑x.snd)) { fst := x, snd := { val := i, isLt := hi } } =
      (fun x => (x.fst, ↑x.snd)) { fst := y, snd := { val := j, isLt := hj } } →
    { fst := x, snd := { val := i, isLt := hi } } = { fst := y, snd := { val := j, isLt := hj } }
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refl
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
hi hj : i < count x m
⊢ { fst := x, snd := { val := i, isLt := hi } } = { fst := x, snd := { val := i, isLt := hj } }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : ToType m
⊢ ↑(coeEmbedding m) x ∈ toEnumFinset m
[PROOFSTEP]
rw [Multiset.mem_toEnumFinset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : ToType m
⊢ (↑(coeEmbedding m) x).snd < count (↑(coeEmbedding m) x).fst m
[PROOFSTEP]
exact x.2.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : { x // x ∈ toEnumFinset m }
⊢ (↑x).snd < count (↑x).fst m
[PROOFSTEP]
rw [← Multiset.mem_toEnumFinset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : { x // x ∈ toEnumFinset m }
⊢ ↑x ∈ toEnumFinset m
[PROOFSTEP]
exact x.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.LeftInverse
    (fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, isLt := (_ : (↑x).snd < count (↑x).fst m) } }) fun x =>
    { val := ↑(coeEmbedding m) x, property := (_ : ↑(coeEmbedding m) x ∈ toEnumFinset m) }
[PROOFSTEP]
rintro ⟨x, i, h⟩
[GOAL]
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
h : i < count x m
⊢ (fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, isLt := (_ : (↑x).snd < count (↑x).fst m) } })
      ((fun x => { val := ↑(coeEmbedding m) x, property := (_ : ↑(coeEmbedding m) x ∈ toEnumFinset m) })
        { fst := x, snd := { val := i, isLt := h } }) =
    { fst := x, snd := { val := i, isLt := h } }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.RightInverse
    (fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, isLt := (_ : (↑x).snd < count (↑x).fst m) } }) fun x =>
    { val := ↑(coeEmbedding m) x, property := (_ : ↑(coeEmbedding m) x ∈ toEnumFinset m) }
[PROOFSTEP]
rintro ⟨⟨x, i⟩, h⟩
[GOAL]
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
h : (x, i) ∈ toEnumFinset m
⊢ (fun x => { val := ↑(coeEmbedding m) x, property := (_ : ↑(coeEmbedding m) x ∈ toEnumFinset m) })
      ((fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, isLt := (_ : (↑x).snd < count (↑x).fst m) } })
        { val := (x, i), property := h }) =
    { val := (x, i), property := h }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.Embedding.trans (Equiv.toEmbedding (coeEquiv m)) (Function.Embedding.subtype fun x => x ∈ toEnumFinset m) =
    coeEmbedding m
[PROOFSTEP]
ext
[GOAL]
case h.h₁
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x✝ : ToType m
⊢ (↑(Function.Embedding.trans (Equiv.toEmbedding (coeEquiv m)) (Function.Embedding.subtype fun x => x ∈ toEnumFinset m))
        x✝).fst =
    (↑(coeEmbedding m) x✝).fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x✝ : ToType m
⊢ (↑(Function.Embedding.trans (Equiv.toEmbedding (coeEquiv m)) (Function.Embedding.subtype fun x => x ∈ toEnumFinset m))
        x✝).snd =
    (↑(coeEmbedding m) x✝).snd
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Finset.map (coeEmbedding m) Finset.univ = toEnumFinset m
[PROOFSTEP]
ext ⟨x, i⟩
[GOAL]
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
⊢ (x, i) ∈ Finset.map (coeEmbedding m) Finset.univ ↔ (x, i) ∈ toEnumFinset m
[PROOFSTEP]
simp only [Fin.exists_iff, Finset.mem_map, Finset.mem_univ, Multiset.coeEmbedding_apply, Prod.mk.inj_iff,
  exists_true_left, Multiset.exists_coe, Multiset.coe_mk, Fin.val_mk, exists_prop, exists_eq_right_right,
  exists_eq_right, Multiset.mem_toEnumFinset, iff_self_iff, true_and_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
⊢ Finset.filter (fun p => x = p.fst) (toEnumFinset m) =
    Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) } (Finset.range (count x m))
[PROOFSTEP]
ext ⟨y, i⟩
[GOAL]
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x y : α
i : ℕ
⊢ (y, i) ∈ Finset.filter (fun p => x = p.fst) (toEnumFinset m) ↔
    (y, i) ∈ Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) } (Finset.range (count x m))
[PROOFSTEP]
simp only [eq_comm, Finset.mem_filter, Multiset.mem_toEnumFinset, Finset.mem_map, Finset.mem_range,
  Function.Embedding.coeFn_mk, Prod.mk.inj_iff, exists_prop, exists_eq_right_right', and_congr_left_iff]
[GOAL]
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x y : α
i : ℕ
⊢ x = y → (i < count y m ↔ i < count x m)
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
i : ℕ
⊢ i < count x m ↔ i < count x m
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map Prod.fst (toEnumFinset m).val = m
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
x : α
⊢ count x (map Prod.fst (toEnumFinset m).val) = count x m
[PROOFSTEP]
simp only [Multiset.count_map, ← Finset.filter_val, Multiset.toEnumFinset_filter_eq, Finset.map_val, Finset.range_val,
  Multiset.card_map, Multiset.card_range]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Finset.image Prod.fst (toEnumFinset m) = toFinset m
[PROOFSTEP]
rw [Finset.image, Multiset.map_toEnumFinset_fst]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map (fun x => x.fst) Finset.univ.val = m
[PROOFSTEP]
have := m.map_toEnumFinset_fst
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
this : map Prod.fst (toEnumFinset m).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m
[PROOFSTEP]
rw [← m.map_univ_coeEmbedding] at this 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
this : map Prod.fst (Finset.map (coeEmbedding m) Finset.univ).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m
[PROOFSTEP]
simpa only [Finset.map_val, Multiset.coeEmbedding_apply, Multiset.map_map, Function.comp_apply] using this
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ : Multiset α
β : Type u_2
m : Multiset α
f : α → β
⊢ map (fun x => f x.fst) Finset.univ.val = map f m
[PROOFSTEP]
erw [← Multiset.map_map]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ : Multiset α
β : Type u_2
m : Multiset α
f : α → β
⊢ map f (map (fun x => x.fst) Finset.univ.val) = map f m
[PROOFSTEP]
rw [Multiset.map_univ_coe]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Finset.card (toEnumFinset m) = ↑card m
[PROOFSTEP]
rw [Finset.card, ← Multiset.card_map Prod.fst m.toEnumFinset.val]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ ↑card (map Prod.fst (toEnumFinset m).val) = ↑card m
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map Prod.fst (toEnumFinset m).val = m
[PROOFSTEP]
exact m.map_toEnumFinset_fst
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Fintype.card (ToType m) = ↑card m
[PROOFSTEP]
rw [Fintype.card_congr m.coeEquiv]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Fintype.card { x // x ∈ toEnumFinset m } = ↑card m
[PROOFSTEP]
simp only [Fintype.card_coe, card_toEnumFinset]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
inst✝ : CommMonoid α
m : Multiset α
⊢ prod m = ∏ x : ToType m, x.fst
[PROOFSTEP]
congr
  -- Porting note: `simp` fails with "maximum recursion depth has been reached"
[GOAL]
case e_a
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x => x.fst) Finset.univ.val
[PROOFSTEP]
erw [map_univ_coe]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
inst✝ : CommMonoid α
m : Multiset α
⊢ prod m = ∏ x in toEnumFinset m, x.fst
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x => x.fst) (toEnumFinset m).val
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_2
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x in toEnumFinset m, f x.fst x.snd = ∏ x : ToType m, f x.fst ↑x.snd
[PROOFSTEP]
rw [Fintype.prod_equiv m.coeEquiv (fun x ↦ f x x.2) fun x ↦ f x.1.1 x.1.2]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_2
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x in toEnumFinset m, f x.fst x.snd = ∏ x : { x // x ∈ toEnumFinset m }, f (↑x).fst (↑x).snd
[PROOFSTEP]
rw [← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_2
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∀ (x : ToType m), f x.fst ↑x.snd = f (↑(↑(coeEquiv m) x)).fst (↑(↑(coeEquiv m) x)).snd
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_2
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
x : ToType m
⊢ f x.fst ↑x.snd = f (↑(↑(coeEquiv m) x)).fst (↑(↑(coeEquiv m) x)).snd
[PROOFSTEP]
rfl
