[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ List.NodupKeys (List.map Prod.toSigma (Finset.toList (graph f)))
[PROOFSTEP]
rw [List.NodupKeys, List.keys, List.map_map, Prod.fst_comp_toSigma, List.nodup_map_iff_inj_on]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ ∀ (x : α × M), x ∈ Finset.toList (graph f) → ∀ (y : α × M), y ∈ Finset.toList (graph f) → x.fst = y.fst → x = y
[PROOFSTEP]
rintro ⟨b, m⟩ hb ⟨c, n⟩ hc (rfl : b = c)
[GOAL]
case mk.mk
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : (b, m) ∈ Finset.toList (graph f)
n : M
hc : (b, n) ∈ Finset.toList (graph f)
⊢ (b, m) = (b, n)
[PROOFSTEP]
rw [Finset.mem_toList, Finsupp.mem_graph_iff] at hb hc 
[GOAL]
case mk.mk
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : ↑f (b, m).fst = (b, m).snd ∧ (b, m).snd ≠ 0
n : M
hc : ↑f (b, n).fst = (b, n).snd ∧ (b, n).snd ≠ 0
⊢ (b, m) = (b, n)
[PROOFSTEP]
dsimp at hb hc 
[GOAL]
case mk.mk
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : ↑f b = m ∧ ¬m = 0
n : M
hc : ↑f b = n ∧ ¬n = 0
⊢ (b, m) = (b, n)
[PROOFSTEP]
rw [← hc.1, hb.1]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ List.Nodup (Finset.toList (graph f))
[PROOFSTEP]
apply Finset.nodup_toList
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ List.toFinset (AList.keys (toAList f)) = f.support
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a✝ : α
⊢ a✝ ∈ List.toFinset (AList.keys (toAList f)) ↔ a✝ ∈ f.support
[PROOFSTEP]
simp [toAList, AList.mem_keys, AList.keys, List.keys]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ toAList f ↔ ↑f x ≠ 0
[PROOFSTEP]
classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ toAList f ↔ ↑f x ≠ 0
[PROOFSTEP]
rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
⊢ Finset α
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
this : DecidableEq α
⊢ Finset α
[PROOFSTEP]
haveI := Classical.decEq M
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
this✝ : DecidableEq α
this : DecidableEq M
⊢ Finset α
[PROOFSTEP]
exact (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
⊢ a ∈ toFinset (List.keys (filter (fun x => decide (x.snd ≠ 0)) l.entries)) ↔
    (fun a => Option.getD (lookup a l) 0) a ≠ 0
[PROOFSTEP]
classical
simp_rw [@mem_toFinset _ _, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
cases lookup a l <;> simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
⊢ a ∈ toFinset (List.keys (filter (fun x => decide (x.snd ≠ 0)) l.entries)) ↔
    (fun a => Option.getD (lookup a l) 0) a ≠ 0
[PROOFSTEP]
simp_rw [@mem_toFinset _ _, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
⊢ (∃ b, b ∈ lookup a l ∧ decide (b ≠ 0) = true) ↔ Option.getD (lookup a l) 0 ≠ 0
[PROOFSTEP]
cases lookup a l
[GOAL]
case none
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
⊢ (∃ b, b ∈ none ∧ decide (b ≠ 0) = true) ↔ Option.getD none 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
val✝ : M
⊢ (∃ b, b ∈ some val✝ ∧ decide (b ≠ 0) = true) ↔ Option.getD (some val✝) 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ ↑(lookupFinsupp l) a = Option.getD (lookup a l) 0
[PROOFSTEP]
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ Option.getD (lookup a l) 0 = Option.getD (lookup a l) 0
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (lookupFinsupp l).support = toFinset (List.keys (filter (fun x => decide (x.snd ≠ 0)) l.entries))
[PROOFSTEP]
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
[GOAL]
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ toFinset (List.keys (filter (fun x => decide ¬x.snd = 0) l.entries)) =
    toFinset (List.keys (filter (fun x => decide ¬x.snd = 0) l.entries))
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝¹ a b
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case h.e_3.h.e_a.e_p
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0
[PROOFSTEP]
funext
[GOAL]
case h.e_3.h.e_a.e_p.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
x✝ : (_ : α) × M
⊢ (decide ¬x✝.snd = 0) = decide ¬x✝.snd = 0
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ ↑(lookupFinsupp l) a = x ↔ x ∈ lookup a l
[PROOFSTEP]
rw [lookupFinsupp_apply]
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ Option.getD (lookup a l) 0 = x ↔ x ∈ lookup a l
[PROOFSTEP]
cases' lookup a l with m
[GOAL]
case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ Option.getD none 0 = x ↔ x ∈ none
[PROOFSTEP]
simp [hx.symm]
[GOAL]
case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
m : M
⊢ Option.getD (some m) 0 = x ↔ x ∈ some m
[PROOFSTEP]
simp [hx.symm]
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ ↑(lookupFinsupp l) a = 0 ↔ ¬a ∈ l ∨ 0 ∈ lookup a l
[PROOFSTEP]
rw [lookupFinsupp_apply, ← lookup_eq_none]
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ Option.getD (lookup a l) 0 = 0 ↔ lookup a l = none ∨ 0 ∈ lookup a l
[PROOFSTEP]
cases' lookup a l with m
[GOAL]
case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ Option.getD none 0 = 0 ↔ none = none ∨ 0 ∈ none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
⊢ Option.getD (some m) 0 = 0 ↔ some m = none ∨ 0 ∈ some m
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ lookupFinsupp ∅ = 0
[PROOFSTEP]
classical
ext
simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ lookupFinsupp ∅ = 0
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
a✝ : α
⊢ ↑(lookupFinsupp ∅) a✝ = ↑0 a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
⊢ lookupFinsupp (insert a m l) = Finsupp.update (lookupFinsupp l) a m
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
⊢ ↑(lookupFinsupp (insert a m l)) b = ↑(Finsupp.update (lookupFinsupp l) a m) b
[PROOFSTEP]
by_cases h : b = a
[GOAL]
case pos
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
h : b = a
⊢ ↑(lookupFinsupp (insert a m l)) b = ↑(Finsupp.update (lookupFinsupp l) a m) b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
h : ¬b = a
⊢ ↑(lookupFinsupp (insert a m l)) b = ↑(Finsupp.update (lookupFinsupp l) a m) b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ lookupFinsupp (singleton a m) = Finsupp.single a m
[PROOFSTEP]
classical
  -- porting note: was `simp [←AList.insert_empty]` but timeout issuessimp only [← AList.insert_empty,
  insert_lookupFinsupp, empty_lookupFinsupp, Finsupp.zero_update]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ lookupFinsupp (singleton a m) = Finsupp.single a m
[PROOFSTEP]
simp only [← AList.insert_empty, insert_lookupFinsupp, empty_lookupFinsupp, Finsupp.zero_update]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ lookupFinsupp (Finsupp.toAList f) = f
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
classical
by_cases h : f a = 0
· suffices f.toAList.lookup a = none by simp [h, this]
  · simp [lookup_eq_none, h]
· suffices f.toAList.lookup a = some (f a) by simp [h, this]
  · apply mem_lookup_iff.2
    simpa using h
[GOAL]
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
by_cases h : f a = 0
[GOAL]
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
suffices f.toAList.lookup a = none by simp [h, this]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
this : lookup a (Finsupp.toAList f) = none
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
simp [h, this]
[GOAL]
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
⊢ lookup a (Finsupp.toAList f) = none
[PROOFSTEP]
simp [lookup_eq_none, h]
[GOAL]
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
suffices f.toAList.lookup a = some (f a) by simp [h, this]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
this : lookup a (Finsupp.toAList f) = some (↑f a)
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
simp [h, this]
[GOAL]
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ lookup a (Finsupp.toAList f) = some (↑f a)
[PROOFSTEP]
apply mem_lookup_iff.2
[GOAL]
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ { fst := a, snd := ↑f a } ∈ (Finsupp.toAList f).entries
[PROOFSTEP]
simpa using h
