[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f✝ g✝ f g : α →₀ N
a : α
⊢ a ∈ neLocus f g ↔ ↑f a ≠ ↑g a
[PROOFSTEP]
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff, and_iff_right_iff_imp] using Ne.ne_or_ne _
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ ↑(neLocus f g) = {x | ↑f x ≠ ↑g x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
x✝ : α
⊢ x✝ ∈ ↑(neLocus f g) ↔ x✝ ∈ {x | ↑f x ≠ ↑g x}
[PROOFSTEP]
exact mem_neLocus
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f✝ g✝ f g : α →₀ N
h : f = g
⊢ neLocus f f = ∅
[PROOFSTEP]
simp only [neLocus, Ne.def, eq_self_iff_true, not_true, Finset.filter_False]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ neLocus f g = neLocus g f
[PROOFSTEP]
simp_rw [neLocus, Finset.union_comm, ne_comm]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ neLocus f 0 = f.support
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
a✝ : α
⊢ a✝ ∈ neLocus f 0 ↔ a✝ ∈ f.support
[PROOFSTEP]
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : Zero N
inst✝¹ : DecidableEq M
inst✝ : Zero M
f g : α →₀ N
F : N → M
F0 : F 0 = 0
x : α
⊢ x ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) → x ∈ neLocus f g
[PROOFSTEP]
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
⊢ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) = neLocus g₁ g₂
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
a✝ : α
⊢ a✝ ∈ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) ↔ a✝ ∈ neLocus g₁ g₂
[PROOFSTEP]
simpa only [mem_neLocus] using (hF _).ne_iff
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f => F f g
⊢ neLocus (zipWith F F0 f₁ g) (zipWith F F0 f₂ g) = neLocus f₁ f₂
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f => F f g
a✝ : α
⊢ a✝ ∈ neLocus (zipWith F F0 f₁ g) (zipWith F F0 f₂ g) ↔ a✝ ∈ neLocus f₁ f₂
[PROOFSTEP]
simpa only [mem_neLocus] using (hF _).ne_iff
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
⊢ neLocus (mapRange F F0 f) (mapRange F F0 g) = neLocus f g
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
a✝ : α
⊢ a✝ ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) ↔ a✝ ∈ neLocus f g
[PROOFSTEP]
simpa only [mem_neLocus] using hF.ne_iff
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (-f) g = neLocus f (-g)
[PROOFSTEP]
rw [← neLocus_neg_neg, neg_neg]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus f g = (f - g).support
[PROOFSTEP]
rw [← neLocus_add_right _ _ (-g), add_right_neg, neLocus_zero_right, sub_eq_add_neg]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂
[PROOFSTEP]
simp only [sub_eq_add_neg, neLocus_add_left, neLocus_neg_neg]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂
[PROOFSTEP]
simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus f (f + g) = g.support
[PROOFSTEP]
rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f + g) f = g.support
[PROOFSTEP]
rw [neLocus_comm, neLocus_self_add_right]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus f (f - g) = g.support
[PROOFSTEP]
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f - g) f = g.support
[PROOFSTEP]
rw [neLocus_comm, neLocus_self_sub_right]
