-- Module: Mathlib.Data.Multiset.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
m_1 m : Multiset α
f : α → β
l : List α
a : α
s : List α
x_1 :
  { v : Equiv.{u_1 + 1, u_2 + 1} (ToType ⟦s⟧) (map f ⟦s⟧).ToType //
    ∀ (a : ToType ⟦s⟧),
      Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))) ((v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType) a) =
        f (a.fst (β := fun (x : α) ↦ Fin (count x ⟦s⟧))) }
v : Equiv.{u_1 + 1, u_2 + 1} (ToType ⟦s⟧) (map f ⟦s⟧).ToType
hv :
  ∀ (a : ToType ⟦s⟧),
    Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))) ((v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType) a) =
      f (a.fst (β := fun (x : α) ↦ Fin (count x ⟦s⟧)))
x : ToType ⟦a :: s⟧
isTrue :
  x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))) = a ∧
      (↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ) = count a ⟦s⟧ →
    Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦a :: s⟧)))
        ((Equiv.symm (cast ⋯) : (a_1 : (f a ::ₘ map f ⟦s⟧).ToType) → (map f ⟦a :: s⟧).ToType)
          (Option.elim (Option.map.{u_1, u_2} (α := ToType ⟦s⟧) (⇑v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType) none)
            (Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧))) (f a)
              (⟨count (f a) (map f ⟦s⟧), ⋯⟩ : Fin (count (f a) (f a ::ₘ map f ⟦s⟧))))
            fun (x : (map f ⟦s⟧).ToType) ↦
            Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧)))
              (x.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))
              (Fin.castLE ⋯ (x.snd (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))))) =
      f (x.fst (β := fun (x : α) ↦ Fin (count x ⟦a :: s⟧)))
isFalse :
  ∀
    (h :
      ¬(x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))) = a ∧
          (↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ) = count a ⟦s⟧)),
    Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦a :: s⟧)))
        ((Equiv.symm (cast ⋯) : (a_1 : (f a ::ₘ map f ⟦s⟧).ToType) → (map f ⟦a :: s⟧).ToType)
          (Option.elim
            (Option.map (α := ToType ⟦s⟧) (⇑v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType)
              (some
                (Sigma.mk (β := fun (x : α) ↦ Fin (count x ⟦s⟧)) (x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))))
                  ⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ), ⋯⟩)))
            (Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧))) (f a)
              (⟨count (f a) (map f ⟦s⟧), ⋯⟩ : Fin (count (f a) (f a ::ₘ map f ⟦s⟧))))
            fun (x : (map f ⟦s⟧).ToType) ↦
            Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧)))
              (x.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))
              (Fin.castLE ⋯ (x.snd (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))))) =
      f (x.fst (β := fun (x : α) ↦ Fin (count x ⟦a :: s⟧)))
⊢ Sigma.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦a :: s⟧)))
      ((Equiv.symm (cast ⋯) : (a_1 : (f a ::ₘ map f ⟦s⟧).ToType) → (map f ⟦a :: s⟧).ToType)
        (Option.elim
          (Option.map.{u_1, u_2} (α := ToType ⟦s⟧) (⇑v : (a : ToType ⟦s⟧) → (map f ⟦s⟧).ToType)
            (if h :
                x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))) = a ∧
                  (↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ) = count a ⟦s⟧ then
              none
            else
              some
                (Sigma.mk (β := fun (x : α) ↦ Fin (count x ⟦s⟧)) (x.fst (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧))))
                  ⟨(↑(x.snd (β := fun (x : α) ↦ Fin (count x (a ::ₘ ⟦s⟧)))) : ℕ), ⋯⟩)))
          (Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧))) (f a)
            (⟨count (f a) (map f ⟦s⟧), ⋯⟩ : Fin (count (f a) (f a ::ₘ map f ⟦s⟧))))
          fun (x : (map f ⟦s⟧).ToType) ↦
          Sigma.mk (β := fun (x : β) ↦ Fin (count x (f a ::ₘ map f ⟦s⟧)))
            (x.fst (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))
            (Fin.castLE ⋯ (x.snd (β := fun (x : β) ↦ Fin (count x (map f ⟦s⟧))))))) =
    f (x.fst (β := fun (x : α) ↦ Fin (count x ⟦a :: s⟧)))

Tactic:
split