[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
⊢ Injective toFun
[PROOFSTEP]
rintro ⟨s, f, hf⟩ ⟨t, g, hg⟩ (rfl : f = g)
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
⊢ { support := s, toFun := f, mem_support_toFun := hf } = { support := t, toFun := f, mem_support_toFun := hg }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_support
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
⊢ s = t
[PROOFSTEP]
ext a
[GOAL]
case mk.mk.e_support.a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
a : α
⊢ a ∈ s ↔ a ∈ t
[PROOFSTEP]
exact (hf _).trans (hg _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
⊢ ↑f = 0 ↔ f = 0
[PROOFSTEP]
rw [← coe_zero, FunLike.coe_fn_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
⊢ ↑f a = ↑g a
[PROOFSTEP]
classical exact
  if h : a ∈ f.support then h₂ a h
  else by
    have hf : f a = 0 := not_mem_support_iff.1 h
    have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h 
    rw [hf, hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
⊢ ↑f a = ↑g a
[PROOFSTEP]
exact
  if h : a ∈ f.support then h₂ a h
  else by
    have hf : f a = 0 := not_mem_support_iff.1 h
    have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h 
    rw [hf, hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
⊢ ↑f a = ↑g a
[PROOFSTEP]
have hf : f a = 0 := not_mem_support_iff.1 h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
hf : ↑f a = 0
⊢ ↑f a = ↑g a
[PROOFSTEP]
have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
hf : ↑f a = 0
⊢ ↑g a = 0
[PROOFSTEP]
rwa [h₁, not_mem_support_iff] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
hf : ↑f a = 0
hg : ↑g a = 0
⊢ ↑f a = ↑g a
[PROOFSTEP]
rw [hf, hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
⊢ f.support = ∅ ↔ f = 0
[PROOFSTEP]
exact_mod_cast @Function.support_eq_empty_iff _ _ _ f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
⊢ Finset.Nonempty f.support ↔ f ≠ 0
[PROOFSTEP]
simp only [Finsupp.support_eq_empty, Finset.nonempty_iff_ne_empty, Ne.def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
⊢ f ≠ 0 ↔ ∃ a, ↑f a ≠ 0
[PROOFSTEP]
simp [← Finsupp.support_eq_empty, Finset.eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
⊢ card f.support = 0 ↔ f = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ ↑f.support ⊆ s ↔ ∀ (a : α), ¬a ∈ s → ↑f a = 0
[PROOFSTEP]
simp only [Set.subset_def, mem_coe, mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ (∀ (x : α), ↑f x ≠ 0 → x ∈ s) ↔ ∀ (a : α), ¬a ∈ s → ↑f a = 0
[PROOFSTEP]
exact forall_congr' fun a => not_imp_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Unique α
f g : α →₀ M
h : ↑f default = ↑g default
a : α
⊢ ↑f a = ↑g a
[PROOFSTEP]
rwa [Unique.eq_default a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a : α
b : M
a' : α
⊢ (a' ∈ if b = 0 then ∅ else {a}) ↔ Pi.single a b a' ≠ 0
[PROOFSTEP]
classical
obtain rfl | hb := eq_or_ne b 0
· simp [Pi.single, update]
rw [if_neg hb, mem_singleton]
obtain rfl | ha := eq_or_ne a' a
· simp [hb, Pi.single, update]
simp [Pi.single_eq_of_ne' ha.symm, ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a : α
b : M
a' : α
⊢ (a' ∈ if b = 0 then ∅ else {a}) ↔ Pi.single a b a' ≠ 0
[PROOFSTEP]
obtain rfl | hb := eq_or_ne b 0
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b : M
a a' : α
⊢ (a' ∈ if 0 = 0 then ∅ else {a}) ↔ Pi.single a 0 a' ≠ 0
[PROOFSTEP]
simp [Pi.single, update]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a : α
b : M
a' : α
hb : b ≠ 0
⊢ (a' ∈ if b = 0 then ∅ else {a}) ↔ Pi.single a b a' ≠ 0
[PROOFSTEP]
rw [if_neg hb, mem_singleton]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a : α
b : M
a' : α
hb : b ≠ 0
⊢ a' = a ↔ Pi.single a b a' ≠ 0
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a' a
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a'✝ : α
b✝ b : M
a' : α
hb : b ≠ 0
⊢ a' = a' ↔ Pi.single a' b a' ≠ 0
[PROOFSTEP]
simp [hb, Pi.single, update]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a : α
b : M
a' : α
hb : b ≠ 0
ha : a' ≠ a
⊢ a' = a ↔ Pi.single a b a' ≠ 0
[PROOFSTEP]
simp [Pi.single_eq_of_ne' ha.symm, ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ ↑(single a b) a' = if a = a' then b else 0
[PROOFSTEP]
classical
simp_rw [@eq_comm _ a a']
convert Pi.single_apply a b a'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ ↑(single a b) a' = if a = a' then b else 0
[PROOFSTEP]
simp_rw [@eq_comm _ a a']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ ↑(single a b) a' = if a' = a then b else 0
[PROOFSTEP]
convert Pi.single_apply a b a'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
f : α → β
hf : Injective f
x z : α
y : M
⊢ ↑(single (f x) y) (f z) = ↑(single x y) z
[PROOFSTEP]
classical simp only [single_apply, hf.eq_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
f : α → β
hf : Injective f
x z : α
y : M
⊢ ↑(single (f x) y) (f z) = ↑(single x y) z
[PROOFSTEP]
simp only [single_apply, hf.eq_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ ↑(single a b) = Set.indicator {a} fun x => b
[PROOFSTEP]
classical
ext
simp [single_apply, Set.indicator, @eq_comm _ a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ ↑(single a b) = Set.indicator {a} fun x => b
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
x✝ : α
⊢ ↑(single a b) x✝ = Set.indicator {a} (fun x => b) x✝
[PROOFSTEP]
simp [single_apply, Set.indicator, @eq_comm _ a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ ↑(single a b) a = b
[PROOFSTEP]
classical exact Pi.single_eq_same (f := λ _ => M) a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ ↑(single a b) a = b
[PROOFSTEP]
exact Pi.single_eq_same (f := λ _ => M) a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ ↑(single a b) a' = 0
[PROOFSTEP]
classical exact Pi.single_eq_of_ne' h _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ ↑(single a b) a' = 0
[PROOFSTEP]
exact Pi.single_eq_of_ne' h _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a✝ a' : α
b✝ : M
inst✝ : DecidableEq α
a : α
b : M
⊢ ↑(single a b) = update 0 a b
[PROOFSTEP]
classical rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a✝ a' : α
b✝ : M
inst✝ : DecidableEq α
a : α
b : M
⊢ ↑(single a b) = update 0 a b
[PROOFSTEP]
rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
a : α
⊢ (fun f => ↑f) (single a 0) = (fun f => ↑f) 0
[PROOFSTEP]
classical simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
a : α
⊢ (fun f => ↑f) (single a 0) = (fun f => ↑f) 0
[PROOFSTEP]
simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a a' : α
b : M
⊢ single a (↑(single a' b) a) = ↑(single a' (single a' b)) a
[PROOFSTEP]
classical
rw [single_apply, single_apply]
ext
split_ifs with h
· rw [h]
· rw [zero_apply, single_apply, ite_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a a' : α
b : M
⊢ single a (↑(single a' b) a) = ↑(single a' (single a' b)) a
[PROOFSTEP]
rw [single_apply, single_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a a' : α
b : M
⊢ single a (if a' = a then b else 0) = if a' = a then single a' b else 0
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
⊢ ↑(single a (if a' = a then b else 0)) a✝ = ↑(if a' = a then single a' b else 0) a✝
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
h : a' = a
⊢ ↑(single a b) a✝ = ↑(single a' b) a✝
[PROOFSTEP]
rw [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
h : ¬a' = a
⊢ ↑(single a 0) a✝ = ↑0 a✝
[PROOFSTEP]
rw [zero_apply, single_apply, ite_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ (single a b).support ⊆ {a}
[PROOFSTEP]
classical show ite _ _ _ ⊆ _; split_ifs <;> [exact empty_subset _; exact Subset.refl _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ (single a b).support ⊆ {a}
[PROOFSTEP]
show ite _ _ _ ⊆ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ (if b = 0 then ∅ else {a}) ⊆ {a}
[PROOFSTEP]
split_ifs <;> [exact empty_subset _; exact Subset.refl _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ (if b = 0 then ∅ else {a}) ⊆ {a}
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
h✝ : b = 0
⊢ ∅ ⊆ {a}
[PROOFSTEP]
exact empty_subset _
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
h✝ : ¬b = 0
⊢ {a} ⊆ {a}
[PROOFSTEP]
exact Subset.refl _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
x : α
⊢ ↑(single a b) x ∈ {0, b}
[PROOFSTEP]
rcases em (a = x) with (rfl | hx) <;> [simp; simp [single_eq_of_ne hx]]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
x : α
⊢ ↑(single a b) x ∈ {0, b}
[PROOFSTEP]
rcases em (a = x) with (rfl | hx)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ ↑(single a b) a ∈ {0, b}
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
x : α
hx : ¬a = x
⊢ ↑(single a b) x ∈ {0, b}
[PROOFSTEP]
simp [single_eq_of_ne hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ b₁ = b₂
[PROOFSTEP]
have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a := by rw [eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ ↑(single a b₁) a = ↑(single a b₂) a
[PROOFSTEP]
rw [eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
this : ↑(single a b₁) a = ↑(single a b₂) a
⊢ b₁ = b₂
[PROOFSTEP]
rwa [single_eq_same, single_eq_same] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b✝ : M
a x : α
b : M
⊢ ↑(single a b) x = 0 ↔ x = a → b = 0
[PROOFSTEP]
simp [single_eq_set_indicator]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b✝ : M
a x : α
b : M
⊢ ↑(single a b) x ≠ 0 ↔ x = a ∧ b ≠ 0
[PROOFSTEP]
simp [single_apply_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a a' : α
b : M
⊢ a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0
[PROOFSTEP]
simp [single_apply_eq_zero, not_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b✝ : M
f : α →₀ M
a : α
b : M
⊢ f = single a b ↔ f.support ⊆ {a} ∧ ↑f a = b
[PROOFSTEP]
refine' ⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b✝ : M
f : α →₀ M
a : α
b : M
⊢ f.support ⊆ {a} ∧ ↑f a = b → f = single a b
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
⊢ f = single a (↑f a)
[PROOFSTEP]
ext x
[GOAL]
case intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ ↑f x = ↑(single a (↑f a)) x
[PROOFSTEP]
by_cases hx : a = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : a = x
⊢ ↑f x = ↑(single a (↑f a)) x
[PROOFSTEP]
simp only [hx, single_eq_same, single_eq_of_ne, Ne.def, not_false_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬a = x
⊢ ↑f x = ↑(single a (↑f a)) x
[PROOFSTEP]
simp only [hx, single_eq_same, single_eq_of_ne, Ne.def, not_false_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬a = x
⊢ ↑f x = 0
[PROOFSTEP]
exact not_mem_support_iff.1 (mt (fun hx => (mem_singleton.1 (h hx)).symm) hx)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
intro eq
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
by_cases h : a₁ = a₂
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
refine' Or.inl ⟨h, _⟩
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ b₁ = b₂
[PROOFSTEP]
rwa [h, (single_injective a₂).eq_iff] at eq 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
rw [FunLike.ext_iff] at eq 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
eq : ∀ (x : α), ↑(single a₁ b₁) x = ↑(single a₂ b₂) x
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
have h₁ := eq a₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
eq : ∀ (x : α), ↑(single a₁ b₁) x = ↑(single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : ↑(single a₁ b₁) a₁ = ↑(single a₂ b₂) a₁
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
have h₂ := eq a₂
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
eq : ∀ (x : α), ↑(single a₁ b₁) x = ↑(single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : ↑(single a₁ b₁) a₁ = ↑(single a₂ b₂) a₁
h₂ : ↑(single a₁ b₁) a₂ = ↑(single a₂ b₂) a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
simp only [single_eq_same, single_eq_of_ne h, single_eq_of_ne (Ne.symm h)] at h₁ h₂ 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
eq : ∀ (x : α), ↑(single a₁ b₁) x = ↑(single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : b₁ = 0
h₂ : 0 = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
[PROOFSTEP]
exact Or.inr ⟨h₁, h₂.symm⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → single a₁ b₁ = single a₂ b₂
[PROOFSTEP]
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case mpr.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ : α
b₁ : M
⊢ single a₁ b₁ = single a₁ b₁
[PROOFSTEP]
rfl
[GOAL]
case mpr.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
⊢ single a₁ 0 = single a₂ 0
[PROOFSTEP]
rw [single_zero, single_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
i : α
h : b ≠ 0
⊢ (single i b).support ≠ ⊥
[PROOFSTEP]
simpa only [support_single_ne_zero _ h] using singleton_ne_empty _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint (single i b).support (single j b').support ↔ i ≠ j
[PROOFSTEP]
rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
⊢ single a b = 0 ↔ b = 0
[PROOFSTEP]
simp [FunLike.ext_iff, single_eq_set_indicator]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b✝ : M
a₁ a₂ : α
b : M
⊢ ↑(single a₁ b) a₂ = ↑(single a₂ b) a₁
[PROOFSTEP]
classical simp only [single_apply, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b✝ : M
a₁ a₂ : α
b : M
⊢ ↑(single a₁ b) a₂ = ↑(single a₂ b) a₁
[PROOFSTEP]
simp only [single_apply, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : Nonempty α
inst✝ : Nontrivial M
⊢ Nontrivial (α →₀ M)
[PROOFSTEP]
inhabit α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : Nonempty α
inst✝ : Nontrivial M
inhabited_h : Inhabited α
⊢ Nontrivial (α →₀ M)
[PROOFSTEP]
rcases exists_ne (0 : M) with ⟨x, hx⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : Nonempty α
inst✝ : Nontrivial M
inhabited_h : Inhabited α
x : M
hx : x ≠ 0
⊢ Nontrivial (α →₀ M)
[PROOFSTEP]
exact nontrivial_of_ne (single default x) 0 (mt single_eq_zero.1 hx)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ single a b = single a' b' ↔ b = b'
[PROOFSTEP]
rw [unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same, single_eq_same]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
f : α →₀ M
⊢ card f.support = 1 ↔ ∃ a, ↑f a ≠ 0 ∧ f = single a (↑f a)
[PROOFSTEP]
simp only [card_eq_one, support_eq_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
f : α →₀ M
⊢ card f.support = 1 ↔ ∃ a b x, f = single a b
[PROOFSTEP]
simp only [card_eq_one, support_eq_singleton']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a✝ a' : α
b✝ : M
f : α →₀ M
a : α
x✝ : ∃ b, f = single a b
b : M
hb : f = single a b
⊢ f.support ⊆ {a}
[PROOFSTEP]
rw [hb, support_subset_singleton, single_eq_same]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Nonempty α
f : α →₀ M
⊢ card f.support ≤ 1 ↔ ∃ a, f = single a (↑f a)
[PROOFSTEP]
simp only [card_le_one_iff_subset_singleton, support_subset_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Nonempty α
f : α →₀ M
⊢ card f.support ≤ 1 ↔ ∃ a b, f = single a b
[PROOFSTEP]
simp only [card_le_one_iff_subset_singleton, support_subset_singleton']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ ↑equivFunOnFinite (single x m) = Pi.single x m
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
x✝ : α
⊢ ↑equivFunOnFinite (single x m) x✝ = Pi.single x m x✝
[PROOFSTEP]
simp [Finsupp.single_eq_pi_single, equivFunOnFinite]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ ↑equivFunOnFinite.symm (Pi.single x m) = single x m
[PROOFSTEP]
rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i : α
f : α →₀ M
a : α
b : M
⊢ Finset α
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i : α
f : α →₀ M
a : α
b : M
this : DecidableEq α
⊢ Finset α
[PROOFSTEP]
haveI := Classical.decEq M
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i : α
f : α →₀ M
a : α
b : M
this✝ : DecidableEq α
this : DecidableEq M
⊢ Finset α
[PROOFSTEP]
exact if b = 0 then f.support.erase a else insert a f.support
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
⊢ (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ Function.update (↑f) a b i ≠ 0
[PROOFSTEP]
classical
simp [Function.update, Ne.def]
split_ifs with hb ha ha <;> try simp only [*, not_false_iff, iff_true, not_true, iff_false]
· rw [Finset.mem_erase]
  simp
· rw [Finset.mem_erase]
  simp [ha]
· rw [Finset.mem_insert]
  simp [ha]
· rw [Finset.mem_insert]
  simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
⊢ (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ Function.update (↑f) a b i ≠ 0
[PROOFSTEP]
simp [Function.update, Ne.def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
⊢ (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ ¬(if i = a then b else ↑f i) = 0
[PROOFSTEP]
split_ifs with hb ha ha
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : b = 0
ha : i = a
⊢ i ∈ erase f.support a ↔ ¬b = 0
[PROOFSTEP]
try simp only [*, not_false_iff, iff_true, not_true, iff_false]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : b = 0
ha : i = a
⊢ i ∈ erase f.support a ↔ ¬b = 0
[PROOFSTEP]
simp only [*, not_false_iff, iff_true, not_true, iff_false]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : b = 0
ha : ¬i = a
⊢ i ∈ erase f.support a ↔ ¬↑f i = 0
[PROOFSTEP]
try simp only [*, not_false_iff, iff_true, not_true, iff_false]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : b = 0
ha : ¬i = a
⊢ i ∈ erase f.support a ↔ ¬↑f i = 0
[PROOFSTEP]
simp only [*, not_false_iff, iff_true, not_true, iff_false]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : ¬b = 0
ha : i = a
⊢ i ∈ insert a f.support ↔ ¬b = 0
[PROOFSTEP]
try simp only [*, not_false_iff, iff_true, not_true, iff_false]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : ¬b = 0
ha : i = a
⊢ i ∈ insert a f.support ↔ ¬b = 0
[PROOFSTEP]
simp only [*, not_false_iff, iff_true, not_true, iff_false]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : ¬b = 0
ha : ¬i = a
⊢ i ∈ insert a f.support ↔ ¬↑f i = 0
[PROOFSTEP]
try simp only [*, not_false_iff, iff_true, not_true, iff_false]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : ¬b = 0
ha : ¬i = a
⊢ i ∈ insert a f.support ↔ ¬↑f i = 0
[PROOFSTEP]
simp only [*, not_false_iff, iff_true, not_true, iff_false]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : b = 0
ha : i = a
⊢ ¬a ∈ erase f.support a
[PROOFSTEP]
rw [Finset.mem_erase]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : b = 0
ha : i = a
⊢ ¬(a ≠ a ∧ a ∈ f.support)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : b = 0
ha : ¬i = a
⊢ i ∈ erase f.support a ↔ ¬↑f i = 0
[PROOFSTEP]
rw [Finset.mem_erase]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : b = 0
ha : ¬i = a
⊢ i ≠ a ∧ i ∈ f.support ↔ ¬↑f i = 0
[PROOFSTEP]
simp [ha]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : ¬b = 0
ha : i = a
⊢ a ∈ insert a f.support
[PROOFSTEP]
rw [Finset.mem_insert]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : ¬b = 0
ha : i = a
⊢ a = a ∨ a ∈ f.support
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : ¬b = 0
ha : ¬i = a
⊢ i ∈ insert a f.support ↔ ¬↑f i = 0
[PROOFSTEP]
rw [Finset.mem_insert]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f✝ : α →₀ M
a✝ : α
b✝ : M
i✝ : α
f : α →₀ M
a : α
b : M
i : α
hb : ¬b = 0
ha : ¬i = a
⊢ i = a ∨ i ∈ f.support ↔ ¬↑f i = 0
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ ↑(update f a b) = Function.update (↑f) a b
[PROOFSTEP]
delta update Function.update
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ ↑{ support := if b = 0 then erase f.support a else insert a f.support,
        toFun := fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1,
        mem_support_toFun :=
          (_ :
            ∀ (i : α),
              (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ Function.update (↑f) a b i ≠ 0) } =
    fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
x✝ : α
⊢ ↑{ support := if b = 0 then erase f.support a else insert a f.support,
          toFun := fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1,
          mem_support_toFun :=
            (_ :
              ∀ (i : α),
                (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ Function.update (↑f) a b i ≠ 0) }
      x✝ =
    if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝
[PROOFSTEP]
dsimp
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
x✝ : α
⊢ (if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝) = if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
x✝ : α
h✝ : x✝ = a
⊢ (_ : a = x✝) ▸ b = (_ : a = x✝) ▸ b
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
x✝ : α
h✝ : ¬x✝ = a
⊢ ↑f x✝ = ↑f x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i : α
⊢ update f a (↑f a) = f
[PROOFSTEP]
classical
ext
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i : α
⊢ update f a (↑f a) = f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update f a (↑f a)) a✝ = ↑f a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i : α
⊢ update 0 a b = single a b
[PROOFSTEP]
classical
ext
rw [single_eq_update]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i : α
⊢ update 0 a b = single a b
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update 0 a b) a✝ = ↑(single a b) a✝
[PROOFSTEP]
rw [single_eq_update]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update 0 a b) a✝ = Function.update 0 a b a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (update f a b).support = if b = 0 then erase f.support a else insert a f.support
[PROOFSTEP]
classical dsimp [update]; congr <;> apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (update f a b).support = if b = 0 then erase f.support a else insert a f.support
[PROOFSTEP]
dsimp [update]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (if b = 0 then erase f.support a else insert a f.support) = if b = 0 then erase f.support a else insert a f.support
[PROOFSTEP]
congr
[GOAL]
case e_t.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝¹ a b
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case e_e.h.e_3.h.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝¹ a b
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ (update f a 0).support = erase f.support a
[PROOFSTEP]
classical
simp only [update, ite_true, mem_support_iff, ne_eq, not_not]
congr; apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ (update f a 0).support = erase f.support a
[PROOFSTEP]
simp only [update, ite_true, mem_support_iff, ne_eq, not_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ erase f.support a = erase f.support a
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (update f a b).support = insert a f.support
[PROOFSTEP]
classical
simp only [update, h, ite_false, mem_support_iff, ne_eq]
congr; apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (update f a b).support = insert a f.support
[PROOFSTEP]
simp only [update, h, ite_false, mem_support_iff, ne_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ insert a f.support = insert a f.support
[PROOFSTEP]
congr
[GOAL]
case h.e_3.h.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
a' : α
⊢ a' ∈ Finset.erase f.support a ↔ (fun a' => if a' = a then 0 else ↑f a') a' ≠ 0
[PROOFSTEP]
classical
rw [mem_erase, mem_support_iff]; dsimp
split_ifs with h
exact ⟨fun H _ => H.1 h, fun H => (H rfl).elim⟩
exact and_iff_right h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
a' : α
⊢ a' ∈ Finset.erase f.support a ↔ (fun a' => if a' = a then 0 else ↑f a') a' ≠ 0
[PROOFSTEP]
rw [mem_erase, mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
a' : α
⊢ a' ≠ a ∧ ↑f a' ≠ 0 ↔ (fun a' => if a' = a then 0 else ↑f a') a' ≠ 0
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
a' : α
⊢ ¬a' = a ∧ ¬↑f a' = 0 ↔ ¬(if a' = a then 0 else ↑f a') = 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
a' : α
h : a' = a
⊢ ¬a' = a ∧ ¬↑f a' = 0 ↔ ¬0 = 0
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
a' : α
h : ¬a' = a
⊢ ¬a' = a ∧ ¬↑f a' = 0 ↔ ¬↑f a' = 0
[PROOFSTEP]
exact ⟨fun H _ => H.1 h, fun H => (H rfl).elim⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
a' : α
h : ¬a' = a
⊢ ¬a' = a ∧ ¬↑f a' = 0 ↔ ¬↑f a' = 0
[PROOFSTEP]
exact and_iff_right h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = Finset.erase f.support a
[PROOFSTEP]
classical
dsimp [erase]
congr; apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = Finset.erase f.support a
[PROOFSTEP]
dsimp [erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ Finset.erase f.support a = Finset.erase f.support a
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
⊢ ↑(erase a f) a = 0
[PROOFSTEP]
classical simp only [erase, coe_mk, ite_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
f : α →₀ M
⊢ ↑(erase a f) a = 0
[PROOFSTEP]
simp only [erase, coe_mk, ite_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ ↑(erase a f) a' = ↑f a'
[PROOFSTEP]
classical simp only [erase, coe_mk, h, ite_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ ↑(erase a f) a' = ↑f a'
[PROOFSTEP]
simp only [erase, coe_mk, h, ite_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
b : M
⊢ erase a (single a b) = 0
[PROOFSTEP]
ext s
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
b : M
s : α
⊢ ↑(erase a (single a b)) s = ↑0 s
[PROOFSTEP]
by_cases hs : s = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
b : M
s : α
hs : s = a
⊢ ↑(erase a (single a b)) s = ↑0 s
[PROOFSTEP]
rw [hs, erase_same]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
b : M
s : α
hs : s = a
⊢ 0 = ↑0 a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ ↑(erase a (single a b)) s = ↑0 s
[PROOFSTEP]
rw [erase_ne hs]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ ↑(single a b) s = ↑0 s
[PROOFSTEP]
exact single_eq_of_ne (Ne.symm hs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ erase a (single a' b) = single a' b
[PROOFSTEP]
ext s
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s
[PROOFSTEP]
by_cases hs : s = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : s = a
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s
[PROOFSTEP]
rw [hs, erase_same, single_eq_of_ne h.symm]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : ¬s = a
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s
[PROOFSTEP]
rw [erase_ne hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
⊢ erase a f = f
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
⊢ ↑(erase a f) b = ↑f b
[PROOFSTEP]
by_cases hab : b = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
hab : b = a
⊢ ↑(erase a f) b = ↑f b
[PROOFSTEP]
rwa [hab, erase_same, eq_comm, ← not_mem_support_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
hab : ¬b = a
⊢ ↑(erase a f) b = ↑f b
[PROOFSTEP]
rw [erase_ne hab]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
⊢ erase a 0 = 0
[PROOFSTEP]
classical rw [← support_eq_empty, support_erase, support_zero, erase_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
a : α
⊢ erase a 0 = 0
[PROOFSTEP]
rw [← support_eq_empty, support_erase, support_zero, erase_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ (a : α), a ∈ filter (fun x => f x ≠ 0) s ↔ f a ≠ 0
[PROOFSTEP]
classical simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ (a : α), a ∈ filter (fun x => f x ≠ 0) s ↔ f a ≠ 0
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support ⊆ s
[PROOFSTEP]
classical convert filter_subset (f · ≠ 0) s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support ⊆ s
[PROOFSTEP]
convert filter_subset (f · ≠ 0) s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0
[PROOFSTEP]
rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support = filter (fun a => f a ≠ 0) s
[PROOFSTEP]
dsimp [onFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ filter (fun x => ¬f x = 0) s = filter (fun a => ¬f a = 0) s
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ (f ∘ ↑g) a ≠ 0 → a ∈ g.support
[PROOFSTEP]
rw [mem_support_iff, not_imp_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ ↑g a = 0 → (f ∘ ↑g) a = 0
[PROOFSTEP]
exact fun H => (congr_arg f H).trans hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N
hf : f 0 = 0
a : α
⊢ ↑(mapRange f hf 0) a = ↑0 a
[PROOFSTEP]
simp only [hf, zero_apply, mapRange_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N
hf : f 0 = 0
a : α
b : M
a' : α
⊢ ↑(mapRange f hf (single a b)) a' = ↑(single a (f b)) a'
[PROOFSTEP]
classical simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N
hf : f 0 = 0
a : α
b : M
a' : α
⊢ ↑(mapRange f hf (single a b)) a' = ↑(single a (f b)) a'
[PROOFSTEP]
simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
⊢ (mapRange e he0 f).support = f.support
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
a✝ : ι
⊢ a✝ ∈ (mapRange e he0 f).support ↔ a✝ ∈ f.support
[PROOFSTEP]
simp only [Finsupp.mem_support_iff, Ne.def, Finsupp.mapRange_apply]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
a✝ : ι
⊢ ¬e (↑f a✝) = 0 ↔ ¬↑f a✝ = 0
[PROOFSTEP]
exact he.ne_iff' he0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
this : DecidableEq β
h : a₂ ∈ map f v.support
⊢ ∃! a, a ∈ v.support ∧ (fun a₁ => ↑f a₁ = a₂) a
[PROOFSTEP]
rcases Finset.mem_map.1 h with ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
this : DecidableEq β
a : α
ha : a ∈ v.support
h : ↑f a ∈ map f v.support
⊢ ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1
[PROOFSTEP]
exact ExistsUnique.intro a ⟨ha, rfl⟩ fun b ⟨_, hb⟩ => f.injective hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
⊢ a₂ ∈ map f v.support ↔
    (fun a₂ =>
          if h : a₂ ∈ map f v.support then
            ↑v (choose (fun a₁ => ↑f a₁ = a₂) v.support (_ : ∃! a, a ∈ v.support ∧ (fun a₁ => ↑f a₁ = a₂) a))
          else 0)
        a₂ ≠
      0
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
⊢ a₂ ∈ map f v.support ↔
    ¬(if h : a₂ ∈ map f v.support then
          ↑v (choose (fun a₁ => ↑f a₁ = a₂) v.support (_ : ∃! a, a ∈ v.support ∧ ↑f a = a₂))
        else 0) =
        0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
⊢ a₂ ∈ map f v.support ↔ ¬↑v (choose (fun a₁ => ↑f a₁ = a₂) v.support (_ : ∃! a, a ∈ v.support ∧ ↑f a = a₂)) = 0
[PROOFSTEP]
simp only [h, true_iff_iff, Ne.def]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
⊢ ¬↑v (choose (fun a₁ => ↑f a₁ = a₂) v.support (_ : ∃! a, a ∈ v.support ∧ ↑f a = a₂)) = 0
[PROOFSTEP]
rw [← not_mem_support_iff, not_not]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
⊢ choose (fun a₁ => ↑f a₁ = a₂) v.support (_ : ∃! a, a ∈ v.support ∧ ↑f a = a₂) ∈ v.support
[PROOFSTEP]
classical apply Finset.choose_mem
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
⊢ choose (fun a₁ => ↑f a₁ = a₂) v.support (_ : ∃! a, a ∈ v.support ∧ ↑f a = a₂) ∈ v.support
[PROOFSTEP]
apply Finset.choose_mem
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : ¬a₂ ∈ map f v.support
⊢ a₂ ∈ map f v.support ↔ ¬0 = 0
[PROOFSTEP]
simp only [h, Ne.def, ne_self_iff_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
⊢ ↑(embDomain f v) (↑f a) = ↑v a
[PROOFSTEP]
classical
change dite _ _ _ = _
split_ifs with h <;> rw [Finset.mem_map' f] at h 
· refine' congr_arg (v : α → M) (f.inj' _)
  exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
· exact (not_mem_support_iff.1 h).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
⊢ ↑(embDomain f v) (↑f a) = ↑v a
[PROOFSTEP]
change dite _ _ _ = _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
⊢ (if h : ↑f a ∈ map f v.support then
      (fun h =>
          ↑v (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)))
        h
    else (fun h => 0) h) =
    ↑v a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h : ↑f a ∈ map f v.support
⊢ (fun h => ↑v (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)))
      h =
    ↑v a
[PROOFSTEP]
rw [Finset.mem_map' f] at h 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h : ¬↑f a ∈ map f v.support
⊢ (fun h => 0) h = ↑v a
[PROOFSTEP]
rw [Finset.mem_map' f] at h 
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ↑f a ∈ map f v.support
h : a ∈ v.support
⊢ (fun h => ↑v (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)))
      h✝ =
    ↑v a
[PROOFSTEP]
refine' congr_arg (v : α → M) (f.inj' _)
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ↑f a ∈ map f v.support
h : a ∈ v.support
⊢ Embedding.toFun f
      (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)) =
    Embedding.toFun f a
[PROOFSTEP]
exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ¬↑f a ∈ map f v.support
h : ¬a ∈ v.support
⊢ (fun h => 0) h✝ = ↑v a
[PROOFSTEP]
exact (not_mem_support_iff.1 h).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f v) a = 0
[PROOFSTEP]
classical
refine' dif_neg (mt (fun h => _) h)
rcases Finset.mem_map.1 h with ⟨a, _h, rfl⟩
exact Set.mem_range_self a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f v) a = 0
[PROOFSTEP]
refine' dif_neg (mt (fun h => _) h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : β
h✝ : ¬a ∈ Set.range ↑f
h : a ∈ map f v.support
⊢ a ∈ Set.range ↑f
[PROOFSTEP]
rcases Finset.mem_map.1 h with ⟨a, _h, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
_h : a ∈ v.support
h✝ : ¬↑f a ∈ Set.range ↑f
h : ↑f a ∈ map f v.support
⊢ ↑f a ∈ Set.range ↑f
[PROOFSTEP]
exact Set.mem_range_self a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
l₁ l₂ : α →₀ M
h : embDomain f l₁ = embDomain f l₂
a : α
⊢ ↑l₁ a = ↑l₂ a
[PROOFSTEP]
simpa only [embDomain_apply] using FunLike.ext_iff.1 h (f a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
⊢ embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p)
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a
[PROOFSTEP]
by_cases h : a ∈ Set.range f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : a ∈ Set.range ↑f
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a
[PROOFSTEP]
rcases h with ⟨a', rfl⟩
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a' : α
⊢ ↑(embDomain f (mapRange g hg p)) (↑f a') = ↑(mapRange g hg (embDomain f p)) (↑f a')
[PROOFSTEP]
rw [mapRange_apply, embDomain_apply, embDomain_apply, mapRange_apply]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a
[PROOFSTEP]
rw [mapRange_apply, embDomain_notin_range, embDomain_notin_range, ← hg]
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : ¬a ∈ Set.range ↑f
⊢ ¬a ∈ Set.range ↑f
[PROOFSTEP]
assumption
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : ¬a ∈ Set.range ↑f
⊢ ¬a ∈ Set.range ↑f
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ ∃ x, l = single x b ∧ ↑f x = a
[PROOFSTEP]
classical
have h_map_support : Finset.map f l.support = { a } := by rw [← support_embDomain, h, support_single_ne_zero _ hb]
have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
use c
constructor
· ext d
  rw [← embDomain_apply f l, h]
  by_cases h_cases : c = d
  · simp only [Eq.symm h_cases, hc₂, single_eq_same]
  · rw [single_apply, single_apply, if_neg, if_neg h_cases]
    by_contra hfd
    exact h_cases (f.injective (hc₂.trans hfd))
· exact hc₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ ∃ x, l = single x b ∧ ↑f x = a
[PROOFSTEP]
have h_map_support : Finset.map f l.support = { a } := by rw [← support_embDomain, h, support_single_ne_zero _ hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ map f l.support = {a}
[PROOFSTEP]
rw [← support_embDomain, h, support_single_ne_zero _ hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ ∃ x, l = single x b ∧ ↑f x = a
[PROOFSTEP]
have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ a ∈ map f l.support
[PROOFSTEP]
simp only [h_map_support, Finset.mem_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
⊢ ∃ x, l = single x b ∧ ↑f x = a
[PROOFSTEP]
rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ ∃ x, l = single x b ∧ ↑f x = a
[PROOFSTEP]
use c
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ l = single c b ∧ ↑f c = a
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ l = single c b
[PROOFSTEP]
ext d
[GOAL]
case h.left.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
⊢ ↑l d = ↑(single c b) d
[PROOFSTEP]
rw [← embDomain_apply f l, h]
[GOAL]
case h.left.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
⊢ ↑(single a b) (↑f d) = ↑(single c b) d
[PROOFSTEP]
by_cases h_cases : c = d
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : c = d
⊢ ↑(single a b) (↑f d) = ↑(single c b) d
[PROOFSTEP]
simp only [Eq.symm h_cases, hc₂, single_eq_same]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
⊢ ↑(single a b) (↑f d) = ↑(single c b) d
[PROOFSTEP]
rw [single_apply, single_apply, if_neg, if_neg h_cases]
[GOAL]
case neg.hnc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
⊢ ¬a = ↑f d
[PROOFSTEP]
by_contra hfd
[GOAL]
case neg.hnc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
hfd : a = ↑f d
⊢ False
[PROOFSTEP]
exact h_cases (f.injective (hc₂.trans hfd))
[GOAL]
case h.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ ↑f c = a
[PROOFSTEP]
exact hc₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
⊢ embDomain f (single a m) = single (↑f a) m
[PROOFSTEP]
classical
ext b
by_cases h : b ∈ Set.range f
· rcases h with ⟨a', rfl⟩
  simp [single_apply]
· simp only [embDomain_notin_range, h, single_apply, not_false_iff]
  rw [if_neg]
  rintro rfl
  simp at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
⊢ embDomain f (single a m) = single (↑f a) m
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b
[PROOFSTEP]
by_cases h : b ∈ Set.range f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : b ∈ Set.range ↑f
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b
[PROOFSTEP]
rcases h with ⟨a', rfl⟩
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
a' : α
⊢ ↑(embDomain f (single a m)) (↑f a') = ↑(single (↑f a) m) (↑f a')
[PROOFSTEP]
simp [single_apply]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b
[PROOFSTEP]
simp only [embDomain_notin_range, h, single_apply, not_false_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ 0 = if ↑f a = b then m else 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case neg.hnc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ ¬↑f a = b
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.hnc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
h : ¬↑f a ∈ Set.range ↑f
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f (↑g₁ a) (↑g₂ a) ≠ 0
⊢ a ∈ g₁.support ∪ g₂.support
[PROOFSTEP]
classical
rw [mem_union, mem_support_iff, mem_support_iff, ← not_and_or]
rintro ⟨h₁, h₂⟩; rw [h₁, h₂] at H ; exact H hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f (↑g₁ a) (↑g₂ a) ≠ 0
⊢ a ∈ g₁.support ∪ g₂.support
[PROOFSTEP]
rw [mem_union, mem_support_iff, mem_support_iff, ← not_and_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f (↑g₁ a) (↑g₂ a) ≠ 0
⊢ ¬(↑g₁ a = 0 ∧ ↑g₂ a = 0)
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f (↑g₁ a) (↑g₂ a) ≠ 0
h₁ : ↑g₁ a = 0
h₂ : ↑g₂ a = 0
⊢ False
[PROOFSTEP]
rw [h₁, h₂] at H 
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f 0 0 ≠ 0
h₁ : ↑g₁ a = 0
h₂ : ↑g₂ a = 0
⊢ False
[PROOFSTEP]
exact H hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
D : DecidableEq α
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
⊢ (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
[PROOFSTEP]
rw [Subsingleton.elim D]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
D : DecidableEq α
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
⊢ (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
[PROOFSTEP]
exact support_onFinset_subset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₁.support
⊢ a ∈ (g₁ + g₂).support
[PROOFSTEP]
have : a ∉ g₂.support := disjoint_left.1 h ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₁.support
this : ¬a ∈ g₂.support
⊢ a ∈ (g₁ + g₂).support
[PROOFSTEP]
simp only [mem_support_iff, not_not] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : ↑g₁ a ≠ 0
this : ↑g₂ a = 0
⊢ ↑(g₁ + g₂) a ≠ 0
[PROOFSTEP]
simpa only [add_apply, this, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₂.support
⊢ a ∈ (g₁ + g₂).support
[PROOFSTEP]
have : a ∉ g₁.support := disjoint_right.1 h ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₂.support
this : ¬a ∈ g₁.support
⊢ a ∈ (g₁ + g₂).support
[PROOFSTEP]
simp only [mem_support_iff, not_not] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : ↑g₂ a ≠ 0
this : ↑g₁ a = 0
⊢ ↑(g₁ + g₂) a ≠ 0
[PROOFSTEP]
simpa only [add_apply, this, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
b₁ b₂ : M
a' : α
⊢ ↑(single a (b₁ + b₂)) a' = ↑(single a b₁ + single a b₂) a'
[PROOFSTEP]
by_cases h : a = a'
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
b₁ b₂ : M
a' : α
h : a = a'
⊢ ↑(single a (b₁ + b₂)) a' = ↑(single a b₁ + single a b₂) a'
[PROOFSTEP]
rw [h, add_apply, single_eq_same, single_eq_same, single_eq_same]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
b₁ b₂ : M
a' : α
h : ¬a = a'
⊢ ↑(single a (b₁ + b₂)) a' = ↑(single a b₁ + single a b₂) a'
[PROOFSTEP]
rw [add_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ update f a b = single a b + erase a f
[PROOFSTEP]
classical
ext j
rcases eq_or_ne a j with (rfl | h)
· simp
· simp [Function.update_noteq h.symm, single_apply, h, erase_ne, h.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ update f a b = single a b + erase a f
[PROOFSTEP]
ext j
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ ↑(update f a b) j = ↑(single a b + erase a f) j
[PROOFSTEP]
rcases eq_or_ne a j with (rfl | h)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ ↑(update f a b) a = ↑(single a b + erase a f) a
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ ↑(update f a b) j = ↑(single a b + erase a f) j
[PROOFSTEP]
simp [Function.update_noteq h.symm, single_apply, h, erase_ne, h.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ update f a b = erase a f + single a b
[PROOFSTEP]
classical
ext j
rcases eq_or_ne a j with (rfl | h)
· simp
· simp [Function.update_noteq h.symm, single_apply, h, erase_ne, h.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ update f a b = erase a f + single a b
[PROOFSTEP]
ext j
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ ↑(update f a b) j = ↑(erase a f + single a b) j
[PROOFSTEP]
rcases eq_or_ne a j with (rfl | h)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ ↑(update f a b) a = ↑(erase a f + single a b) a
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ ↑(update f a b) j = ↑(erase a f + single a b) j
[PROOFSTEP]
simp [Function.update_noteq h.symm, single_apply, h, erase_ne, h.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
f : α →₀ M
⊢ single a (↑f a) + erase a f = f
[PROOFSTEP]
rw [← update_eq_single_add_erase, update_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
f : α →₀ M
⊢ erase a f + single a (↑f a) = f
[PROOFSTEP]
rw [← update_eq_erase_add_single, update_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
⊢ erase a (f + f') = erase a f + erase a f'
[PROOFSTEP]
ext s
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s
[PROOFSTEP]
by_cases hs : s = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : s = a
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s
[PROOFSTEP]
rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : ¬s = a
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s
[PROOFSTEP]
rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s : Finset α
f : α →₀ M
hf : f.support = ∅
⊢ p f
[PROOFSTEP]
rwa [support_eq_empty.1 hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p f
[PROOFSTEP]
suffices p (single a (f a) + f.erase a) by rwa [single_add_erase] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
this : p (single a (↑f a) + erase a f)
⊢ p f
[PROOFSTEP]
rwa [single_add_erase] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (single a (↑f a) + erase a f)
[PROOFSTEP]
classical
apply ha
· rw [support_erase, mem_erase]
  exact fun H => H.1 rfl
· rw [← mem_support_iff, hf]
  exact mem_cons_self _ _
· apply ih _ _
  rw [support_erase, hf, Finset.erase_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (single a (↑f a) + erase a f)
[PROOFSTEP]
apply ha
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬a ∈ (erase a f).support
[PROOFSTEP]
rw [support_erase, mem_erase]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)
[PROOFSTEP]
exact fun H => H.1 rfl
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ↑f a ≠ 0
[PROOFSTEP]
rw [← mem_support_iff, hf]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ a ∈ cons a s has
[PROOFSTEP]
exact mem_cons_self _ _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f)
[PROOFSTEP]
apply ih _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ (erase a f).support = s
[PROOFSTEP]
rw [support_erase, hf, Finset.erase_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s : Finset α
f : α →₀ M
hf : f.support = ∅
⊢ p f
[PROOFSTEP]
rwa [support_eq_empty.1 hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p f
[PROOFSTEP]
suffices p (f.erase a + single a (f a)) by rwa [erase_add_single] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
this : p (erase a f + single a (↑f a))
⊢ p f
[PROOFSTEP]
rwa [erase_add_single] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f + single a (↑f a))
[PROOFSTEP]
classical
apply ha
· rw [support_erase, mem_erase]
  exact fun H => H.1 rfl
· rw [← mem_support_iff, hf]
  exact mem_cons_self _ _
· apply ih _ _
  rw [support_erase, hf, Finset.erase_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f + single a (↑f a))
[PROOFSTEP]
apply ha
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬a ∈ (erase a f).support
[PROOFSTEP]
rw [support_erase, mem_erase]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)
[PROOFSTEP]
exact fun H => H.1 rfl
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ↑f a ≠ 0
[PROOFSTEP]
rw [← mem_support_iff, hf]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ a ∈ cons a s has
[PROOFSTEP]
exact mem_cons_self _ _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f)
[PROOFSTEP]
apply ih _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ (erase a f).support = s
[PROOFSTEP]
rw [support_erase, hf, Finset.erase_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), ↑f (single x y) = ↑g (single x y)
⊢ f = g
[PROOFSTEP]
refine' AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), ↑f (single x y) = ↑g (single x y)
⊢ Set.EqOn ↑f ↑g {f | ∃ a b, f = single a b}
[PROOFSTEP]
rintro _ ⟨x, y, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), ↑f (single x y) = ↑g (single x y)
x : α
y : M
⊢ ↑f (single x y) = ↑g (single x y)
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
⊢ f = g
[PROOFSTEP]
have := @addHom_ext α M (Additive N) _ _ (MonoidHom.toAdditive'' f) (MonoidHom.toAdditive'' g) H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
⊢ f = g
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
x✝ : Multiplicative (α →₀ M)
⊢ ↑f x✝ = ↑g x✝
[PROOFSTEP]
rw [FunLike.ext_iff] at this 
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H✝ : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this✝ : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
this : ∀ (x : α →₀ M), ↑(↑MonoidHom.toAdditive'' f) x = ↑(↑MonoidHom.toAdditive'' g) x
x✝ : Multiplicative (α →₀ M)
⊢ ↑f x✝ = ↑g x✝
[PROOFSTEP]
apply this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f : M → N
hf : f 0 = 0
hf' : ∀ (x y : M), f (x + y) = f x + f y
v₁ v₂ : α →₀ M
x✝ : α
⊢ ↑(mapRange f hf (v₁ + v₂)) x✝ = ↑(mapRange f hf v₁ + mapRange f hf v₂) x✝
[PROOFSTEP]
simp only [hf', add_apply, mapRange_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α ↪ β
⊢ (fun v => embDomain f v) 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α ↪ β
v w : α →₀ M
⊢ ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } (v + w) =
    ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } v +
      ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } w
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α ↪ β
v w : α →₀ M
b : β
⊢ ↑(ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } (v + w)) b =
    ↑(ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } v +
          ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } w)
      b
[PROOFSTEP]
by_cases h : b ∈ Set.range f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α ↪ β
v w : α →₀ M
b : β
h : b ∈ Set.range ↑f
⊢ ↑(ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } (v + w)) b =
    ↑(ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } v +
          ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } w)
      b
[PROOFSTEP]
rcases h with ⟨a, rfl⟩
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α ↪ β
v w : α →₀ M
a : α
⊢ ↑(ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } (v + w)) (↑f a) =
    ↑(ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } v +
          ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } w)
      (↑f a)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddZeroClass M
f : α ↪ β
v w : α →₀ M
b : β
h : ¬b ∈ Set.range ↑f
⊢ ↑(ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } (v + w)) b =
    ↑(ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } v +
          ZeroHom.toFun { toFun := fun v => embDomain f v, map_zero' := (_ : 0 = 0) } w)
      b
[PROOFSTEP]
simp only [Set.mem_range, not_exists, coe_add, Pi.add_apply, embDomain_notin_range _ _ _ h, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : NegZeroClass G
inst✝ : NegZeroClass H
f : G → H
hf : f 0 = 0
hf' : ∀ (x : G), f (-x) = -f x
v : α →₀ G
x✝ : α
⊢ ↑(mapRange f hf (-v)) x✝ = ↑(-mapRange f hf v) x✝
[PROOFSTEP]
simp only [hf', neg_apply, mapRange_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : SubNegZeroMonoid G
inst✝ : SubNegZeroMonoid H
f : G → H
hf : f 0 = 0
hf' : ∀ (x y : G), f (x - y) = f x - f y
v₁ v₂ : α →₀ G
x✝ : α
⊢ ↑(mapRange f hf (v₁ - v₂)) x✝ = ↑(mapRange f hf v₁ - mapRange f hf v₂) x✝
[PROOFSTEP]
simp only [hf', sub_apply, mapRange_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
[PROOFSTEP]
classical
simp_rw [FunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
exact Pi.single_add_single_eq_single_add_single hu hv
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
[PROOFSTEP]
simp_rw [FunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ ((fun a => (Pi.single k u + Pi.single l v) a) = fun a => (Pi.single m u + Pi.single n v) a) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
[PROOFSTEP]
exact Pi.single_add_single_eq_single_add_single hu hv
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : DecidableEq α
inst✝ : AddGroup G
f g : α →₀ G
⊢ (f - g).support ⊆ f.support ∪ g.support
[PROOFSTEP]
rw [sub_eq_add_neg, ← support_neg g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : DecidableEq α
inst✝ : AddGroup G
f g : α →₀ G
⊢ (f + -g).support ⊆ f.support ∪ (-g).support
[PROOFSTEP]
exact support_add
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddGroup G
f : α →₀ G
a : α
⊢ erase a f = f - single a (↑f a)
[PROOFSTEP]
ext a'
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddGroup G
f : α →₀ G
a a' : α
⊢ ↑(erase a f) a' = ↑(f - single a (↑f a)) a'
[PROOFSTEP]
rcases eq_or_ne a a' with (rfl | h)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddGroup G
f : α →₀ G
a : α
⊢ ↑(erase a f) a = ↑(f - single a (↑f a)) a
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddGroup G
f : α →₀ G
a a' : α
h : a ≠ a'
⊢ ↑(erase a f) a' = ↑(f - single a (↑f a)) a'
[PROOFSTEP]
simp [erase_ne h.symm, single_eq_of_ne h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝ : AddGroup G
f : α →₀ G
a : α
b : G
⊢ update f a b = f - single a (↑f a) + single a b
[PROOFSTEP]
rw [update_eq_erase_add_single, erase_eq_sub_single]
