awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
this : map Prod.fst (Finset.map (α := m.ToType) m.coeEmbedding Finset.univ).val = m
⊢ map (fun (x : m.ToType) ↦ x.fst (β := fun (x : α) ↦ Fin (count x m))) (Finset.val Finset.univ) = m

Tactic:
simpa only [Finset.map_val, Multiset.coeEmbedding_apply, Multiset.map_map,
    Function.comp_apply] using this

Premises used: Multiset.coeEmbedding_apply, Finset.map_val, Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_3
m : Multiset α
f : α → β
rw : map f (map (fun (x : m.ToType) ↦ x.fst (β := fun (x : α) ↦ Fin (count x m))) (Finset.val Finset.univ)) = map f m
rw₁ rw₂ : map f m = map f m
⊢ map (α := m.ToType) (f ∘ fun (x : m.ToType) ↦ x.fst (β := fun (x : α) ↦ Fin (count x m))) (Finset.val Finset.univ) =
    map f m

Tactic:
rw [← Multiset.map_map, Multiset.map_univ_coe]

Premises used: Multiset.map_univ_coe, Multiset.map_map
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_3
m : Multiset α
f : α → β
simp_rw :
  map (fun (x : m.ToType) ↦ (f ∘ Sigma.fst (β := fun (x : α) ↦ Fin (count x m))) x) (Finset.val Finset.univ) = map f m
⊢ map (fun (x : m.ToType) ↦ f (x.fst (β := fun (x : α) ↦ Fin (count x m)))) (Finset.val Finset.univ) = map f m

Tactic:
simp_rw [← Function.comp_apply (f := f)]

Premises used: Function.comp_apply
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_3
m : Multiset α
f : α → β
⊢ map (fun (x : m.ToType) ↦ (f ∘ Sigma.fst (β := fun (x : α) ↦ Fin (count x m))) x) (Finset.val Finset.univ) = map f m

Tactic:
map_univ_comp_coe m f

Premises used: Multiset.map_univ_comp_coe
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_3
m : Multiset α
f : α → β
⊢ map (fun (x : m.ToType) ↦ (f ∘ Sigma.fst (β := fun (x : α) ↦ Fin (count x m))) x) (Finset.val Finset.univ) = map f m

Tactic:
exact map_univ_comp_coe m f

Premises used: Multiset.map_univ_comp_coe
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
rw : (map Prod.fst m.toEnumFinset.val).card = m.card
⊢ m.toEnumFinset.card = m.card

Tactic:
rw [Finset.card, ← Multiset.card_map Prod.fst m.toEnumFinset.val]

Premises used: Multiset.toEnumFinset, Finset.val, Prod.fst, Finset.card, Multiset.card_map
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
e_a : map Prod.fst m.toEnumFinset.val = m
⊢ (map Prod.fst m.toEnumFinset.val).card = m.card

Tactic:
congr
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m

Tactic:
m.map_toEnumFinset_fst

Premises used: Multiset.map_toEnumFinset_fst
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m

Tactic:
exact m.map_toEnumFinset_fst

Premises used: Multiset.map_toEnumFinset_fst
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
rw : Fintype.card.{u_1} ↥m.toEnumFinset = m.card
⊢ Fintype.card.{u_1} m.ToType = m.card

Tactic:
rw [Fintype.card_congr m.coeEquiv]

Premises used: Fintype.card_congr, Multiset.coeEquiv
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ Fintype.card.{u_1} ↥m.toEnumFinset = m.card

Tactic:
simp only [Fintype.card_coe, card_toEnumFinset]

Premises used: Multiset.card_toEnumFinset, Fintype.card_coe
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
m : Multiset α
e_a : m = map (fun (x : m.ToType) ↦ x.fst (β := fun (x : α) ↦ Fin (count x m))) (Finset.val Finset.univ)
⊢ m.prod = ∏ x : m.ToType, x.fst (β := fun (x : α) ↦ Fin (count x m))

Tactic:
congr
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
m : Multiset α
⊢ m = map (fun (x : m.ToType) ↦ x.fst (β := fun (x : α) ↦ Fin (count x m))) (Finset.val Finset.univ)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
m : Multiset α
e_a : m = map (fun (x : α × ℕ) ↦ x.1) m.toEnumFinset.val
⊢ m.prod = ∏ x ∈ m.toEnumFinset, x.1

Tactic:
congr
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
m : Multiset α
⊢ m = map (fun (x : α × ℕ) ↦ x.1) m.toEnumFinset.val

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_3
inst_1 : CommMonoid β
m : Multiset α
f : α → ℕ → β
rw : Eq.{u_3 + 1} (α := β) (∏ x ∈ m.toEnumFinset, f x.1 x.2) (∏ x : ↥m.toEnumFinset, f (↑x : α × ℕ).1 (↑x : α × ℕ).2)
rw₁ :
  ∀ (x : m.ToType),
    f (x.fst (β := fun (x : α) ↦ Fin (count x m))) (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ) =
      f (↑((m.coeEquiv : (a : m.ToType) → ↥m.toEnumFinset) x) : α × ℕ).1
        (↑((m.coeEquiv : (a : m.ToType) → ↥m.toEnumFinset) x) : α × ℕ).2
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ m.toEnumFinset, f x.1 x.2)
    (∏ x : m.ToType, f (x.fst (β := fun (x : α) ↦ Fin (count x m))) (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ))

Tactic:
rw [Fintype.prod_equiv m.coeEquiv (fun x ↦ f x x.2) fun x ↦ f x.1.1 x.1.2]

Premises used: Fintype.prod_equiv, Sigma.fst, Fin.val, Prod.fst, Multiset.coeEquiv, Sigma.snd, Subtype.val, Prod.snd
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_3
inst_1 : CommMonoid β
m : Multiset α
f : α → ℕ → β
rw rw₁ :
  Eq.{u_3 + 1} (α := β) (∏ i : ↥m.toEnumFinset, f (↑i : α × ℕ).1 (↑i : α × ℕ).2)
    (∏ x : ↥m.toEnumFinset, f (↑x : α × ℕ).1 (↑x : α × ℕ).2)
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ m.toEnumFinset, f x.1 x.2) (∏ x : ↥m.toEnumFinset, f (↑x : α × ℕ).1 (↑x : α × ℕ).2)

Tactic:
rw [← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2]

Premises used: Finset.prod_coe_sort, Multiset.toEnumFinset, Prod.fst, Prod.snd
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_3
inst_1 : CommMonoid β
m : Multiset α
f : α → ℕ → β
x : m.ToType
⊢ f (x.fst (β := fun (x : α) ↦ Fin (count x m))) (↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ) =
    f (↑((m.coeEquiv : (a : m.ToType) → ↥m.toEnumFinset) x) : α × ℕ).1
      (↑((m.coeEquiv : (a : m.ToType) → ↥m.toEnumFinset) x) : α × ℕ).2

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m s t : Multiset α
h : s = t
x : s.ToType
⊢ count (x.fst (β := fun (x : α) ↦ Fin (count x s))) s = count (x.fst (β := fun (x : α) ↦ Fin (count x s))) t

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m s t : Multiset α
h : s = t
x : t.ToType
⊢ count (x.fst (β := fun (x : α) ↦ Fin (count x t))) t = count (x.fst (β := fun (x : α) ↦ Fin (count x t))) s

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
⊢ Fintype.card.{u_1} (ToType (α := α) 0) = 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
⊢ Fintype.card.{u_1} (ToType (α := α) ∅) = 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h :
  ¬(x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
      (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m)
pos :
  ∀ (hv : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v),
    (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) <
      count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m
neg :
  ∀ (hv : ¬x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v),
    (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) <
      count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) <
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m

Tactic:
by_cases hv : x.1 = v

Premises used: Sigma.fst
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h :
  ¬(x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
      (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m)
hv : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
pos :
  ∀ (h : ¬(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m),
    (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) < count v m
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) <
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m

Tactic:
simp only [hv, true_and] at h ⊢

Premises used: true_and
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hv : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
h : ¬(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m
apply : (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) < count v m + 1
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) < count v m

Tactic:
apply lt_of_le_of_ne (Nat.le_of_lt_add_one _) h

Premises used: Nat.le_of_lt_add_one, lt_of_le_of_ne
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hv : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
h : ¬(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) <
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) (v ::ₘ 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 : Multiset α
v : α
x : (v ::ₘ m).ToType
hv : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
h : ¬(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m
h₁ : count v m + 1 = count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) (v ::ₘ m)
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) < count v m + 1

Tactic:
convert! x.2.2 using 1

Premises used: Fin.isLt, Sigma.snd
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hv : x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
h : ¬(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m
⊢ count v m + 1 = count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) (v ::ₘ m)

Tactic:
simp [hv]
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h :
  ¬(x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
      (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m)
hv : ¬x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) <
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) (v ::ₘ 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 : Multiset α
v : α
x : (v ::ₘ m).ToType
h :
  ¬(x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
      (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m)
hv : ¬x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
h₁ :
  count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m =
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) (v ::ₘ m)
⊢ (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) <
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m

Tactic:
convert! x.2.2 using 1

Premises used: Fin.isLt, Sigma.snd
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h :
  ¬(x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
      (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m)
hv : ¬x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
⊢ count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m =
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) (v ::ₘ m)

Tactic:
(count_cons_of_ne hv _).symm

Premises used: Multiset.count_cons_of_ne, Eq.symm
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h :
  ¬(x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
      (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m)
hv : ¬x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v
⊢ count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m =
    count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) (v ::ₘ m)

Tactic:
exact (count_cons_of_ne hv _).symm

Premises used: Multiset.count_cons_of_ne, Eq.symm
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : Option m.ToType
⊢ count v m < count v (v ::ₘ m)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
dsimp :
  Eq (α := (v ::ₘ m).ToType)
    (Option.elim
      (if h : x = v ∧ (↑hx : ℕ) = count v m then none
      else some (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨(↑hx : ℕ), ⋯⟩ : Fin (count x m))))
      (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
      fun (x : m.ToType) ↦
      Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
        (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))))
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) x hx)
⊢ Eq (α := (v ::ₘ m).ToType)
    ((fun (x : Option m.ToType) ↦
        (x.elim (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
            fun (x : m.ToType) ↦
            Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
              (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))) :
          (v ::ₘ m).ToType))
      ((fun (x : (v ::ₘ m).ToType) ↦
          (if h :
                x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
                  (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m then
              none
            else
              some
                (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
                  (⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ), ⋯⟩ :
                    Fin (count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m))) :
            Option m.ToType))
        (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) x hx)))
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) x hx)

Tactic:
dsimp only
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
isTrue :
  x = v ∧ (↑hx : ℕ) = count v m →
    Eq (α := (v ::ₘ m).ToType)
      (Option.elim none
        (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
        fun (x : m.ToType) ↦
        Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
          (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))))
      (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) x hx)
isFalse :
  ∀ (h : ¬(x = v ∧ (↑hx : ℕ) = count v m)),
    Eq (α := (v ::ₘ m).ToType)
      (Option.elim (some (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨(↑hx : ℕ), ⋯⟩ : Fin (count x m))))
        (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
        fun (x : m.ToType) ↦
        Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
          (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))))
      (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) x hx)
⊢ Eq (α := (v ::ₘ m).ToType)
    (Option.elim
      (if h : x = v ∧ (↑hx : ℕ) = count v m then none
      else some (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨(↑hx : ℕ), ⋯⟩ : Fin (count x m))))
      (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
      fun (x : m.ToType) ↦
      Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
        (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))))
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) x hx)

Tactic:
split
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
h : x = v ∧ (↑hx : ℕ) = count v m
isTrue :
  ∀ (hx : Fin (count x (x ::ₘ m))) (h2 : (↑hx : ℕ) = count x m),
    Eq (α := (x ::ₘ m).ToType)
      (Option.elim none
        (Sigma.mk (β := fun (x_1 : α) ↦ Fin (count x_1 (x ::ₘ m))) x (⟨count x m, ⋯⟩ : Fin (count x (x ::ₘ m))))
        fun (x_1 : m.ToType) ↦
        Sigma.mk (β := fun (x_2 : α) ↦ Fin (count x_2 (x ::ₘ m))) (x_1.fst (β := fun (x : α) ↦ Fin (count x m)))
          (Fin.castLE ⋯ (x_1.snd (β := fun (x : α) ↦ Fin (count x m)))))
      (Sigma.mk (β := fun (x_1 : α) ↦ Fin (count x_1 (x ::ₘ m))) x hx)
⊢ Eq (α := (v ::ₘ m).ToType)
    (Option.elim none
      (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
      fun (x : m.ToType) ↦
      Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
        (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))))
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) x hx)

Tactic:
obtain ⟨rfl, h2⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
x : α
hx : Fin (count x (x ::ₘ m))
h2 : (↑hx : ℕ) = count x m
⊢ Eq (α := (x ::ₘ m).ToType)
    (Option.elim none
      (Sigma.mk (β := fun (x_1 : α) ↦ Fin (count x_1 (x ::ₘ m))) x (⟨count x m, ⋯⟩ : Fin (count x (x ::ₘ m))))
      fun (x_1 : m.ToType) ↦
      Sigma.mk (β := fun (x_2 : α) ↦ Fin (count x_2 (x ::ₘ m))) (x_1.fst (β := fun (x : α) ↦ Fin (count x m)))
        (Fin.castLE ⋯ (x_1.snd (β := fun (x : α) ↦ Fin (count x m)))))
    (Sigma.mk (β := fun (x_1 : α) ↦ Fin (count x_1 (x ::ₘ m))) x hx)

Tactic:
simp [← h2]
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
h : ¬(x = v ∧ (↑hx : ℕ) = count v m)
⊢ Eq (α := (v ::ₘ m).ToType)
    (Option.elim (some (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) x (⟨(↑hx : ℕ), ⋯⟩ : Fin (count x m))))
      (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
      fun (x : m.ToType) ↦
      Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
        (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))))
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) x hx)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
⊢ Eq.{u_1 + 1} (α := Option m.ToType)
    ((fun (x : (v ::ₘ m).ToType) ↦
        (if h :
              x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
                (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m then
            none
          else
            some
              (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
                (⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ), ⋯⟩ :
                  Fin (count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m))) :
          Option m.ToType))
      ((fun (x : Option m.ToType) ↦
          (x.elim (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
              fun (x : m.ToType) ↦
              Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
                (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))) :
            (v ::ₘ m).ToType))
        none))
    none

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m : Multiset α
v : α
x : m.ToType
some : x.fst (β := fun (x : α) ↦ Fin (count x m)) = v → ¬(↑(x.snd (β := fun (x : α) ↦ Fin (count x m))) : ℕ) = count v m
⊢ (fun (x : (v ::ₘ m).ToType) ↦
        (if h :
              x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) = v ∧
                (↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ) = count v m then
            none
          else
            Option.some
              (Sigma.mk (β := fun (x : α) ↦ Fin (count x m)) (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))))
                (⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) : ℕ), ⋯⟩ :
                  Fin (count (x.fst (β := fun (x : α) ↦ Fin (count x (v ::ₘ m)))) m))) :
          Option m.ToType))
      ((fun (x : Option m.ToType) ↦
          (x.elim (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v (⟨count v m, ⋯⟩ : Fin (count v (v ::ₘ m))))
              fun (x : m.ToType) ↦
              Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
                (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))) :
            (v ::ₘ m).ToType))
        (Option.some x)) =
    Option.some x

Tactic:
simp only [Option.elim_some, Fin.val_castLE, Fin.eta, Sigma.eta, dite_eq_ite,
        ite_eq_right_iff, reduceCtorEq, imp_false, not_and]

Premises used: reduceCtorEq, imp_false, Sigma.eta, Fin.eta, Option.elim_some, ite_eq_right_iff, dite_eq_ite, not_and, Fin.val_castLE
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : 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:
x.2.2.ne

Premises used: Fin.isLt, Sigma.snd, LT.lt.ne
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : 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:
exact x.2.2.ne

Premises used: Fin.isLt, Sigma.snd, LT.lt.ne
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
v : α
⊢ Eq.{u_1 + 1} (α := (v ::ₘ m).ToType)
    ((Equiv.symm consEquiv : (a : Option m.ToType) → (v ::ₘ m).ToType) none : (v ::ₘ m).ToType)
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) v ⟨count v m, ⋯⟩ : (x : α) × Fin (count x (v ::ₘ m)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
v : α
x : m.ToType
⊢ Eq (α := (v ::ₘ m).ToType)
    ((Equiv.symm consEquiv : (a : Option m.ToType) → (v ::ₘ m).ToType) (some x) : (v ::ₘ m).ToType)
    (Sigma.mk (β := fun (x : α) ↦ Fin (count x (v ::ₘ m))) (x.fst (β := fun (x : α) ↦ Fin (count x m)))
        (Fin.castLE ⋯ (x.snd (β := fun (x : α) ↦ Fin (count x m)))) :
      (x : α) × Fin (count x (v ::ₘ m)))

Tactic:
rfl

Premises used: rfl