Multiset.Pi.cons_ne

theorem Multiset.Pi.cons_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort v} {m : Multiset α} {a a' : α} {b : δ a} {f : (a : α) → a ∈ m → δ a} (h' : a' ∈ a ::ₘ m) (h : a' ≠ a), Multiset.Pi.cons m a b f a' h' = f a' ⋯

The theorem `Multiset.Pi.cons_ne` states that for any type `α` with decidable equality, a function `δ` from `α` to any sort `v`, a multiset `m` of `α`, elements `a` and `a'` of `α`, a term `b` of type `δ a`, and a function `f` mapping any element `a` of `α` in the multiset `m` to `δ a`: if `a'` belongs to multiset created by adding `a` to `m` (`a ::ₘ m`) and `a'` is not equal to `a`, then the `Multiset.Pi.cons` function applied to `m`, `a`, `b`, `f`, `a'`, and the proof that `a'` belongs to `a ::ₘ m` equals the application of function `f` to `a'` and the proof that `a'` belongs to `m`. In other words, `Multiset.Pi.cons` behaves like function `f` for elements not equal to the one being inserted.

More concisely: For any type `α` with decidable equality, multiset `m` of `α`, function `δ : α →* any sort v`, function `f : α → δ`, `a` and `a'` in `α`, if `a'` is in `m` after adding `a` (`a :: m`) and `a ≠ a'`, then `Multiset.Pi.cons m a b f a' (in_multiset! a' (insert a m)) = f a' (in_multiset! a' m)`.