Don't understand type mismatch

Stream: new members

[Pim Otte]

In the example below, the approach I want to take is to rewrite the sum to separate out the zero's using finset.sum_erase_add, but I'm getting a type mismatch. I tried using @, but that gives an even more confusing type mismatch. Any pointers? (Or alternative routes to prove this example)

import data.finsupp.basic
import set_theory.zfc.basic



example (m : (fin 2) →₀ ℕ) : (m.support.sum (λ (i : fin 2), m i) = 2) → m 0 + m 1 = 2:=
begin
    have zero_ne_one_fin2 : ((0 : (fin 2)) ≠ (1 : (fin 2))),
    {
        simp only [ne.def, fin.zero_eq_one_iff, nat.one_ne_zero, not_false_iff],
    },
    intros h,
    rw ← finset.sum_pair zero_ne_one_fin2,
    rw ← @finset.sum_insert_of_eq_zero_if_not_mem ℕ (fin 2) m.support 0 m nat.add_comm_monoid (fin.decidable_eq 2) (finsupp.not_mem_support_iff.mp) at h,

    simp_rw ← h,
    have factoid : (0 : (fin 2)) ∈ ({(0 : (fin 2)), (1 : (fin 2))} : set (fin 2)),
    {
      refine set.mem_insert (0 : (fin 2)) {1},
    },

    --rw ← @finset.sum_erase_add ℕ (fin 2) nat.add_comm_monoid (fin.decidable_eq 2) {0, 1} m 0 factoid,
    rw ← finset.sum_erase_add {(0 : (fin 2)), (1 : (fin 2))} m factoid,

    -- type mismatch at application
    -- {0, 1}.sum_erase_add ⇑m factoid
    -- term
    -- factoid
    -- has type
    -- 0 ∈ {0, 1}
    -- but is expected to have type
    -- ?m_1 ∈ {0, 1}

    sorry,
end

[Kevin Buzzard]

I think the issue is this: finset and set are unrelated types. Your factoid is a statement about a set but finset.sum_erase_add wants to eat various things about finsets so it will choke on factoid.

[Kevin Buzzard]

    have factoid : (0 : (fin 2)) ∈ ({0, 1} : finset (fin 2)),
    { rw finset.mem_insert, left, refl, },

    rw ← finset.sum_erase_add _ m factoid,
    -- works

[Pim Otte]

Ah, I get it now. Thanks a lot:)

[Eric Wieser]

You might also want to solve this via docs#fin.sum_univ_two