awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ≤ s

Tactic:
(le_ndinter.1 le_rfl).1

Premises used: le_rfl, Multiset.le_ndinter, And.left, Iff.mp
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ s

Tactic:
subset_of_le (ndinter_le_left s t)

Premises used: Multiset.subset_of_le, Multiset.ndinter_le_left
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ t

Tactic:
(le_ndinter.1 le_rfl).2

Premises used: le_rfl, Multiset.le_ndinter, And.right, Iff.mp
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ s.ndinter t ≤ t

Tactic:
(le_iff_subset <| d.ndinter _).2 <| ndinter_subset_right _ _

Premises used: Multiset.le_iff_subset, Iff.mpr, Multiset.Nodup.ndinter, Multiset.ndinter_subset_right
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∩ t ≤ s.ndinter t

Tactic:
le_ndinter.2 ⟨inter_le_left, subset_of_le inter_le_right⟩

Premises used: Iff.mpr, Multiset.subset_of_le, Multiset.le_ndinter, Multiset.inter_le_right, And.intro, Multiset.inter_le_left
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ s.ndinter t = s ∩ t

Tactic:
le_antisymm (le_inter (ndinter_le_left _ _) (ndinter_le_right _ d)) (inter_le_ndinter _ _)

Premises used: Multiset.ndinter_le_left, Multiset.le_inter, le_antisymm, Multiset.inter_le_ndinter, Multiset.ndinter_le_right
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
d : s.Nodup
rw : (s.ndinter t).Nodup
⊢ (s ∩ t).Nodup

Tactic:
rw [← ndinter_eq_inter d]

Premises used: Multiset.ndinter_eq_inter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s.ndinter t).Nodup

Tactic:
d.filter _

Premises used: Multiset.Nodup.filter, Multiset.ndinter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s.ndinter t).Nodup

Tactic:
exact d.filter _

Premises used: Multiset.Nodup.filter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
rw : s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t
⊢ s.ndinter t = 0 ↔ _root_.Disjoint s t

Tactic:
rw [← subset_zero]

Premises used: Multiset.subset_zero
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t

Tactic:
simp [subset_iff, disjoint_left]

Premises used: Multiset.disjoint_left, Multiset.subset_iff
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ⊆ t
h₁ :
  ∀ (a b : List α)
    (h :
      Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)),
    ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
      Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a
⊢ s.ndinter t = s

Tactic:
induction s, t using Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
h₁ : (↑a : Multiset α).ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) = (↑a : Multiset α)
h₂ : (↑a : Multiset α).ndinter (↑b : Multiset α) = (↑a : Multiset α)
h₃ : (↑(a ∩ b) : Multiset α) = (↑a : Multiset α)
h₄ h₅ : (↑a : Multiset α) = (↑a : Multiset α)
⊢ ndinter (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a

Tactic:
rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]

Premises used: List.Subset.inter_eq_left, Multiset.coe_ndinter, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
x : α
i : Fin (count x m)
⊢ (m.mkToType x i).fst (β := fun (x : α) ↦ Fin (count x m)) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
x : m.ToType
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ) < count (x.fst (β := fun (x : α) ↦ Fin (count x m))) m

Tactic:
have := x.2.2
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
x : m.ToType
this : (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ) < count (x.fst (β := fun (x : α) ↦ Fin (count x m))) m
⊢ 0 < count (x.fst (β := fun (x : α) ↦ Fin (count x m))) m

Tactic:
lia
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
p : m.ToType → Prop
⊢ (∀ (x : m.ToType), p x) ↔ ∀ (x : α) (i : Fin (count x m)), p (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x i)

Tactic:
Sigma.forall

Premises used: Sigma.forall, Multiset.ToType
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
p : m.ToType → Prop
⊢ (∃ (x : m.ToType), p x) ↔ ∃ (x : α) (i : Fin (count x m)), p (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x i)

Tactic:
Sigma.exists

Premises used: Sigma.exists, Multiset.ToType
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
x : α
hx : x ∈ (↑m.toFinset : Set α)
y : α
hy : y ∈ (↑m.toFinset : Set α)
hxy : x ≠ y
⊢ Function.onFun (β := Finset (α × ℕ)) Disjoint
    (fun (x : α) ↦ Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (count x m))) x y

Tactic:
simp [Function.onFun, Finset.disjoint_right, hxy]

Premises used: Function.onFun, Finset.disjoint_right
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
x : α
i : ℕ
simp_rw : (∃ a ∈ m, ∃ a_1 < count a m, a = x ∧ a_1 = i) ↔ i < count x m
⊢ Membership.mem (γ := Finset (α × ℕ))
      (m.toFinset.disjiUnion (fun (x : α) ↦ Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (count x m))) ⋯)
      (x, i) ↔
    Membership.mem (γ := Set (α × ℕ)) {p : α × ℕ | p.2 < count p.1 m} (x, i)

Tactic:
simp_rw [Finset.mem_disjiUnion, Multiset.mem_toFinset, Finset.mem_map, Finset.mem_range,
        Function.Embedding.coeFn_mk, Prod.mk_inj, Set.mem_setOf_eq]

Premises used: Prod.mk_inj, Set.mem_setOf_eq, Finset.mem_range, Finset.mem_disjiUnion, Function.Embedding.coeFn_mk, Finset.mem_map, Multiset.mem_toFinset
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
x : α
i : ℕ
simp : i < count x m → x ∈ m
⊢ (∃ a ∈ m, ∃ a_1 < count a m, a = x ∧ a_1 = i) ↔ i < count x m

Tactic:
simp only [← and_assoc, exists_eq_right, and_iff_right_iff_imp]

Premises used: exists_eq_right, and_iff_right_iff_imp, and_assoc
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
x : α
i : ℕ
h : i < count x m
⊢ 0 < count x m

Tactic:
lia
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ i < count x m → x ∈ m

Tactic:
exact fun h ↦ Multiset.count_pos.mp (by lia)

Premises used: Multiset.count_pos, Iff.mp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
p : α × ℕ
⊢ p ∈ m.toEnumFinset ↔ p.2 < count p.1 m

Tactic:
Set.mem_toFinset

Premises used: Set.Mem, setOf, Set.mem_toFinset, Nat.lt
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
p : α × ℕ
h : p ∈ m.toEnumFinset
this : p.2 < count p.1 m
⊢ 0 < count p.1 m

Tactic:
lia
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
a : α
⊢ {x ∈ m.toEnumFinset | x.1 = a} = SProd.sprod (α := Finset α) {a} (Finset.range (count a m))

Tactic:
aesop
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
a : ∀ (a : α), count a (map Prod.fst m.toEnumFinset.val) = count a m
⊢ map Prod.fst m.toEnumFinset.val = m

Tactic:
ext a
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
a : α
⊢ count a (map Prod.fst m.toEnumFinset.val) = count a m

Tactic:
simp [count_map, ← Finset.filter_val, eq_comm (a := a)]

Premises used: eq_comm, Multiset.count_map, Finset.filter_val
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
rw : (map Prod.fst m.toEnumFinset.val).toFinset = m.toFinset
rw₁ rw₂ : m.toFinset = m.toFinset
⊢ Finset.image Prod.fst m.toEnumFinset = m.toFinset

Tactic:
rw [Finset.image, Multiset.map_toEnumFinset_fst]

Premises used: Multiset.map_toEnumFinset_fst, Finset.image
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
simp_rw : ∀ (a : α), (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m
⊢ map Prod.fst s.val ≤ m

Tactic:
simp_rw [le_iff_count, count_map]

Premises used: Multiset.le_iff_count, Multiset.count_map
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
inl :
  ∀ (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
inr :
  ∀ (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
⊢ (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

Premises used: Finset.val, Multiset.card, Eq, Nat.eq_zero_or_pos, Multiset.filter
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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
inl : 0 ≤ count a m
⊢ (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m

Tactic:
rw [ha]
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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 _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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
by_contra! : ∀ (h : ∀ (n : ℕ) (_ : n ≥ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1), (a, n) ∉ s), False
⊢ ∃ n ≥ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1, (a, n) ∈ s

Tactic:
by_contra! h
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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 : ℕ) (_ : n ≥ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1), (a, n) ∉ s
⊢ {x ∈ s | x.1 = a} ⊆
    SProd.sprod (α := Finset α) {a} (Finset.range ((filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1))

Tactic:
simpa +contextual [forall_comm (β := _ = a), Finset.subset_iff,
        imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using h

Premises used: not_le, Nat.lt_sub_iff_add_lt, forall_comm, imp_not_comm, Finset.subset_iff
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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 : ℕ) (_ : n ≥ (filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1), (a, n) ∉ s
⊢ {x ∈ s | x.1 = a} ⊆
    SProd.sprod (α := Finset α) {a} (Finset.range ((filter (fun (x : α × ℕ) ↦ a = x.1) s.val).card - 1))

Tactic:
replace h : {x ∈ s | x.1 = a} ⊆ {a} ×ˢ .range (card (s.1.filter fun x ↦ a = x.1) - 1) := by
      simpa +contextual [forall_comm (β := _ = a), Finset.subset_iff,
        imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using h
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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 :
  {x ∈ s | x.1 = a} ⊆
    SProd.sprod (α := Finset α) {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

Premises used: eq_comm, Finset.card, Finset.card_mono
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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 :
  {x ∈ s | x.1 = a} ⊆
    SProd.sprod (α := Finset α) {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:
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
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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 :
  {x ∈ s | x.1 = a} ⊆
    SProd.sprod (α := Finset α) {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:
lia
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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
inr :
  ∀ (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
⊢ (filter (fun (a_1 : α × ℕ) ↦ a = a_1.1) s.val).card ≤ count a m

Tactic:
obtain ⟨n, han, hn⟩ : ∃ n ≥ card (s.1.filter fun x ↦ a = x.1) - 1, (a, n) ∈ s := by
    by_contra! h
    replace h : {x ∈ s | x.1 = a} ⊆ {a} ×ˢ .range (card (s.1.filter fun x ↦ a = x.1) - 1) := by
      simpa +contextual [forall_comm (β := _ = a), Finset.subset_iff,
        imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using h
    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
    lia

Premises used: Finset.val, Multiset.card, Eq, Multiset.filter
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : 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)

Premises used: Nat.le_of_pred_lt, LE.le.trans_lt
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
simp : p.2 < count p.1 m₁ → p.2 < count p.1 m₂
⊢ p ∈ m₁.toEnumFinset → p ∈ m₂.toEnumFinset

Tactic:
simp only [Multiset.mem_toEnumFinset]

Premises used: Multiset.mem_toEnumFinset
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.2 < count p.1 m₁ → p.2 < count p.1 m₂

Tactic:
lt_of_le_of_lt' (Multiset.le_iff_count.mp h p.1)

Premises used: Multiset.le_iff_count, lt_of_le_of_lt', Prod.fst, Iff.mp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.2 < count p.1 m₁ → p.2 < count p.1 m₂

Tactic:
exact lt_of_le_of_lt' (Multiset.le_iff_count.mp h p.1)

Premises used: Multiset.le_iff_count, lt_of_le_of_lt', Prod.fst, Iff.mp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m₁ m₂ : Multiset α
h : m₁.toEnumFinset ⊆ m₂.toEnumFinset
⊢ m₁ ≤ m₂

Tactic:
simpa using map_fst_le_of_subset_toEnumFinset h

Premises used: Multiset.map_fst_le_of_subset_toEnumFinset
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
x : α
i : ℕ
hi : i < count x m
this :
  ∀ (y : α) (j : ℕ) (hj : j < count y m),
    Eq.{u_1 + 1} (α := α × ℕ)
        ((fun (x : m.ToType) ↦
            (x.fst (β := fun (x : α) ↦ Fin (count x m)), (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ)))
          (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨i, hi⟩ : Fin (count x m))))
        ((fun (x : m.ToType) ↦
            (x.fst (β := fun (x : α) ↦ Fin (count x m)), (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ)))
          (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) y (⟨j, hj⟩ : Fin (count y m)))) →
      Eq (α := m.ToType) (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨i, hi⟩ : Fin (count x m)))
        (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) y (⟨j, hj⟩ : Fin (count y m)))
⊢ ∀ ⦃a₂ : m.ToType⦄,
    Eq.{u_1 + 1} (α := α × ℕ)
        ((fun (x : m.ToType) ↦
            (x.fst (β := fun (x : α) ↦ Fin (count x m)), (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ)))
          (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨i, hi⟩ : Fin (count x m))))
        ((fun (x : m.ToType) ↦
            (x.fst (β := fun (x : α) ↦ Fin (count x m)), (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ)))
          a₂) →
      Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨i, hi⟩ : Fin (count x m)) = a₂

Tactic:
⟨y, j, hj⟩
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
x : α
i : ℕ
hi hj : i < count x m
⊢ Eq (α := m.ToType) (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨i, hi⟩ : Fin (count x m)))
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨i, hj⟩ : Fin (count x m)))

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
x : m.ToType
rw : ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).2 < count ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).1 m
⊢ Membership.mem (α := α × ℕ) m.toEnumFinset ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x : α × ℕ)

Tactic:
rw [Multiset.mem_toEnumFinset]

Premises used: Multiset.mem_toEnumFinset
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
x : m.ToType
⊢ ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).2 < count ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).1 m

Tactic:
x.2.2

Premises used: Fin.isLt, Sigma.snd
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
x : m.ToType
⊢ ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).2 < count ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).1 m

Tactic:
exact x.2.2

Premises used: Fin.isLt, Sigma.snd
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
x : ↥m.toEnumFinset
rw : (↑x : α × ℕ) ∈ m.toEnumFinset
⊢ (↑x : α × ℕ).2 < count (↑x : α × ℕ).1 m

Tactic:
rw [← Multiset.mem_toEnumFinset]

Premises used: Multiset.mem_toEnumFinset
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
x : ↥m.toEnumFinset
⊢ (↑x : α × ℕ) ∈ m.toEnumFinset

Tactic:
x.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
x : ↥m.toEnumFinset
⊢ (↑x : α × ℕ) ∈ m.toEnumFinset

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
h :
  ∀ (x : m.ToType),
    Eq.{u_1 + 1} (α := α)
      ((Function.Embedding.trans (Equiv.toEmbedding m.coeEquiv)
              (Function.Embedding.subtype fun (x : α × ℕ) ↦ x ∈ m.toEnumFinset) :
            (a : m.ToType) → α × ℕ)
          x).1
      ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).1
h₁ :
  ∀ (x : m.ToType),
    Eq (α := ℕ)
      ((Function.Embedding.trans (Equiv.toEmbedding m.coeEquiv)
              (Function.Embedding.subtype fun (x : α × ℕ) ↦ x ∈ m.toEnumFinset) :
            (a : m.ToType) → α × ℕ)
          x).2
      ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).2
⊢ Eq (α := m.ToType ↪ α × ℕ)
    (Function.Embedding.trans (Equiv.toEmbedding m.coeEquiv)
      (Function.Embedding.subtype fun (x : α × ℕ) ↦ x ∈ m.toEnumFinset))
    m.coeEmbedding

Tactic:
ext
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
x : m.ToType
⊢ Eq.{u_1 + 1} (α := α)
    ((Function.Embedding.trans (Equiv.toEmbedding m.coeEquiv)
            (Function.Embedding.subtype fun (x : α × ℕ) ↦ x ∈ m.toEnumFinset) :
          (a : m.ToType) → α × ℕ)
        x).1
    ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).1

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
x : m.ToType
⊢ Eq (α := ℕ)
    ((Function.Embedding.trans (Equiv.toEmbedding m.coeEquiv)
            (Function.Embedding.subtype fun (x : α × ℕ) ↦ x ∈ m.toEnumFinset) :
          (a : m.ToType) → α × ℕ)
        x).2
    ((m.coeEmbedding : (a : m.ToType) → α × ℕ) x).2

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
h : ∀ (x : α) (i : ℕ), (x, i) ∈ Finset.map (α := m.ToType) m.coeEmbedding Finset.univ ↔ (x, i) ∈ m.toEnumFinset
⊢ Finset.map (α := m.ToType) m.coeEmbedding Finset.univ = m.toEnumFinset

Tactic:
ext ⟨x, i⟩
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ (x, i) ∈ Finset.map (α := m.ToType) m.coeEmbedding Finset.univ ↔ (x, i) ∈ m.toEnumFinset

Tactic:
simp only [Fin.exists_iff, Finset.mem_map, Finset.mem_univ, Multiset.coeEmbedding_apply,
    Prod.mk_inj, Multiset.exists_coe, Multiset.coe_mk,
    exists_prop, exists_eq_right_right, exists_eq_right, Multiset.mem_toEnumFinset, true_and]

Premises used: Finset.mem_univ, exists_eq_right_right, Multiset.coeEmbedding_apply, Prod.mk_inj, exists_eq_right, exists_prop, Multiset.mem_toEnumFinset, Multiset.coe_mk, Fin.exists_iff, Finset.mem_map, true_and, Multiset.exists_coe
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m

Tactic:
have := m.map_toEnumFinset_fst
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
this : map Prod.fst m.toEnumFinset.val = m
⊢ map Prod.fst (Finset.map (α := m.ToType) m.coeEmbedding Finset.univ).val = m

Tactic:
rw [← m.map_univ_coeEmbedding] at this

Premises used: Multiset.map_univ_coeEmbedding