Stream: new members

Topic: Don't understand type mismatch

Pim Otte (Aug 06 2022 at 13:38):

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
-- term
-- factoid
-- has type
-- 0 ∈ {0, 1}
-- but is expected to have type
-- ?m_1 ∈ {0, 1}

sorry,
end


Kevin Buzzard (Aug 06 2022 at 14:01):

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 (Aug 06 2022 at 14:02):

    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 (Aug 06 2022 at 14:05):

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

Eric Wieser (Aug 07 2022 at 13:28):

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

Last updated: Dec 20 2023 at 11:08 UTC