ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → β i<VAR>s : Multiset ι<VAR>h : ∀ (i : ι), i ∈ s ∨ f i = 0<GOAL>{ toFun := f, support' := Trunc.mk ⟨s, h⟩ }.support ⊆ s.toFinset
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>i ∈ f.support ↔ f i ≠ 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<GOAL>f = DFinsupp.mk f.support fun i => f ↑i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Finset ι<GOAL>∀ (x : { f // f.support = s }) (i : { x // x ∈ s }), ↑((DFinsupp.subtypeSupportEqEquiv s) x i) = ↑x ↑i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Finset ι<VAR>f : (i : { x // x ∈ s }) → { x // x ≠ 0 }<GOAL>↑((DFinsupp.subtypeSupportEqEquiv s).symm f) = DFinsupp.mk s fun i => ↑(f i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<GOAL>∀ (a : Π₀ (i : ι), β i) (i : { x // x ∈ ((Equiv.sigmaFiberEquiv DFinsupp.support).symm a).fst }), ↑((DFinsupp.sigmaFinsetFunEquiv a).snd i) = a ↑i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<GOAL>∀ (a : Π₀ (i : ι), β i), (DFinsupp.sigmaFinsetFunEquiv a).fst = a.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<GOAL>DFinsupp.support 0 = ∅
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>i ∉ f.support ↔ f i = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<GOAL>f.support = ∅ ↔ f = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Set ι<VAR>f : Π₀ (i : ι), β i<GOAL>↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>b : β i<VAR>hb : b ≠ 0<GOAL>(DFinsupp.single i b).support = {i}
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>b : β i<GOAL>(DFinsupp.single i b).support ⊆ {i}
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<GOAL>DFinsupp.mapRange f hf g = DFinsupp.mk g.support fun i => f (↑i) (g ↑i)
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>i : ι<VAR>b : β₁ i<GOAL>DFinsupp.mapRange f hf (DFinsupp.single i b) = DFinsupp.single i (f i b)
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<GOAL>(DFinsupp.mapRange f hf g).support ⊆ g.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>dec : DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>g₁ : Π₀ (i : ι), β₁ i<VAR>g₂ : Π₀ (i : ι), β₂ i<GOAL>DFinsupp.zipWith f hf g₁ g₂ = DFinsupp.mk (g₁.support ∪ g₂.support) fun i => f (↑i) (g₁ ↑i) (g₂ ↑i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>g₁ : Π₀ (i : ι), β₁ i<VAR>g₂ : Π₀ (i : ι), β₂ i<GOAL>(DFinsupp.zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.erase i f = DFinsupp.mk (f.support.erase i) fun j => f ↑j
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>(DFinsupp.erase i f).support = f.support.erase i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>h : b ≠ 0<GOAL>(DFinsupp.update i f b).support = insert i f.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>Decidable (b = 0)<GOAL>(DFinsupp.update i f b).support = if b = 0 then (DFinsupp.erase i f).support else insert i f.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.filter p f = DFinsupp.mk (Finset.filter p f.support) fun i => f ↑i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : Π₀ (i : ι), β i<GOAL>(DFinsupp.filter p f).support = Finset.filter p f.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.subtypeDomain p f = DFinsupp.mk (Finset.subtype p f.support) fun i => f ↑↑i
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>f : Π₀ (i : ι), β i<GOAL>(DFinsupp.subtypeDomain p f).support = Finset.subtype p f.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>g₁ g₂ : Π₀ (i : ι), β i<GOAL>(g₁ + g₂).support ⊆ g₁.support ∪ g₂.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddGroup (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<GOAL>(-f).support = f.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>γ : Type w<VAR>Semiring γ<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → Module γ (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>b : γ<VAR>v : Π₀ (i : ι), β i<GOAL>(b • v).support ⊆ v.support
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>(i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>f : Π₀ (i : ι), β i<VAR>k : κ<GOAL>(DFinsupp.comapDomain h hh f) k = f (h k)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>(i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<GOAL>DFinsupp.comapDomain h hh 0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>(i : ι) → AddZeroClass (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>f g : Π₀ (i : ι), β i<GOAL>DFinsupp.comapDomain h hh (f + g) = DFinsupp.comapDomain h hh f + DFinsupp.comapDomain h hh g
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>Monoid γ<VAR>(i : ι) → AddMonoid (β i)<VAR>(i : ι) → DistribMulAction γ (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>r : γ<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.comapDomain h hh (r • f) = r • DFinsupp.comapDomain h hh f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>κ : Type u_1<VAR>DecidableEq κ<VAR>(i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>k : κ<VAR>x : β (h k)<GOAL>DFinsupp.comapDomain h hh (DFinsupp.single (h k) x) = DFinsupp.single k x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>(i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>f : Π₀ (i : ι), β i<VAR>k : κ<GOAL>(DFinsupp.comapDomain' h hh' f) k = f (h k)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>(i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<GOAL>DFinsupp.comapDomain' h hh' 0 = 0
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>(i : ι) → AddZeroClass (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>f g : Π₀ (i : ι), β i<GOAL>DFinsupp.comapDomain' h hh' (f + g) = DFinsupp.comapDomain' h hh' f + DFinsupp.comapDomain' h hh' g
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>Monoid γ<VAR>(i : ι) → AddMonoid (β i)<VAR>(i : ι) → DistribMulAction γ (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>r : γ<VAR>f : Π₀ (i : ι), β i<GOAL>DFinsupp.comapDomain' h hh' (r • f) = r • DFinsupp.comapDomain' h hh' f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>(i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>k : κ<VAR>x : β (h k)<GOAL>DFinsupp.comapDomain' h hh' (DFinsupp.single (h k) x) = DFinsupp.single k x
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>κ : Type u_1<VAR>(i : ι) → Zero (β i)<VAR>h : ι ≃ κ<VAR>f : Π₀ (i : ι), β i<GOAL>(DFinsupp.equivCongrLeft h) f = DFinsupp.comapDomain' ⇑h.symm ⋯ f
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>(i : ι) → (j : α i) → Zero (δ i j)<VAR>f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd<VAR>i : ι<VAR>j : α i<GOAL>(f.sigmaCurry i) j = f ⟨i, j⟩
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>(i : ι) → (j : α i) → Zero (δ i j)<GOAL>DFinsupp.sigmaCurry 0 = 0
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>(i : ι) → (j : α i) → AddZeroClass (δ i j)<VAR>f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd<GOAL>(f + g).sigmaCurry = f.sigmaCurry + g.sigmaCurry
<VAR>ι : Type u<VAR>γ : Type w<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>Monoid γ<VAR>(i : ι) → (j : α i) → AddMonoid (δ i j)<VAR>(i : ι) → (j : α i) → DistribMulAction γ (δ i j)<VAR>r : γ<VAR>f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd<GOAL>(r • f).sigmaCurry = r • f.sigmaCurry
<VAR>ι : Type u<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → (j : α i) → Zero (δ i j)<VAR>ij : (i : ι) × α i<VAR>x : δ ij.fst ij.snd<GOAL>(DFinsupp.single ij x).sigmaCurry = DFinsupp.single ij.fst (DFinsupp.single ij.snd x)
<VAR>ι : Type u<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>(i : ι) → (j : α i) → Zero (δ i j)<VAR>DecidableEq ι<VAR>f : Π₀ (i : ι) (j : α i), δ i j<VAR>i : ι<VAR>j : α i<GOAL>f.sigmaUncurry ⟨i, j⟩ = (f i) j
<VAR>ι : Type u<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>(i : ι) → (j : α i) → Zero (δ i j)<VAR>DecidableEq ι<GOAL>DFinsupp.sigmaUncurry 0 = 0
<VAR>ι : Type u<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>(i : ι) → (j : α i) → AddZeroClass (δ i j)<VAR>DecidableEq ι<VAR>f g : Π₀ (i : ι) (j : α i), δ i j<GOAL>(f + g).sigmaUncurry = f.sigmaUncurry + g.sigmaUncurry
<VAR>ι : Type u<VAR>γ : Type w<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>Monoid γ<VAR>(i : ι) → (j : α i) → AddMonoid (δ i j)<VAR>DecidableEq ι<VAR>(i : ι) → (j : α i) → DistribMulAction γ (δ i j)<VAR>r : γ<VAR>f : Π₀ (i : ι) (j : α i), δ i j<GOAL>(r • f).sigmaUncurry = r • f.sigmaUncurry
<VAR>ι : Type u<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>(i : ι) → (j : α i) → Zero (δ i j)<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>i : ι<VAR>j : α i<VAR>x : δ i j<GOAL>(DFinsupp.single i (DFinsupp.single j x)).sigmaUncurry = DFinsupp.single ⟨i, j⟩ x
<VAR>ι : Type u<VAR>α : Option ι → Type v<VAR>(i : Option ι) → Zero (α i)<VAR>f : Π₀ (i : ι), α (some i)<VAR>a : α none<GOAL>(DFinsupp.extendWith a f) none = a
<VAR>ι : Type u<VAR>α : Option ι → Type v<VAR>(i : Option ι) → Zero (α i)<VAR>f : Π₀ (i : ι), α (some i)<VAR>a : α none<VAR>i : ι<GOAL>(DFinsupp.extendWith a f) (some i) = f i
<VAR>ι : Type u<VAR>α : Option ι → Type v<VAR>DecidableEq ι<VAR>(i : Option ι) → Zero (α i)<VAR>i : ι<VAR>x : α (some i)<GOAL>DFinsupp.extendWith 0 (DFinsupp.single i x) = DFinsupp.single (some i) x
<VAR>ι : Type u<VAR>α : Option ι → Type v<VAR>DecidableEq ι<VAR>(i : Option ι) → Zero (α i)<VAR>x : α none<GOAL>DFinsupp.extendWith x 0 = DFinsupp.single none x
<VAR>ι : Type u<VAR>α : Option ι → Type v<VAR>(i : Option ι) → Zero (α i)<VAR>f : Π₀ (i : Option ι), α i<GOAL>DFinsupp.equivProdDFinsupp f = (f none, DFinsupp.comapDomain some ⋯ f)
<VAR>ι : Type u<VAR>α : Option ι → Type v<VAR>(i : Option ι) → Zero (α i)<VAR>f : α none × Π₀ (i : ι), α (some i)<GOAL>DFinsupp.equivProdDFinsupp.symm f = DFinsupp.extendWith f.1 f.2
<VAR>ι : Type u<VAR>α : Option ι → Type v<VAR>(i : Option ι) → AddZeroClass (α i)<VAR>f g : Π₀ (i : Option ι), α i<GOAL>DFinsupp.equivProdDFinsupp (f + g) = DFinsupp.equivProdDFinsupp f + DFinsupp.equivProdDFinsupp g
<VAR>ι : Type u<VAR>γ : Type w<VAR>α : Option ι → Type v<VAR>Monoid γ<VAR>(i : Option ι) → AddMonoid (α i)<VAR>(i : Option ι) → DistribMulAction γ (α i)<VAR>r : γ<VAR>f : Π₀ (i : Option ι), α i<GOAL>DFinsupp.equivProdDFinsupp (r • f) = r • DFinsupp.equivProdDFinsupp f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid R<VAR>CommMonoid S<VAR>FunLike H R S<VAR>MonoidHomClass H R S<VAR>h : H<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → R<GOAL>h (f.prod g) = f.prod fun a b => h (g a b)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid R<VAR>AddCommMonoid S<VAR>FunLike H R S<VAR>AddMonoidHomClass H R S<VAR>h : H<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → R<GOAL>h (f.sum g) = f.sum fun a b => h (g a b)
<VAR>ι : Type u<VAR>γ : Type w<VAR>DecidableEq ι<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<VAR>h : (i : ι) → β₂ i → γ<VAR>h0 : ∀ (i : ι), h i 0 = 1<GOAL>(DFinsupp.mapRange f hf g).prod h = g.prod fun i b => h i (f i b)
<VAR>ι : Type u<VAR>γ : Type w<VAR>DecidableEq ι<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → Zero (β₁ i)<VAR>(i : ι) → Zero (β₂ i)<VAR>(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<VAR>h : (i : ι) → β₂ i → γ<VAR>h0 : ∀ (i : ι), h i 0 = 0<GOAL>(DFinsupp.mapRange f hf g).sum h = g.sum fun i b => h i (f i b)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>h : (i : ι) → β i → γ<GOAL>DFinsupp.prod 0 h = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>h : (i : ι) → β i → γ<GOAL>DFinsupp.sum 0 h = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>i : ι<VAR>b : β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : h i 0 = 1<GOAL>(DFinsupp.single i b).prod h = h i b
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>i : ι<VAR>b : β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : h i 0 = 0<GOAL>(DFinsupp.single i b).sum h = h i b
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddGroup (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h0 : ∀ (i : ι), h i 0 = 1<GOAL>(-g).prod h = g.prod fun i b => h i (-b)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddGroup (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h0 : ∀ (i : ι), h i 0 = 0<GOAL>(-g).sum h = g.sum fun i b => h i (-b)
<VAR>γ : Type w<VAR>ι₁ : Type u_3<VAR>ι₂ : Type u_4<VAR>β₁ : ι₁ → Type u_1<VAR>β₂ : ι₂ → Type u_2<VAR>DecidableEq ι₁<VAR>DecidableEq ι₂<VAR>(i : ι₁) → Zero (β₁ i)<VAR>(i : ι₂) → Zero (β₂ i)<VAR>(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>f₁ : Π₀ (i : ι₁), β₁ i<VAR>f₂ : Π₀ (i : ι₂), β₂ i<VAR>h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ<GOAL>(f₁.sum fun i₁ x₁ => f₂.sum fun i₂ x₂ => h i₁ x₁ i₂ x₂) = f₂.sum fun i₂ x₂ => f₁.sum fun i₁ x₁ => h i₁ x₁ i₂ x₂
<VAR>γ : Type w<VAR>ι₁ : Type u_3<VAR>ι₂ : Type u_4<VAR>β₁ : ι₁ → Type u_1<VAR>β₂ : ι₂ → Type u_2<VAR>DecidableEq ι₁<VAR>DecidableEq ι₂<VAR>(i : ι₁) → Zero (β₁ i)<VAR>(i : ι₂) → Zero (β₂ i)<VAR>(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>f₁ : Π₀ (i : ι₁), β₁ i<VAR>f₂ : Π₀ (i : ι₂), β₂ i<VAR>h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ<GOAL>(f₁.prod fun i₁ x₁ => f₂.prod fun i₂ x₂ => h i₁ x₁ i₂ x₂) = f₂.prod fun i₂ x₂ => f₁.prod fun i₁ x₁ => h i₁ x₁ i₂ x₂
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>ι₁ : Type u₁<VAR>DecidableEq ι₁<VAR>β₁ : ι₁ → Type v₁<VAR>(i₁ : ι₁) → Zero (β₁ i₁)<VAR>(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → AddCommMonoid (β i)<VAR>f : Π₀ (i₁ : ι₁), β₁ i₁<VAR>g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i<VAR>i₂ : ι<GOAL>(f.sum g) i₂ = f.sum fun i₁ b => (g i₁ b) i₂
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>ι₁ : Type u₁<VAR>DecidableEq ι₁<VAR>β₁ : ι₁ → Type v₁<VAR>(i₁ : ι₁) → Zero (β₁ i₁)<VAR>(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i₁ : ι₁), β₁ i₁<VAR>g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i<GOAL>(f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>f : Π₀ (i : ι), β i<GOAL>(f.sum fun x x => 0) = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>f : Π₀ (i : ι), β i<GOAL>(f.prod fun x x => 1) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>f : Π₀ (i : ι), β i<VAR>h₁ h₂ : (i : ι) → β i → γ<GOAL>(f.sum fun i b => h₁ i b + h₂ i b) = f.sum h₁ + f.sum h₂
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>f : Π₀ (i : ι), β i<VAR>h₁ h₂ : (i : ι) → β i → γ<GOAL>(f.prod fun i b => h₁ i b * h₂ i b) = f.prod h₁ * f.prod h₂
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommGroup γ<VAR>f : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<GOAL>(f.sum fun i b => -h i b) = -f.sum h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommGroup γ<VAR>f : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<GOAL>(f.prod fun i b => (h i b)⁻¹) = (f.prod h)⁻¹
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>f : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>hyp : ∀ (i : ι), h i (f i) = 1<GOAL>f.prod h = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>f : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>hyp : ∀ (i : ι), h i (f i) = 0<GOAL>f.sum h = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>α : Type u_1<VAR>Monoid α<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>DistribMulAction α γ<VAR>f : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>c : α<GOAL>c • f.sum h = f.sum fun a b => c • h a b
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 1<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂<GOAL>(f + g).prod h = f.prod h * g.prod h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 0<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂<GOAL>(f + g).sum h = f.sum h + g.sum h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>S : Type u_1<VAR>SetLike S γ<VAR>AddSubmonoidClass S γ<VAR>s : S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → γ<VAR>h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s<GOAL>f.sum g ∈ s
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>S : Type u_1<VAR>SetLike S γ<VAR>SubmonoidClass S γ<VAR>s : S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → γ<VAR>h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s<GOAL>f.prod g ∈ s
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>Fintype ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>f : (i : ι) → β i → γ<VAR>hf : ∀ (i : ι), f i 0 = 1<GOAL>v.prod f = ∏ i : ι, f i (DFinsupp.equivFunOnFintype v i)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>Fintype ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>f : (i : ι) → β i → γ<VAR>hf : ∀ (i : ι), f i 0 = 0<GOAL>v.sum f = ∑ i : ι, f i (DFinsupp.equivFunOnFintype v i)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>CommMonoidWithZero γ<VAR>Nontrivial γ<VAR>NoZeroDivisors γ<VAR>(i : ι) → DecidableEq (β i)<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → γ<GOAL>f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>CommMonoidWithZero γ<VAR>Nontrivial γ<VAR>NoZeroDivisors γ<VAR>(i : ι) → DecidableEq (β i)<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → γ<GOAL>f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>i : ι<VAR>x : β i<GOAL>(DFinsupp.sumAddHom φ) (DFinsupp.single i x) = (φ i) x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>f : (i : ι) → β i →+ γ<VAR>i : ι<GOAL>(DFinsupp.sumAddHom f).comp (DFinsupp.singleAddHom β i) = f i