Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Johannes Hölzl, Kenny Lau

! This file was ported from Lean 3 source module data.dfinsupp.basic
! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Module.LinearMap
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Set.Finite
import Mathlib.GroupTheory.Submonoid.Membership
import Mathlib.GroupTheory.GroupAction.BigOperators
import Mathlib.Data.Finset.Preimage

/-!
# Dependent functions with finite support

For a non-dependent version see `data/finsupp.lean`.

## Notation

This file introduces the notation `Π₀ a, β a` as notation for `Dfinsupp β`, mirroring the `α →₀ β`
notation used for `Finsupp`. This works for nested binders too, with `Π₀ a b, γ a b` as notation
for `Dfinsupp (λ a, Dfinsupp (γ a))`.

## Implementation notes

The support is internally represented (in the primed `Dfinsupp.support'`) as a `Multiset` that
represents a superset of the true support of the function, quotiented by the always-true relation so
that this does not impact equality. This approach has computational benefits over storing a
`Finset`; it allows us to add together two finitely-supported functions without
having to evaluate the resulting function to recompute its support (which would required
decidability of `b = 0` for `b : β i`).

The true support of the function can still be recovered with `Dfinsupp.support`; but these
decidability obligations are now postponed to when the support is actually needed. As a consequence,
there are two ways to sum a `Dfinsupp`: with `Dfinsupp.sum` which works over an arbitrary function
but requires recomputation of the support and therefore a `Decidable` argument; and with
`Dfinsupp.sumAddHom` which requires an additive morphism, using its properties to show that
summing over a superset of the support is sufficient.

`Finsupp` takes an altogether different approach here; it uses `Classical.Decidable` and declares
the `Add` instance as noncomputable. This design difference is independent of the fact that
`Dfinsupp` is dependently-typed and `Finsupp` is not; in future, we may want to align these two
definitions, or introduce two more definitions for the other combinations of decisions.
-/

universe u u₁ u₂ v v₁ v₂ v₃ w x y l

open BigOperators

variable {ι: Type uι : Type u: Type (u+1)Type u} {γ: Type wγ : Type w: Type (w+1)Type w} {β: ι → Type vβ : ι: Type uι → Type v: Type (v+1)Type v} {β₁: ι → Type v₁β₁ : ι: Type uι → Type v₁: Type (v₁+1)Type v₁} {β₂: ι → Type v₂β₂ : ι: Type uι → Type v₂: Type (v₂+1)Type v₂}

variable (β: ?m.34β)

/-- A dependent function `Π i, β i` with finite support, with notation `Π₀ i, β i`.

Note that `Dfinsupp.support` is the preferred API for accessing the support of the function,
`Dfinsupp.support'` is a implementation detail that aids computability; see the implementation
structure Dfinsupp: {ι : Type u} → (β : ι → Type v) → [inst : (i : ι) → Zero (β i)] → Type (maxuv)Dfinsupp [∀ i: ?m.54i, Zero: Type ?u.57 → Type ?u.57Zero (β: ι → Type vβ i: ?m.54i)] : Type max u v: Type ((maxuv)+1)Type max u v where mk': {ι : Type u} →
{β : ι → Type v} →
[inst : (i : ι) → Zero (β i)] → (toFun : (i : ι) → β i) → Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun i = 0 } → Dfinsupp βmk' ::
/-- The underlying function of a dependent function with finite support (aka `Dfinsupp`). -/
toFun: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → Dfinsupp β → (i : ι) → β itoFun : ∀ i: ?m.63i, β: ι → Type vβ i: ?m.63i
/-- The support of a dependent function with finite support (aka `Dfinsupp`). -/
support': {ι : Type u} →
{β : ι → Type v} →
[inst : (i : ι) → Zero (β i)] → (self : Dfinsupp β) → Trunc { s // ∀ (i : ι), i ∈ s ∨ Dfinsupp.toFun self i = 0 }support' : Trunc: Sort ?u.68 → Sort ?u.68Trunc { s: Multiset ιs : Multiset: Type ?u.72 → Type ?u.72Multiset ι: Type uι // ∀ i: ?m.75i, i: ?m.75i ∈ s: Multiset ιs ∨ toFun: (i : ι) → β itoFun i: ?m.75i = 0: ?m.990 }
#align dfinsupp Dfinsupp: {ι : Type u} → (β : ι → Type v) → [inst : (i : ι) → Zero (β i)] → Type (maxuv)Dfinsupp

variable {β: ?m.772β}

-- mathport name: «exprΠ₀ , »
/-- `Π₀ i, β i` denotes the type of dependent functions with finite support `Dfinsupp β`. -/
notation3"Π₀ "(...)", "r: ?m.934r:(scoped f => Dfinsupp f) => r

-- mathport name: «expr →ₚ »
@[inherit_doc]
infixl:25 " →ₚ " => Dfinsupp: {ι : Type u} → (β : ι → Type v) → [inst : (i : ι) → Zero (β i)] → Type (maxuv)Dfinsupp

namespace Dfinsupp

section Basic

variable [∀ i: ?m.11496i, Zero: Type ?u.11539 → Type ?u.11539Zero (β: ι → Type vβ i: ?m.12525i)] [∀ i: ?m.15743i, Zero: Type ?u.15427 → Type ?u.15427Zero (β₁: ι → Type v₁β₁ i: ?m.15424i)] [∀ i: ?m.15751i, Zero: Type ?u.12870 → Type ?u.12870Zero (β₂: ι → Type v₂β₂ i: ?m.15432i)]

instance funLike: FunLike (Dfinsupp fun i => β i) ι βfunLike : FunLike: Sort ?u.11561 →
(α : outParam (Sort ?u.11560)) → outParam (α → Sort ?u.11559) → Sort (max(max(max1?u.11561)?u.11560)?u.11559)FunLike (Π₀ i: ?m.11566i, β: ι → Type vβ i: ?m.11566i) ι: Type uι β: ι → Type vβ :=
⟨fun f: ?m.11632f => f: ?m.11632f.toFun: {ι : Type ?u.11635} → {β : ι → Type ?u.11634} → [inst : (i : ι) → Zero (β i)] → Dfinsupp β → (i : ι) → β itoFun, fun ⟨f₁: (i : ι) → β if₁, s₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }s₁⟩ ⟨f₂: (i : ι) → β if₂, s₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₂ i = 0 }s₁⟩ ↦ fun (h: f₁ = f₂h : f₁: (i : ι) → β if₁ = f₂: (i : ι) → β if₂) ↦ byGoals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)x✝¹, x✝: Dfinsupp fun i => β if₁: (i : ι) → β is₁✝: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }f₂: (i : ι) → β is₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₂ i = 0 }h: f₁ = f₂{ toFun := f₁, support' := s₁✝ } = { toFun := f₂, support' := s₁ }subst h: f₁ = f₂hι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)x✝¹, x✝: Dfinsupp fun i => β if₁: (i : ι) → β is₁✝, s₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }{ toFun := f₁, support' := s₁✝ } = { toFun := f₁, support' := s₁ }
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)x✝¹, x✝: Dfinsupp fun i => β if₁: (i : ι) → β is₁✝: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }f₂: (i : ι) → β is₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₂ i = 0 }h: f₁ = f₂{ toFun := f₁, support' := s₁✝ } = { toFun := f₂, support' := s₁ }congrι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)x✝¹, x✝: Dfinsupp fun i => β if₁: (i : ι) → β is₁✝, s₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }e_support's₁✝ = s₁
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)x✝¹, x✝: Dfinsupp fun i => β if₁: (i : ι) → β is₁✝: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }f₂: (i : ι) → β is₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₂ i = 0 }h: f₁ = f₂{ toFun := f₁, support' := s₁✝ } = { toFun := f₂, support' := s₁ }apply Subsingleton.elim: ∀ {α : Sort ?u.12327} [h : Subsingleton α] (a b : α), a = bSubsingleton.elimGoals accomplished! 🐙 ⟩
#align dfinsupp.fun_like Dfinsupp.funLike: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → FunLike (Dfinsupp fun i => β i) ι βDfinsupp.funLike

/-- Helper instance for when there are too many metavariables to apply `FunLike.coeFunForall`
directly. -/
instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → CoeFun (Dfinsupp fun i => β i) fun x => (i : ι) → β iinstance : CoeFun: (α : Sort ?u.12549) → outParam (α → Sort ?u.12548) → Sort (max(max1?u.12549)?u.12548)CoeFun (Π₀ i: ?m.12554i, β: ι → Type vβ i: ?m.12554i) fun _: ?m.12597_ => ∀ i: ?m.12600i, β: ι → Type vβ i: ?m.12600i :=
inferInstance: {α : Sort ?u.12616} → [i : α] → αinferInstance

@[simp]
theorem toFun_eq_coe: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (f : Dfinsupp fun i => β i), f.toFun = ↑ftoFun_eq_coe (f: Dfinsupp fun i => β if : Π₀ i: ?m.12878i, β: ι → Type vβ i: ?m.12878i) : f: Dfinsupp fun i => β if.toFun: {ι : Type ?u.12924} → {β : ι → Type ?u.12923} → [inst : (i : ι) → Zero (β i)] → Dfinsupp β → (i : ι) → β itoFun = f: Dfinsupp fun i => β if :=
rfl: ∀ {α : Sort ?u.13190} {a : α}, a = arfl
#align dfinsupp.to_fun_eq_coe Dfinsupp.toFun_eq_coe: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (f : Dfinsupp fun i => β i), f.toFun = ↑fDfinsupp.toFun_eq_coe

@[ext]
theorem ext: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {f g : Dfinsupp fun i => β i},
(∀ (i : ι), ↑f i = ↑g i) → f = gext {f: Dfinsupp fun i => β if g: Dfinsupp fun i => β ig : Π₀ i: ?m.13258i, β: ι → Type vβ i: ?m.13258i} (h: ∀ (i : ι), ↑f i = ↑g ih : ∀ i: ?m.13318i, f: Dfinsupp fun i => β if i: ?m.13318i = g: Dfinsupp fun i => β ig i: ?m.13318i) : f: Dfinsupp fun i => β if = g: Dfinsupp fun i => β ig :=
FunLike.ext: ∀ {F : Sort ?u.13422} {α : Sort ?u.13423} {β : α → Sort ?u.13421} [i : FunLike F α β] (f g : F),
(∀ (x : α), ↑f x = ↑g x) → f = gFunLike.ext _: ?m.13424_ _: ?m.13424_ h: ∀ (i : ι), ↑f i = ↑g ih
#align dfinsupp.ext Dfinsupp.ext: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {f g : Dfinsupp fun i => β i},
(∀ (i : ι), ↑f i = ↑g i) → f = gDfinsupp.ext

@[deprecated FunLike.ext_iff: ∀ {F : Sort u_1} {α : Sort u_3} {β : α → Sort u_2} [i : FunLike F α β] {f g : F}, f = g ↔ ∀ (x : α), ↑f x = ↑g xFunLike.ext_iff]
theorem ext_iff: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {f g : Dfinsupp fun i => β i},
f = g ↔ ∀ (i : ι), ↑f i = ↑g iext_iff {f: Dfinsupp fun i => β if g: Dfinsupp fun i => β ig : Π₀ i: ?m.13668i, β: ι → Type vβ i: ?m.13668i} : f: Dfinsupp fun i => β if = g: Dfinsupp fun i => β ig ↔ ∀ i: ?m.13735i, f: Dfinsupp fun i => β if i: ?m.13735i = g: Dfinsupp fun i => β ig i: ?m.13735i :=
FunLike.ext_iff: ∀ {F : Sort ?u.13829} {α : Sort ?u.13831} {β : α → Sort ?u.13830} [i : FunLike F α β] {f g : F},
f = g ↔ ∀ (x : α), ↑f x = ↑g xFunLike.ext_iff
#align dfinsupp.ext_iff Dfinsupp.ext_iff: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {f g : Dfinsupp fun i => β i},
f = g ↔ ∀ (i : ι), ↑f i = ↑g iDfinsupp.ext_iff

@[deprecated FunLike.coe_injective: ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective]
theorem coeFn_injective: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)], Function.Injective FunLike.coecoeFn_injective : @Function.Injective: {α : Sort ?u.14057} → {β : Sort ?u.14056} → (α → β) → PropFunction.Injective (Π₀ i: ?m.14062i, β: ι → Type vβ i: ?m.14062i) (∀ i: ?m.14105i, β: ι → Type vβ i: ?m.14105i) (⇑): (Dfinsupp fun i => (fun i => β i) i) → (a : ι) → (fun i => (fun i => β i) i) a(⇑) :=
FunLike.coe_injective: ∀ {F : Sort ?u.14168} {α : Sort ?u.14169} {β : α → Sort ?u.14170} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective
#align dfinsupp.coe_fn_injective Dfinsupp.coeFn_injective: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)], Function.Injective FunLike.coeDfinsupp.coeFn_injective

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → Zero (Dfinsupp fun i => β i)instance : Zero: Type ?u.14398 → Type ?u.14398Zero (Π₀ i: ?m.14403i, β: ι → Type vβ i: ?m.14403i) :=
⟨⟨0: ?m.145250, Trunc.mk: {α : Sort ?u.14598} → α → Trunc αTrunc.mk <| ⟨∅: ?m.14615∅, fun _: ?m.14661_ => Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr rfl: ∀ {α : Sort ?u.14667} {a : α}, a = arfl⟩⟩⟩

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → Inhabited (Dfinsupp fun i => β i)instance : Inhabited: Sort ?u.14874 → Sort (max1?u.14874)Inhabited (Π₀ i: ?m.14879i, β: ι → Type vβ i: ?m.14879i) :=
⟨0: ?m.149290⟩

@[simp]
theorem coe_mk': ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (f : (i : ι) → β i)
(s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }), ↑{ toFun := f, support' := s } = fcoe_mk' (f: (i : ι) → β if : ∀ i: ?m.15123i, β: ι → Type vβ i: ?m.15123i) (s: Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }s) : ⇑(⟨f: (i : ι) → β if, s: ?m.15128s⟩ : Π₀ i: ?m.15137i, β: ι → Type vβ i: ?m.15137i) = f: (i : ι) → β if :=
rfl: ∀ {α : Sort ?u.15346} {a : α}, a = arfl
#align dfinsupp.coe_mk' Dfinsupp.coe_mk': ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (f : (i : ι) → β i)
(s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }), ↑{ toFun := f, support' := s } = fDfinsupp.coe_mk'

@[simp]
theorem coe_zero: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)], ↑0 = 0coe_zero : ⇑(0: ?m.154880 : Π₀ i: ?m.15445i, β: ι → Type vβ i: ?m.15445i) = 0: ?m.155900 :=
rfl: ∀ {α : Sort ?u.15674} {a : α}, a = arfl
#align dfinsupp.coe_zero Dfinsupp.coe_zero: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)], ↑0 = 0Dfinsupp.coe_zero

theorem zero_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (i : ι), ↑0 i = 0zero_apply (i: ιi : ι: Type uι) : (0: ?m.158090 : Π₀ i: ?m.15766i, β: ι → Type vβ i: ?m.15766i) i: ιi = 0: ?m.159110 :=
rfl: ∀ {α : Sort ?u.15959} {a : α}, a = arfl
#align dfinsupp.zero_apply Dfinsupp.zero_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (i : ι), ↑0 i = 0Dfinsupp.zero_apply

/-- The composition of `f : β₁ → β₂` and `g : Π₀ i, β₁ i` is
`mapRange f hf g : Π₀ i, β₂ i`, well defined when `f 0 = 0`.

This preserves the structure on `f`, and exists in various bundled forms for when `f` is itself
bundled:

* `dfinsupp.mapRange.linearMap`
* `dfinsupp.mapRange.linearEquiv`
-/
def mapRange: {ι : Type u} →
{β₁ : ι → Type v₁} →
{β₂ : ι → Type v₂} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange (f: (i : ι) → β₁ i → β₂ if : ∀ i: ?m.16020i, β₁: ι → Type v₁β₁ i: ?m.16020i → β₂: ι → Type v₂β₂ i: ?m.16020i) (hf: ∀ (i : ι), f i 0 = 0hf : ∀ i: ?m.16028i, f: (i : ι) → β₁ i → β₂ if i: ?m.16028i 0: ?m.160330 = 0: ?m.160660) (x: Dfinsupp fun i => β₁ ix : Π₀ i: ?m.16117i, β₁: ι → Type v₁β₁ i: ?m.16117i) : Π₀ i: ?m.16160i, β₂: ι → Type v₂β₂ i: ?m.16160i :=
⟨fun i: ?m.16273i => f: (i : ι) → β₁ i → β₂ if i: ?m.16273i (x: Dfinsupp fun i => β₁ ix i: ?m.16273i),
x: Dfinsupp fun i => β₁ ix.support': {ι : Type ?u.16325} →
{β : ι → Type ?u.16324} →
[inst : (i : ι) → Zero (β i)] → (self : Dfinsupp β) → Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun self i = 0 }support'.map: {α : Sort ?u.16367} → {β : Sort ?u.16366} → (α → β) → Trunc α → Trunc βmap fun s: ?m.16376s => ⟨s: ?m.16376s.1: {α : Sort ?u.16436} → {p : α → Prop} → Subtype p → α1, fun i: ?m.16393i => (s: ?m.16376s.2: ∀ {α : Sort ?u.16442} {p : α → Prop} (self : Subtype p), p ↑self2 i: ?m.16393i).imp_right: ∀ {b c a : Prop}, (b → c) → a ∨ b → a ∨ cimp_right fun h: ↑x i = 0h : x: Dfinsupp fun i => β₁ ix i: ?m.16393i = 0: ?m.164950 => byGoals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ ihf: ∀ (i : ι), f i 0 = 0x: Dfinsupp fun i => β₁ is: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }i: ιh: ↑x i = 0(fun i => f i (↑x i)) i = 0rw [ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ ihf: ∀ (i : ι), f i 0 = 0x: Dfinsupp fun i => β₁ is: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }i: ιh: ↑x i = 0(fun i => f i (↑x i)) i = 0← hf: ∀ (i : ι), f i 0 = 0hf i: ιi,ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ ihf: ∀ (i : ι), f i 0 = 0x: Dfinsupp fun i => β₁ is: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }i: ιh: ↑x i = 0(fun i => f i (↑x i)) i = f i 0 ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ ihf: ∀ (i : ι), f i 0 = 0x: Dfinsupp fun i => β₁ is: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }i: ιh: ↑x i = 0(fun i => f i (↑x i)) i = 0← h: ↑x i = 0hι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ ihf: ∀ (i : ι), f i 0 = 0x: Dfinsupp fun i => β₁ is: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }i: ιh: ↑x i = 0(fun i => f i (↑x i)) i = f i (↑x i)]Goals accomplished! 🐙⟩⟩
#align dfinsupp.map_range Dfinsupp.mapRange: {ι : Type u} →
{β₁ : ι → Type v₁} →
{β₂ : ι → Type v₂} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ iDfinsupp.mapRange

@[simp]
theorem mapRange_apply: ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
(f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Dfinsupp fun i => β₁ i) (i : ι),
↑(mapRange f hf g) i = f i (↑g i)mapRange_apply (f: (i : ι) → β₁ i → β₂ if : ∀ i: ?m.16855i, β₁: ι → Type v₁β₁ i: ?m.16855i → β₂: ι → Type v₂β₂ i: ?m.16855i) (hf: ∀ (i : ι), f i 0 = 0hf : ∀ i: ?m.16863i, f: (i : ι) → β₁ i → β₂ if i: ?m.16863i 0: ?m.168680 = 0: ?m.169010) (g: Dfinsupp fun i => β₁ ig : Π₀ i: ?m.16952i, β₁: ι → Type v₁β₁ i: ?m.16952i) (i: ιi : ι: Type uι) :
mapRange: {ι : Type ?u.16996} →
{β₁ : ι → Type ?u.16995} →
{β₂ : ι → Type ?u.16994} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange f: (i : ι) → β₁ i → β₂ if hf: ∀ (i : ι), f i 0 = 0hf g: Dfinsupp fun i => β₁ ig i: ιi = f: (i : ι) → β₁ i → β₂ if i: ιi (g: Dfinsupp fun i => β₁ ig i: ιi) :=
rfl: ∀ {α : Sort ?u.17202} {a : α}, a = arfl
#align dfinsupp.map_range_apply Dfinsupp.mapRange_apply: ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
(f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Dfinsupp fun i => β₁ i) (i : ι),
↑(mapRange f hf g) i = f i (↑g i)Dfinsupp.mapRange_apply

@[simp]
theorem mapRange_id: ∀ {ι : Type u} {β₁ : ι → Type v₁} [inst : (i : ι) → Zero (β₁ i)]
(h : optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)) (g : Dfinsupp fun i => β₁ i),
mapRange (fun i => id) h g = gmapRange_id (h: optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)h : ∀ i: ?m.17319i, id: {α : Sort ?u.17323} → α → αid (0: ?m.173270 : β₁: ι → Type v₁β₁ i: ?m.17319i) = 0: ?m.173600 := fun i: ?m.17378i => rfl: ∀ {α : Sort ?u.17380} {a : α}, a = arfl) (g: Dfinsupp fun i => β₁ ig : Π₀ i: ιi : ι: Type uι, β₁: ι → Type v₁β₁ i: ιi) :
mapRange: {ι : Type ?u.17436} →
{β₁ : ι → Type ?u.17435} →
{β₂ : ι → Type ?u.17434} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange (fun i: ?m.17443i => (id: {α : Sort ?u.17448} → α → αid : β₁: ι → Type v₁β₁ i: ?m.17443i → β₁: ι → Type v₁β₁ i: ?m.17443i)) h: optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)h g: Dfinsupp fun i => β₁ ig = g: Dfinsupp fun i => β₁ ig := byGoals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)h: optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)g: Dfinsupp fun i => β₁ imapRange (fun i => id) h g = gextι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)h: optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)g: Dfinsupp fun i => β₁ ii✝: ιh↑(mapRange (fun i => id) h g) i✝ = ↑g i✝
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)h: optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)g: Dfinsupp fun i => β₁ imapRange (fun i => id) h g = grflGoals accomplished! 🐙
#align dfinsupp.map_range_id Dfinsupp.mapRange_id: ∀ {ι : Type u} {β₁ : ι → Type v₁} [inst : (i : ι) → Zero (β₁ i)]
(h : optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)) (g : Dfinsupp fun i => β₁ i),
mapRange (fun i => id) h g = gDfinsupp.mapRange_id

theorem mapRange_comp: ∀ (f : (i : ι) → β₁ i → β₂ i) (f₂ : (i : ι) → β i → β₁ i) (hf : ∀ (i : ι), f i 0 = 0) (hf₂ : ∀ (i : ι), f₂ i 0 = 0)
(h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0) (g : Dfinsupp fun i => β i),
mapRange (fun i => f i ∘ f₂ i) h g = mapRange f hf (mapRange f₂ hf₂ g)mapRange_comp (f: (i : ι) → β₁ i → β₂ if : ∀ i: ?m.17661i, β₁: ι → Type v₁β₁ i: ?m.17661i → β₂: ι → Type v₂β₂ i: ?m.17661i) (f₂: (i : ι) → β i → β₁ if₂ : ∀ i: ?m.17669i, β: ι → Type vβ i: ?m.17669i → β₁: ι → Type v₁β₁ i: ?m.17669i) (hf: ∀ (i : ι), f i 0 = 0hf : ∀ i: ?m.17677i, f: (i : ι) → β₁ i → β₂ if i: ?m.17677i 0: ?m.176820 = 0: ?m.177150)
(hf₂: ∀ (i : ι), f₂ i 0 = 0hf₂ : ∀ i: ?m.17763i, f₂: (i : ι) → β i → β₁ if₂ i: ?m.17763i 0: ?m.177680 = 0: ?m.178020) (h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0h : ∀ i: ?m.17843i, (f: (i : ι) → β₁ i → β₂ if i: ?m.17843i ∘ f₂: (i : ι) → β i → β₁ if₂ i: ?m.17843i) 0: ?m.178610 = 0: ?m.178870) (g: Dfinsupp fun i => β ig : Π₀ i: ιi : ι: Type uι, β: ι → Type vβ i: ιi) :
mapRange: {ι : Type ?u.17973} →
{β₁ : ι → Type ?u.17972} →
{β₂ : ι → Type ?u.17971} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange (fun i: ?m.17980i => f: (i : ι) → β₁ i → β₂ if i: ?m.17980i ∘ f₂: (i : ι) → β i → β₁ if₂ i: ?m.17980i) h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0h g: Dfinsupp fun i => β ig = mapRange: {ι : Type ?u.18101} →
{β₁ : ι → Type ?u.18100} →
{β₂ : ι → Type ?u.18099} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange f: (i : ι) → β₁ i → β₂ if hf: ∀ (i : ι), f i 0 = 0hf (mapRange: {ι : Type ?u.18160} →
{β₁ : ι → Type ?u.18159} →
{β₂ : ι → Type ?u.18158} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange f₂: (i : ι) → β i → β₁ if₂ hf₂: ∀ (i : ι), f₂ i 0 = 0hf₂ g: Dfinsupp fun i => β ig) := byGoals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ if₂: (i : ι) → β i → β₁ ihf: ∀ (i : ι), f i 0 = 0hf₂: ∀ (i : ι), f₂ i 0 = 0h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0g: Dfinsupp fun i => β imapRange (fun i => f i ∘ f₂ i) h g = mapRange f hf (mapRange f₂ hf₂ g)extι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ if₂: (i : ι) → β i → β₁ ihf: ∀ (i : ι), f i 0 = 0hf₂: ∀ (i : ι), f₂ i 0 = 0h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0g: Dfinsupp fun i => β ii✝: ιh↑(mapRange (fun i => f i ∘ f₂ i) h g) i✝ = ↑(mapRange f hf (mapRange f₂ hf₂ g)) i✝
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ if₂: (i : ι) → β i → β₁ ihf: ∀ (i : ι), f i 0 = 0hf₂: ∀ (i : ι), f₂ i 0 = 0h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0g: Dfinsupp fun i => β imapRange (fun i => f i ∘ f₂ i) h g = mapRange f hf (mapRange f₂ hf₂ g)simp only [mapRange_apply: ∀ {ι : Type ?u.18397} {β₁ : ι → Type ?u.18396} {β₂ : ι → Type ?u.18395} [inst : (i : ι) → Zero (β₁ i)]
[inst_1 : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Dfinsupp fun i => β₁ i)
(i : ι), ↑(mapRange f hf g) i = f i (↑g i)mapRange_apply]ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ if₂: (i : ι) → β i → β₁ ihf: ∀ (i : ι), f i 0 = 0hf₂: ∀ (i : ι), f₂ i 0 = 0h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0g: Dfinsupp fun i => β ii✝: ιh(f i✝ ∘ f₂ i✝) (↑g i✝) = f i✝ (f₂ i✝ (↑g i✝));ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ if₂: (i : ι) → β i → β₁ ihf: ∀ (i : ι), f i 0 = 0hf₂: ∀ (i : ι), f₂ i 0 = 0h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0g: Dfinsupp fun i => β ii✝: ιh(f i✝ ∘ f₂ i✝) (↑g i✝) = f i✝ (f₂ i✝ (↑g i✝)) ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ if₂: (i : ι) → β i → β₁ ihf: ∀ (i : ι), f i 0 = 0hf₂: ∀ (i : ι), f₂ i 0 = 0h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0g: Dfinsupp fun i => β imapRange (fun i => f i ∘ f₂ i) h g = mapRange f hf (mapRange f₂ hf₂ g)rflGoals accomplished! 🐙
#align dfinsupp.map_range_comp Dfinsupp.mapRange_comp: ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β i)]
[inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i)
(f₂ : (i : ι) → β i → β₁ i) (hf : ∀ (i : ι), f i 0 = 0) (hf₂ : ∀ (i : ι), f₂ i 0 = 0)
(h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0) (g : Dfinsupp fun i => β i),
mapRange (fun i => f i ∘ f₂ i) h g = mapRange f hf (mapRange f₂ hf₂ g)Dfinsupp.mapRange_comp

@[simp]
theorem mapRange_zero: ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
(f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0), mapRange f hf 0 = 0mapRange_zero (f: (i : ι) → β₁ i → β₂ if : ∀ i: ?m.19146i, β₁: ι → Type v₁β₁ i: ?m.19146i → β₂: ι → Type v₂β₂ i: ?m.19146i) (hf: ∀ (i : ι), f i 0 = 0hf : ∀ i: ?m.19154i, f: (i : ι) → β₁ i → β₂ if i: ?m.19154i 0: ?m.191590 = 0: ?m.191920) :
mapRange: {ι : Type ?u.19242} →
{β₁ : ι → Type ?u.19241} →
{β₂ : ι → Type ?u.19240} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange f: (i : ι) → β₁ i → β₂ if hf: ∀ (i : ι), f i 0 = 0hf (0: ?m.193740 : Π₀ i: ?m.19338i, β₁: ι → Type v₁β₁ i: ?m.19338i) = 0: ?m.194390 := byGoals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ ihf: ∀ (i : ι), f i 0 = 0mapRange f hf 0 = 0extι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ ihf: ∀ (i : ι), f i 0 = 0i✝: ιh↑(mapRange f hf 0) i✝ = ↑0 i✝
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ ihf: ∀ (i : ι), f i 0 = 0mapRange f hf 0 = 0simp only [mapRange_apply: ∀ {ι : Type ?u.19575} {β₁ : ι → Type ?u.19574} {β₂ : ι → Type ?u.19573} [inst : (i : ι) → Zero (β₁ i)]
[inst_1 : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Dfinsupp fun i => β₁ i)
(i : ι), ↑(mapRange f hf g) i = f i (↑g i)mapRange_apply, coe_zero: ∀ {ι : Type ?u.19624} {β : ι → Type ?u.19623} [inst : (i : ι) → Zero (β i)], ↑0 = 0coe_zero, Pi.zero_apply: ∀ {I : Type ?u.19648} {f : I → Type ?u.19647} (i : I) [inst : (i : I) → Zero (f i)], OfNat.ofNat 0 i = 0Pi.zero_apply, hf: ∀ (i : ι), f i 0 = 0hf]Goals accomplished! 🐙
#align dfinsupp.map_range_zero Dfinsupp.mapRange_zero: ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
(f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0), mapRange f hf 0 = 0Dfinsupp.mapRange_zero

/-- Let `f i` be a binary operation `β₁ i → β₂ i → β i` such that `f i 0 0 = 0`.
Then `zipWith f hf` is a binary operation `Π₀ i, β₁ i → Π₀ i, β₂ i → Π₀ i, β i`. -/
def zipWith: {ι : Type u} →
{β : ι → Type v} →
{β₁ : ι → Type v₁} →
{β₂ : ι → Type v₂} →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → Zero (β₁ i)] →
[inst_2 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i → β i) →
(∀ (i : ι), f i 0 0 = 0) → (Dfinsupp fun i => β₁ i) → (Dfinsupp fun i => β₂ i) → Dfinsupp fun i => β izipWith (f: (i : ι) → β₁ i → β₂ i → β if : ∀ i: ?m.20230i, β₁: ι → Type v₁β₁ i: ?m.20230i → β₂: ι → Type v₂β₂ i: ?m.20230i → β: ι → Type vβ i: ?m.20230i) (hf: ∀ (i : ι), f i 0 0 = 0hf : ∀ i: ?m.20240i, f: (i : ι) → β₁ i → β₂ i → β if i: ?m.20240i 0: ?m.202450 0: ?m.202780 = 0: ?m.203100) (x: Dfinsupp fun i => β₁ ix : Π₀ i: ?m.20363i, β₁: ι → Type v₁β₁ i: ?m.20363i) (y: Dfinsupp fun i => β₂ iy : Π₀ i: ?m.20406i, β₂: ι → Type v₂β₂ i: ?m.20406i) :
Π₀ i: ?m.20446i, β: ι → Type vβ i: ?m.20446i :=
⟨fun i: ?m.20564i => f: (i : ι) → β₁ i → β₂ i → β if i: ?m.20564i (x: Dfinsupp fun i => β₁ ix i: ?m.20564i) (y: Dfinsupp fun i => β₂ iy i: ?m.20564i), byGoals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }refine' x: Dfinsupp fun i => β₁ ix.support': {ι : Type ?u.20696} →
{β : ι → Type ?u.20695} →
[inst : (i : ι) → Zero (β i)] → (self : Dfinsupp β) → Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun self i = 0 }support'.bind: {α : Sort ?u.20733} → {β : Sort ?u.20732} → Trunc α → (α → Trunc β) → Trunc βbind fun xs: ?m.20743xs => _: Trunc ?m.20740_ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }Trunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }refine' y: Dfinsupp fun i => β₂ iy.support': {ι : Type ?u.20750} →
{β : ι → Type ?u.20749} →
[inst : (i : ι) → Zero (β i)] → (self : Dfinsupp β) → Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun self i = 0 }support'.map: {α : Sort ?u.20785} → {β : Sort ?u.20784} → (α → β) → Trunc α → Trunc βmap fun ys: ?m.20793ys => _: ?m.20791_ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }{ s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }refine' ⟨xs: ?m.20743xs + ys: ?m.20793ys, fun i: ?m.21388i => _: i ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0_⟩ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιi ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }obtain h1: i ∈ ↑xsh1h1 | (h1 : x i = 0): i ∈ ↑xs ∨ toFun x i = 0 | (h1: ↑x i = 0h1h1 : x i = 0: toFun x i = 0 : x: Dfinsupp fun i => β₁ ixh1 : x i = 0: toFun x i = 0 i: ?m.21388ih1 : x i = 0: toFun x i = 0 = 0: ?m.215240h1 | (h1 : x i = 0): i ∈ ↑xs ∨ toFun x i = 0) := xs: ?m.20743xs.prop: ∀ {α : Sort ?u.21396} {p : α → Prop} (x : Subtype p), p ↑xprop i: ?m.21388iι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0inri ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }·ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0 ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0inri ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0leftι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinl.hi ∈ ↑xs + ↑ys
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0rw [ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinl.hi ∈ ↑xs + ↑ysMultiset.mem_add: ∀ {α : Type ?u.21574} {a : α} {s t : Multiset α}, a ∈ s + t ↔ a ∈ s ∨ a ∈ tMultiset.mem_addι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinl.hi ∈ ↑xs ∨ i ∈ ↑ys]ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinl.hi ∈ ↑xs ∨ i ∈ ↑ys
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0leftι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinl.h.hi ∈ ↑xs
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: i ∈ ↑xsinli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0exact h1: i ∈ ↑xsh1Goals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }obtain h2: i ∈ ↑ysh2h2 | (h2 : y i = 0): i ∈ ↑ys ∨ toFun y i = 0 | (h2: ↑y i = 0h2h2 : y i = 0: toFun y i = 0 : y: Dfinsupp fun i => β₂ iyh2 : y i = 0: toFun y i = 0 i: ?m.21388ih2 : y i = 0: toFun y i = 0 = 0: ?m.217090h2 | (h2 : y i = 0): i ∈ ↑ys ∨ toFun y i = 0) := ys: ?m.20793ys.prop: ∀ {α : Sort ?u.21613} {p : α → Prop} (x : Subtype p), p ↑xprop i: ?m.21388iι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inri ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }·ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0 ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inri ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0leftι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inl.hi ∈ ↑xs + ↑ys
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0rw [ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inl.hi ∈ ↑xs + ↑ysMultiset.mem_add: ∀ {α : Type ?u.21758} {a : α} {s t : Multiset α}, a ∈ s + t ↔ a ∈ s ∨ a ∈ tMultiset.mem_addι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inl.hi ∈ ↑xs ∨ i ∈ ↑ys]ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inl.hi ∈ ↑xs ∨ i ∈ ↑ys
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0rightι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inl.h.hi ∈ ↑ys
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: i ∈ ↑ysinr.inli ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0exact h2: i ∈ ↑ysh2Goals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }rightι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inr.h(fun i => f i (↑x i) (↑y i)) i = 0;ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inr.h(fun i => f i (↑x i) (↑y i)) i = 0 ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ iTrunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }rw [ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inr.h(fun i => f i (↑x i) (↑y i)) i = 0← hf: ∀ (i : ι), f i 0 0 = 0hf,ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inr.h(fun i => f i (↑x i) (↑y i)) i = f i 0 0 ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inr.h(fun i => f i (↑x i) (↑y i)) i = 0← h1: ↑x i = 0h1,ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inr.h(fun i => f i (↑x i) (↑y i)) i = f i (↑x i) 0 ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inr.h(fun i => f i (↑x i) (↑y i)) i = 0← h2: ↑y i = 0h2ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝²: (i : ι) → Zero (β i)inst✝¹: (i : ι) → Zero (β₁ i)inst✝: (i : ι) → Zero (β₂ i)f: (i : ι) → β₁ i → β₂ i → β ihf: ∀ (i : ι), f i 0 0 = 0x: Dfinsupp fun i => β₁ iy: Dfinsupp fun i => β₂ ixs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }i: ιh1: ↑x i = 0h2: ↑y i = 0inr.inr.h(fun i => f i (↑x i) (↑y i)) i = f i (↑x i) (↑y i)]Goals accomplished! 🐙⟩
#align dfinsupp.zip_with Dfinsupp.zipWith: {ι : Type u} →
{β : ι → Type v} →
{β₁ : ι → Type v₁} →
{β₂ : ι → Type v₂} →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → Zero (β₁ i)] →
[inst_2 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i → β i) →
(∀ (i : ι), f i 0 0 = 0) → (Dfinsupp fun i => β₁ i) → (Dfinsupp fun i => β₂ i) → Dfinsupp fun i => β iDfinsupp.zipWith

@[simp]
theorem zipWith_apply: ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β i)]
[inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i → β i)
(hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Dfinsupp fun i => β₁ i) (g₂ : Dfinsupp fun i => β₂ i) (i : ι),
↑(zipWith f hf g₁ g₂) i = f i (↑g₁ i) (↑g₂ i)zipWith_apply (f: (i : ι) → β₁ i → β₂ i → β if : ∀ i: ?m.22294i, β₁: ι → Type v₁β₁ i: ?m.22294i → β₂: ι → Type v₂β₂ i: ?m.22294i → β: ι → Type vβ i: ?m.22294i) (hf: ∀ (i : ι), f i 0 0 = 0hf : ∀ i: ?m.22304i, f: (i : ι) → β₁ i → β₂ i → β if i: ?m.22304i 0: ?m.223090 0: ?m.223420 = 0: ?m.223740) (g₁: Dfinsupp fun i => β₁ ig₁ : Π₀ i: ?m.22427i, β₁: ι → Type v₁β₁ i: ?m.22427i)
(g₂: Dfinsupp fun i => β₂ ig₂ : Π₀ i: ?m.22470i, β₂: ι → Type v₂β₂ i: ?m.22470i) (i: ιi : ι: Type uι) : zipWith: {ι : Type ?u.22512} →
{β : ι → Type ?u.22511} →
{β₁ : ι → Type ?u.22510} →
{β₂ : ι → Type ?u.22509} →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → Zero (β₁ i)] →
[inst_2 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i → β i) →
(∀ (i : ι), f i 0 0 = 0) → (Dfinsupp fun i => β₁ i) → (Dfinsupp fun i => β₂ i) → Dfinsupp fun i => β izipWith f: (i : ι) → β₁ i → β₂ i → β if hf: ∀ (i : ι), f i 0 0 = 0hf g₁: Dfinsupp fun i => β₁ ig₁ g₂: Dfinsupp fun i => β₂ ig₂ i: ιi = f: (i : ι) → β₁ i → β₂ i → β if i: ιi (g₁: Dfinsupp fun i => β₁ ig₁ i: ιi) (g₂: Dfinsupp fun i => β₂ ig₂ i: ιi) :=
rfl: ∀ {α : Sort ?u.22817} {a : α}, a = arfl
#align dfinsupp.zip_with_apply Dfinsupp.zipWith_apply: ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β i)]
[inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i → β i)
(hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Dfinsupp fun i => β₁ i) (g₂ : Dfinsupp fun i => β₂ i) (i : ι),
↑(zipWith f hf g₁ g₂) i = f i (↑g₁ i) (↑g₂ i)Dfinsupp.zipWith_apply

section Piecewise

variable (x: Dfinsupp fun i => β ix y: Dfinsupp fun i => β iy : Π₀ i: ?m.23806i, β: ι → Type vβ i: ?m.22957i) (s: Set ιs : Set: Type ?u.24396 → Type ?u.24396Set ι: Type uι) [∀ i: ?m.23153i, Decidable: Prop → TypeDecidable (i: ?m.23020i ∈ s: Set ιs)]

/-- `x.piecewise y s` is the finitely supported function equal to `x` on the set `s`,
and to `y` on its complement. -/
def piecewise: Dfinsupp fun i => β ipiecewise : Π₀ i: ?m.23183i, β: ι → Type vβ i: ?m.23183i :=
zipWith: {ι : Type ?u.23229} →
{β : ι → Type ?u.23228} →
{β₁ : ι → Type ?u.23227} →
{β₂ : ι → Type ?u.23226} →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → Zero (β₁ i)] →
[inst_2 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i → β i) →
(∀ (i : ι), f i 0 0 = 0) → (Dfinsupp fun i => β₁ i) → (Dfinsupp fun i => β₂ i) → Dfinsupp fun i => β izipWith (fun i: ?m.23416i x: ?m.23419x y: ?m.23422y => if i: ?m.23416i ∈ s: Set ιs then x: ?m.23419x else y: ?m.23422y) (fun _: ?m.23465_ => ite_self: ∀ {α : Sort ?u.23467} {c : Prop} {d : Decidable c} (a : α), (if c then a else a) = aite_self 0: ?m.234720) x: Dfinsupp fun i => β ix y: Dfinsupp fun i => β iy
#align dfinsupp.piecewise Dfinsupp.piecewise: {ι : Type u} →
{β : ι → Type v} →
[inst : (i : ι) → Zero (β i)] →
(Dfinsupp fun i => β i) →
(Dfinsupp fun i => β i) → (s : Set ι) → [inst_1 : (i : ι) → Decidable (i ∈ s)] → Dfinsupp fun i => β iDfinsupp.piecewise

theorem piecewise_apply: ∀ (i : ι), ↑(piecewise x y s) i = if i ∈ s then ↑x i else ↑y ipiecewise_apply (i: ιi : ι: Type uι) : x: Dfinsupp fun i => β ix.piecewise: {ι : Type ?u.23851} →
{β : ι → Type ?u.23850} →
[inst : (i : ι) → Zero (β i)] →
(Dfinsupp fun i => β i) →
(Dfinsupp fun i => β i) → (s : Set ι) → [inst_1 : (i : ι) → Decidable (i ∈ s)] → Dfinsupp fun i => β ipiecewise y: Dfinsupp fun i => β iy s: Set ιs i: ιi = if i: ιi ∈ s: Set ιs then x: Dfinsupp fun i => β ix i: ιi else y: Dfinsupp fun i => β iy i: ιi :=
zipWith_apply: ∀ {ι : Type ?u.24084} {β : ι → Type ?u.24083} {β₁ : ι → Type ?u.24082} {β₂ : ι → Type ?u.24081}
[inst : (i : ι) → Zero (β i)] [inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)]
(f : (i : ι) → β₁ i → β₂ i → β i) (hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Dfinsupp fun i => β₁ i)
(g₂ : Dfinsupp fun i => β₂ i) (i : ι), ↑(zipWith f hf g₁ g₂) i = f i (↑g₁ i) (↑g₂ i)zipWith_apply _: (i : ?m.24085) → ?m.24087 i → ?m.24088 i → ?m.24086 i_ _: ∀ (i : ?m.24085), ?m.24092 i 0 0 = 0_ x: Dfinsupp fun i => β ix y: Dfinsupp fun i => β iy i: ιi
#align dfinsupp.piecewise_apply Dfinsupp.piecewise_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (x y : Dfinsupp fun i => β i) (s : Set ι)
[inst_1 : (i : ι) → Decidable (i ∈ s)] (i : ι), ↑(piecewise x y s) i = if i ∈ s then ↑x i else ↑y iDfinsupp.piecewise_apply

@[simp, norm_cast]
theorem coe_piecewise: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (x y : Dfinsupp fun i => β i) (s : Set ι)
[inst_1 : (i : ι) → Decidable (i ∈ s)], ↑(piecewise x y s) = Set.piecewise s ↑x ↑ycoe_piecewise : ⇑(x: Dfinsupp fun i => β ix.piecewise: {ι : Type ?u.24428} →
{β : ι → Type ?u.24427} →
[inst : (i : ι) → Zero (β i)] →
(Dfinsupp fun i => β i) →
(Dfinsupp fun i => β i) → (s : Set ι) → [inst_1 : (i : ι) → Decidable (i ∈ s)] → Dfinsupp fun i => β ipiecewise y: Dfinsupp fun i => β iy s: Set ιs) = s: Set ιs.piecewise: {α : Type ?u.24559} →
{β : α → Sort ?u.24558} →
(s : Set α) → ((i : α) → β i) → ((i : α) → β i) → [inst : (j : α) → Decidable (j ∈ s)] → (i : α) → β ipiecewise x: Dfinsupp fun i => β ix y: Dfinsupp fun i => β iy := byGoals accomplished! 🐙
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝³: (i : ι) → Zero (β i)inst✝²: (i : ι) → Zero (β₁ i)inst✝¹: (i : ι) → Zero (β₂ i)x, y: Dfinsupp fun i => β is: Set ιinst✝: (i : ι) → Decidable (i ∈ s)↑(piecewise x y s) = Set.piecewise s ↑x ↑yextι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝³: (i : ι) → Zero (β i)inst✝²: (i : ι) → Zero (β₁ i)inst✝¹: (i : ι) → Zero (β₂ i)x, y: Dfinsupp fun i => β is: Set ιinst✝: (i : ι) → Decidable (i ∈ s)x✝: ιh↑(piecewise x y s) x✝ = Set.piecewise s (↑x) (↑y) x✝
ι: Type uγ: Type wβ: ι → Type vβ₁: ι → Type v₁β₂: ι → Type v₂inst✝³: (i : ι) → Zero (β i)inst✝²: (i : ι) → Zero (β₁ i)inst✝¹: (i : ι) → Zero (β₂ i)x, y: Dfinsupp fun i => β is: Set ιinst✝: (i : ι) → Decidable (i ∈ s)↑(piecewise x y s) = Set.piecewise s ↑x ↑yapply piecewise_apply: ∀ {ι : Type ?u.24698} {β : ι → Type ?u.24697} [inst : (i : ι) → Zero (β i)] (x y : Dfinsupp fun i => β i) (s : Set ι)
[inst_1 : (i : ι) → Decidable (i ∈ s)] (i : ι), ↑(piecewise x y s) i = if i ∈ s then ↑x i else ↑y ipiecewise_applyGoals accomplished! 🐙
#align dfinsupp.coe_piecewise Dfinsupp.coe_piecewise: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (x y : Dfinsupp fun i => β i) (s : Set ι)
[inst_1 : (i : ι) → Decidable (i ∈ s)], ↑(piecewise x y s) = Set.piecewise s ↑x ↑yDfinsupp.coe_piecewise

end Piecewise

end Basic

section Algebra

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → Add (Dfinsupp fun i => β i)instance [∀ i: ?m.25073i, AddZeroClass: Type ?u.25076 → Type ?u.25076AddZeroClass (β: ι → Type vβ i: ?m.25073i)] : Add: Type ?u.25080 → Type ?u.25080Add (Π₀ i: ?m.25085i, β: ι → Type vβ i: ?m.25085i) :=
⟨zipWith: {ι : Type ?u.26473} →
{β : ι → Type ?u.26472} →
{β₁ : ι → Type ?u.26471} →
{β₂ : ι → Type ?u.26470} →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → Zero (β₁ i)] →
[inst_2 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i → β i) →
(∀ (i : ι), f i 0 0 = 0) → (Dfinsupp fun i => β₁ i) → (Dfinsupp fun i => β₂ i) → Dfinsupp fun i => β izipWith (fun _: ?m.26666_ => (· + ·): β x✝ → β x✝ → β x✝(· + ·)) fun _: ?m.27131_ => add_zero: ∀ {M : Type ?u.27133} [inst : AddZeroClass M] (a : M), a + 0 = aadd_zero 0: ?m.271370⟩

theorem add_apply: ∀ [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i) (i : ι), ↑(g₁ + g₂) i = ↑g₁ i + ↑g₂ iadd_apply [∀ i: ?m.29153i, AddZeroClass: Type ?u.29156 → Type ?u.29156AddZeroClass (β: ι → Type vβ i: ?m.29153i)] (g₁: Dfinsupp fun i => β ig₁ g₂: Dfinsupp fun i => β ig₂ : Π₀ i: ?m.30547i, β: ι → Type vβ i: ?m.30547i) (i: ιi : ι: Type uι) :
(g₁: Dfinsupp fun i => β ig₁ + g₂: Dfinsupp fun i => β ig₂) i: ιi = g₁: Dfinsupp fun i => β ig₁ i: ιi + g₂: Dfinsupp fun i => β ig₂ i: ιi :=
rfl: ∀ {α : Sort ?u.31221} {a : α}, a = arfl
#align dfinsupp.add_apply Dfinsupp.add_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i) (i : ι),
↑(g₁ + g₂) i = ↑g₁ i + ↑g₂ iDfinsupp.add_apply

@[simp]
theorem coe_add: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i),
↑(g₁ + g₂) = ↑g₁ + ↑g₂coe_add [∀ i: ?m.31264i, AddZeroClass: Type ?u.31267 → Type ?u.31267AddZeroClass (β: ι → Type vβ i: ?m.31264i)] (g₁: Dfinsupp fun i => β ig₁ g₂: Dfinsupp fun i => β ig₂ : Π₀ i: ?m.32658i, β: ι → Type vβ i: ?m.31275i) : ⇑(g₁: Dfinsupp fun i => β ig₁ + g₂: Dfinsupp fun i => β ig₂) = g₁: Dfinsupp fun i => β ig₁ + g₂: Dfinsupp fun i => β ig₂ :=
rfl: ∀ {α : Sort ?u.34291} {a : α}, a = arfl
#align dfinsupp.coe_add Dfinsupp.coe_add: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i),
↑(g₁ + g₂) = ↑g₁ + ↑g₂Dfinsupp.coe_add

instance addZeroClass: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → AddZeroClass (Dfinsupp fun i => β i)addZeroClass [∀ i: ?m.34368i, AddZeroClass: Type ?u.34371 → Type ?u.34371AddZeroClass (β: ι → Type vβ i: ?m.34368i)] : AddZeroClass: Type ?u.34375 → Type ?u.34375AddZeroClass (Π₀ i: ?m.34380i, β: ι → Type vβ i: ?m.34380i) :=
FunLike.coe_injective: ∀ {F : Sort ?u.35760} {α : Sort ?u.35761} {β : α → Sort ?u.35762} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.addZeroClass: {M₁ : Type ?u.35835} →
{M₂ : Type ?u.35834} →
[inst_1 : Zero M₁] →
(f : M₁ → M₂) → Function.Injective f → f 0 = 0 → (∀ (x y : M₁), f (x + y) = f x + f y) → AddZeroClass M₁addZeroClass _: ?m.35845 → ?m.35846_ coe_zero: ∀ {ι : Type ?u.35980} {β : ι → Type ?u.35979} [inst : (i : ι) → Zero (β i)], ↑0 = 0coe_zero coe_add: ∀ {ι : Type ?u.37351} {β : ι → Type ?u.37350} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i),
↑(g₁ + g₂) = ↑g₁ + ↑g₂coe_add

/-- Note the general `SMul` instance doesn't apply as `ℕ` is not distributive
unless `β i`'s addition is commutative. -/
instance hasNatScalar: [inst : (i : ι) → AddMonoid (β i)] → SMul ℕ (Dfinsupp fun i => β i)hasNatScalar [∀ i: ?m.37744i, AddMonoid: Type ?u.37747 → Type ?u.37747AddMonoid (β: ι → Type vβ i: ?m.37744i)] : SMul: Type ?u.37752 → Type ?u.37751 → Type (max?u.37752?u.37751)SMul ℕ: Typeℕ (Π₀ i: ?m.37757i, β: ι → Type vβ i: ?m.37757i) :=
⟨fun c: ?m.38898c v: ?m.38901v => v: ?m.38901v.mapRange: {ι : Type ?u.38905} →
{β₁ : ι → Type ?u.38904} →
{β₂ : ι → Type ?u.38903} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange (fun _: ?m.39038_ => (· • ·): ℕ → β x✝ → β x✝(· • ·) c: ?m.38898c) fun _: ?m.39258_ => nsmul_zero: ∀ {A : Type ?u.39260} [inst : AddMonoid A] (n : ℕ), n • 0 = 0nsmul_zero _: ℕ_⟩
#align dfinsupp.has_nat_scalar Dfinsupp.hasNatScalar: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddMonoid (β i)] → SMul ℕ (Dfinsupp fun i => β i)Dfinsupp.hasNatScalar

theorem nsmul_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Dfinsupp fun i => β i) (i : ι),
↑(b • v) i = b • ↑v insmul_apply [∀ i: ?m.40766i, AddMonoid: Type ?u.40769 → Type ?u.40769AddMonoid (β: ι → Type vβ i: ?m.40766i)] (b: ℕb : ℕ: Typeℕ) (v: Dfinsupp fun i => β iv : Π₀ i: ?m.40779i, β: ι → Type vβ i: ?m.40779i) (i: ιi : ι: Type uι) : (b: ℕb • v: Dfinsupp fun i => β iv) i: ιi = b: ℕb • v: Dfinsupp fun i => β iv i: ιi :=
rfl: ∀ {α : Sort ?u.42118} {a : α}, a = arfl
#align dfinsupp.nsmul_apply Dfinsupp.nsmul_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Dfinsupp fun i => β i) (i : ι),
↑(b • v) i = b • ↑v iDfinsupp.nsmul_apply

@[simp]
theorem coe_nsmul: ∀ [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Dfinsupp fun i => β i), ↑(b • v) = b • ↑vcoe_nsmul [∀ i: ?m.42162i, AddMonoid: Type ?u.42165 → Type ?u.42165AddMonoid (β: ι → Type vβ i: ?m.42162i)] (b: ℕb : ℕ: Typeℕ) (v: Dfinsupp fun i => β iv : Π₀ i: ?m.42175i, β: ι → Type vβ i: ?m.42175i) : ⇑(b: ℕb • v: Dfinsupp fun i => β iv) = b: ℕb • ⇑v: Dfinsupp fun i => β iv :=
rfl: ∀ {α : Sort ?u.43537} {a : α}, a = arfl
#align dfinsupp.coe_nsmul Dfinsupp.coe_nsmul: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Dfinsupp fun i => β i),
↑(b • v) = b • ↑vDfinsupp.coe_nsmul

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddMonoid (β i)] → AddMonoid (Dfinsupp fun i => β i)instance [∀ i: ?m.43615i, AddMonoid: Type ?u.43618 → Type ?u.43618AddMonoid (β: ι → Type vβ i: ?m.43615i)] : AddMonoid: Type ?u.43622 → Type ?u.43622AddMonoid (Π₀ i: ?m.43627i, β: ι → Type vβ i: ?m.43627i) :=
FunLike.coe_injective: ∀ {F : Sort ?u.44758} {α : Sort ?u.44759} {β : α → Sort ?u.44760} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.addMonoid: {M₁ : Type ?u.44833} →
{M₂ : Type ?u.44832} →
[inst_1 : Zero M₁] →
[inst_2 : SMul ℕ M₁] →
(f : M₁ → M₂) →
Function.Injective f →
f 0 = 0 →
(∀ (x y : M₁), f (x + y) = f x + f y) → (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddMonoid M₁addMonoid _: ?m.44845 → ?m.44846_ coe_zero: ∀ {ι : Type ?u.45027} {β : ι → Type ?u.45026} [inst : (i : ι) → Zero (β i)], ↑0 = 0coe_zero coe_add: ∀ {ι : Type ?u.46174} {β : ι → Type ?u.46173} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i),
↑(g₁ + g₂) = ↑g₁ + ↑g₂coe_add fun _: ?m.46282_ _: ?m.46285_ => coe_nsmul: ∀ {ι : Type ?u.46288} {β : ι → Type ?u.46287} [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Dfinsupp fun i => β i),
↑(b • v) = b • ↑vcoe_nsmul _: ℕ_ _: Dfinsupp fun i => ?m.46290 i_

/-- Coercion from a `Dfinsupp` to a pi type is an `AddMonoidHom`. -/
def coeFnAddMonoidHom: [inst : (i : ι) → AddZeroClass (β i)] → (Dfinsupp fun i => β i) →+ (i : ι) → β icoeFnAddMonoidHom [∀ i: ?m.46729i, AddZeroClass: Type ?u.46732 → Type ?u.46732AddZeroClass (β: ι → Type vβ i: ?m.46729i)] : (Π₀ i: ?m.46742i, β: ι → Type vβ i: ?m.46742i) →+ ∀ i: ?m.48120i, β: ι → Type vβ i: ?m.48120i
where
toFun := (⇑): (Dfinsupp fun i => (fun i => β i) i) → (a : ι) → (fun i => (fun i => β i) i) a(⇑)
map_zero' := coe_zero: ∀ {ι : Type ?u.49635} {β : ι → Type ?u.49634} [inst : (i : ι) → Zero (β i)], ↑0 = 0coe_zero
map_add' := coe_add: ∀ {ι : Type ?u.50968} {β : ι → Type ?u.50967} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i),
↑(g₁ + g₂) = ↑g₁ + ↑g₂coe_add
#align dfinsupp.coe_fn_add_monoid_hom Dfinsupp.coeFnAddMonoidHom: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → (Dfinsupp fun i => β i) →+ (i : ι) → β iDfinsupp.coeFnAddMonoidHom

/-- Evaluation at a point is an `AddMonoidHom`. This is the finitely-supported version of
def evalAddMonoidHom: [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → (Dfinsupp fun i => β i) →+ β ievalAddMonoidHom [∀ i: ?m.51185i, AddZeroClass: Type ?u.51188 → Type ?u.51188AddZeroClass (β: ι → Type vβ i: ?m.51185i)] (i: ιi : ι: Type uι) : (Π₀ i: ?m.51200i, β: ι → Type vβ i: ?m.51200i) →+ β: ι → Type vβ i: ιi :=
(Pi.evalAddMonoidHom: {I : Type ?u.52626} → (f : I → Type ?u.52625) → [inst : (i : I) → AddZeroClass (f i)] → (i : I) → ((i : I) → f i) →+ f iPi.evalAddMonoidHom β: ι → Type vβ i: ιi).comp: {M : Type ?u.52645} →
{N : Type ?u.52644} →
{P : Type ?u.52643} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ Pcomp coeFnAddMonoidHom: {ι : Type ?u.52719} →
{β : ι → Type ?u.52718} → [inst : (i : ι) → AddZeroClass (β i)] → (Dfinsupp fun i => β i) →+ (i : ι) → β icoeFnAddMonoidHom
#align dfinsupp.eval_add_monoid_hom Dfinsupp.evalAddMonoidHom: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → (Dfinsupp fun i => β i) →+ β iDfinsupp.evalAddMonoidHom

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddCommMonoid (β i)] → AddCommMonoid (Dfinsupp fun i => β i)instance [∀ i: ?m.52895i, AddCommMonoid: Type ?u.52898 → Type ?u.52898AddCommMonoid (β: ι → Type vβ i: ?m.52895i)] : AddCommMonoid: Type ?u.52902 → Type ?u.52902AddCommMonoid (Π₀ i: ?m.52907i, β: ι → Type vβ i: ?m.52907i) :=
FunLike.coe_injective: ∀ {F : Sort ?u.54147} {α : Sort ?u.54148} {β : α → Sort ?u.54149} [i : FunLike F α β], Function.Injective fun f => ↑fFunLike.coe_injective.addCommMonoid: {M₁ : Type ?u.54222} →
{M₂ : Type ?u.54221} →
[inst_1 : Zero M₁] →
[inst_2 : SMul ℕ M₁] →
(f : M₁ → M₂) →
Function.Injective f →
f 0 = 0 →
(∀ (x y : M₁), f (x + y) = f x + f y) → (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddCommMonoid M₁addCommMonoid _: ?m.54234 → ?m.54235_ coe_zero: ∀ {ι : Type ?u.54429} {β : ι → Type ?u.54428} [inst : (i : ι) → Zero (β i)], ↑0 = 0coe_zero coe_add: ∀ {ι : Type ?u.55684} {β : ι → Type ?u.55683} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i),
↑(g₁ + g₂) = ↑g₁ + ↑g₂coe_add fun _: ?m.56549_ _: ?m.56552_ => coe_nsmul: ∀ {ι : Type ?u.56555} {β : ι → Type ?u.56554} [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Dfinsupp fun i => β i),
↑(b • v) = b • ↑vcoe_nsmul _: ℕ_ _: Dfinsupp fun i => ?m.56557 i_

@[simp]
theorem coe_finset_sum: ∀ {ι : Type u} {β : ι → Type v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset α)
(g : α → Dfinsupp fun i => β i), ↑(∑ a in s, g a) = ∑ a in s, ↑(g a)coe_finset_sum {α: Type u_1α} [∀ i: ?m.57978i, AddCommMonoid: Type ?u.57981 → Type ?u.57981AddCommMonoid (β: ι → Type vβ i: ?m.57978i)] (s: Finset αs : Finset: Type ?u.57985 → Type ?u.57985Finset α: ?m.57974α) (g: α → Dfinsupp fun i => β ig : α: ?m.57974α → Π₀ i: ?m.57994i, β: ι → Type vβ i: ?m.57994i) :
⇑(∑ a: ?m.59242a in s: Finset αs, g: α → Dfinsupp fun i => β ig a: ?m.59242a) = ∑ a: ?m.59353a in s: Finset αs, ⇑g: α → Dfinsupp fun i => β ig a: ?m.59353a :=
(coeFnAddMonoidHom: {ι : Type ?u.60314} →
{β : ι → Type ?u.60313} → [inst : (i : ι) → AddZeroClass (β i)] → (Dfinsupp fun i => β i) →+ (i : ι) → β icoeFnAddMonoidHom : _: Type ?u.59443_ →+ ∀ i: ?m.59446i, β: ι → Type vβ i: ?m.59446i).map_sum: ∀ {β : Type ?u.61144} {α : Type ?u.61143} {γ : Type ?u.61142} [inst : AddCommMonoid β] [inst_1 : AddCommMonoid γ]
(g : β →+ γ) (f : α → β) (s : Finset α), ↑g (∑ x in s, f x) = ∑ x in s, ↑g (f x)map_sum g: α → Dfinsupp fun i => β ig s: Finset αs
#align dfinsupp.coe_finset_sum Dfinsupp.coe_finset_sum: ∀ {ι : Type u} {β : ι → Type v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset α)
(g : α → Dfinsupp fun i => β i), ↑(∑ a in s, g a) = ∑ a in s, ↑(g a)Dfinsupp.coe_finset_sum

@[simp]
theorem finset_sum_apply: ∀ {ι : Type u} {β : ι → Type v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset α)
(g : α → Dfinsupp fun i => β i) (i : ι), ↑(∑ a in s, g a) i = ∑ a in s, ↑(g a) ifinset_sum_apply {α: ?m.61441α} [∀ i: ?m.61445i, AddCommMonoid: Type ?u.61448 → Type ?u.61448AddCommMonoid (β: ι → Type vβ i: ?m.61445i)] (s: Finset αs : Finset: Type ?u.61452 → Type ?u.61452Finset α: ?m.61441α) (g: α → Dfinsupp fun i => β ig : α: ?m.61441α → Π₀ i: ?m.61461i, β: ι → Type vβ i: ?m.61461i) (i: ιi : ι: Type uι) :
(∑ a: ?m.62711a in s: Finset αs, g: α → Dfinsupp fun i => β ig a: ?m.62711a) i: ιi = ∑ a: ?m.62822a in s: Finset αs, g: α → Dfinsupp fun i => β ig a: ?m.62822a i: ιi :=
(evalAddMonoidHom: {ι : Type ?u.63270} →
{β : ι → Type ?u.63269} → [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → (Dfinsupp fun i => β i) →+ β ievalAddMonoidHom i: ιi : _: Type ?u.62880_ →+ β: ι → Type vβ i: ιi).map_sum: ∀ {β : Type ?u.64096} {α : Type ?u.64095} {γ : Type ?u.64094} [inst : AddCommMonoid β] [inst_1 : AddCommMonoid γ]
(g : β →+ γ) (f : α → β) (s : Finset α), ↑g (∑ x in s, f x) = ∑ x in s, ↑g (f x)map_sum g: α → Dfinsupp fun i => β ig s: Finset αs
#align dfinsupp.finset_sum_apply Dfinsupp.finset_sum_apply: ∀ {ι : Type u} {β : ι → Type v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset α)
(g : α → Dfinsupp fun i => β i) (i : ι), ↑(∑ a in s, g a) i = ∑ a in s, ↑(g a) iDfinsupp.finset_sum_apply

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddGroup (β i)] → Neg (Dfinsupp fun i => β i)instance [∀ i: ?m.64351i, AddGroup: Type ?u.64354 → Type ?u.64354AddGroup (β: ι → Type vβ i: ?m.64351i)] : Neg: Type ?u.64358 → Type ?u.64358Neg (Π₀ i: ?m.64363i, β: ι → Type vβ i: ?m.64363i) :=
⟨fun f: ?m.65345f => f: ?m.65345f.mapRange: {ι : Type ?u.65349} →
{β₁ : ι → Type ?u.65348} →
{β₂ : ι → Type ?u.65347} →
[inst : (i : ι) → Zero (β₁ i)] →
[inst_1 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Dfinsupp fun i => β₁ i) → Dfinsupp fun i => β₂ imapRange (fun _: ?m.65482_ => Neg.neg: {α : Type ?u.65484} → [self : Neg α] → α → αNeg.neg) fun _: ?m.65673_ => neg_zero: ∀ {G : Type ?u.65675} [inst : NegZeroClass G], -0 = 0neg_zero⟩

theorem neg_apply: ∀ [inst : (i : ι) → AddGroup (β i)] (g : Dfinsupp fun i => β i) (i : ι), ↑(-g) i = -↑g ineg_apply [∀ i: ?m.67316i, AddGroup: Type ?u.67319 → Type ?u.67319AddGroup (β: ι → Type vβ i: ?m.67316i)] (g: Dfinsupp fun i => β ig : Π₀ i: ?m.67327i, β: ι → Type vβ i: ?m.67327i) (i: ιi : ι: Type uι) : (-g: Dfinsupp fun i => β ig) i: ιi = -g: Dfinsupp fun i => β ig i: ιi :=
rfl: ∀ {α : Sort ?u.68596} {a : α}, a = arfl
#align dfinsupp.neg_apply Dfinsupp.neg_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g : Dfinsupp fun i => β i) (i : ι), ↑(-g) i = -↑g iDfinsupp.neg_apply

@[simp]
theorem coe_neg: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g : Dfinsupp fun i => β i), ↑(-g) = -↑gcoe_neg [∀ i: ?m.68636i, AddGroup: Type ?u.68639 → Type ?u.68639AddGroup (β: ι → Type vβ i: ?m.68636i)] (g: Dfinsupp fun i => β ig : Π₀ i: ?m.68647i, β: ι → Type vβ i: ?m.68647i) : ⇑(-g: Dfinsupp fun i => β ig) = -g: Dfinsupp fun i => β ig :=
rfl: ∀ {α : Sort ?u.70327} {a : α}, a = arfl
#align dfinsupp.coe_neg Dfinsupp.coe_neg: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g : Dfinsupp fun i => β i), ↑(-g) = -↑gDfinsupp.coe_neg

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddGroup (β i)] → Sub (Dfinsupp fun i => β i)instance [∀ i: ?m.70393i, AddGroup: Type ?u.70396 → Type ?u.70396AddGroup (β: ι → Type vβ i: ?m.70393i)] : Sub: Type ?u.70400 → Type ?u.70400Sub (Π₀ i: ?m.70405i, β: ι → Type vβ i: ?m.70405i) :=
⟨zipWith: {ι : Type ?u.71389} →
{β : ι → Type ?u.71388} →
{β₁ : ι → Type ?u.71387} →
{β₂ : ι → Type ?u.71386} →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → Zero (β₁ i)] →
[inst_2 : (i : ι) → Zero (β₂ i)] →
(f : (i : ι) → β₁ i → β₂ i → β i) →
(∀ (i : ι), f i 0 0 = 0) → (Dfinsupp fun i => β₁ i) → (Dfinsupp fun i => β₂ i) → Dfinsupp fun i => β izipWith (```