/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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
notes in this file for more information. -/
structure 
Dfinsupp: {ι : Type u} → (β : ι → Type v) → [inst : (i : ι) → Zero (β i)] → Type (maxuv)
Dfinsupp [∀ 
i: ?m.54
i, 
Zero: Type ?u.57 → Type ?u.57
Zero (
β: ι → Type v
β 
i: ?m.54
i)] : 
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 : ι) → β i
toFun : ∀ 
i: ?m.63
i, 
β: ι → Type v
β 
i: ?m.63
i
  /-- 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.68
Trunc { 
s: Multiset ι
s : 
Multiset: Type ?u.72 → Type ?u.72
Multiset 
ι: Type u
ι // ∀ 
i: ?m.75
i, 
i: ?m.75
i ∈ 
s: Multiset ι
s ∨ 
toFun: (i : ι) → β i
toFun 
i: ?m.75
i = 
0: ?m.99
0 }
#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.934
r:(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.11496
i, 
Zero: Type ?u.11539 → Type ?u.11539
Zero (
β: ι → Type v
β 
i: ?m.12525
i)] [∀ 
i: ?m.15743
i, 
Zero: Type ?u.15427 → Type ?u.15427
Zero (
β₁: ι → Type v₁
β₁ 
i: ?m.15424
i)] [∀ 
i: ?m.15751
i, 
Zero: Type ?u.12870 → Type ?u.12870
Zero (
β₂: ι → Type v₂
β₂ 
i: ?m.15432
i)]

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.11566
i, 
β: ι → Type v
β 
i: ?m.11566
i) 
ι: Type u
ι 
β: ι → Type v
β :=
  ⟨fun 
f: ?m.11632
f => 
f: ?m.11632
f.
toFun: {ι : Type ?u.11635} → {β : ι → Type ?u.11634} → [inst : (i : ι) → Zero (β i)] → Dfinsupp β → (i : ι) → β i
toFun, fun ⟨
f₁: (i : ι) → β i
f₁, 
s₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
s₁⟩ ⟨
f₂: (i : ι) → β i
f₂, 
s₁: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₂ i = 0 }
s₁⟩ ↦ fun (
h: f₁ = f₂
h : 
f₁: (i : ι) → β i
f₁ = 
f₂: (i : ι) → β i
f₂) ↦ by
Goals 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 => β i

f₁: (i : ι) → β i

s₁✝: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }

f₂: (i : ι) → β i

s₁: 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 => β i

f₁: (i : ι) → β i

s₁✝, 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 => β i

f₁: (i : ι) → β i

s₁✝: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }

f₂: (i : ι) → β i

s₁: 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 => β i

f₁: (i : ι) → β i

s₁✝, 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 => β i

f₁: (i : ι) → β i

s₁✝: Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }

f₂: (i : ι) → β i

s₁: 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 = b
Subsingleton.elim
Goals 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 : ι) → β i
instance : 
CoeFun: (α : Sort ?u.12549) → outParam (α → Sort ?u.12548) → Sort (max(max1?u.12549)?u.12548)
CoeFun (Π₀ 
i: ?m.12554
i, 
β: ι → Type v
β 
i: ?m.12554
i) fun 
_: ?m.12597
_ => ∀ 
i: ?m.12600
i, 
β: ι → Type v
β 
i: ?m.12600
i :=
  
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 = ↑f
toFun_eq_coe (
f: Dfinsupp fun i => β i
f : Π₀ 
i: ?m.12878
i, 
β: ι → Type v
β 
i: ?m.12878
i) : 
f: Dfinsupp fun i => β i
f.
toFun: {ι : Type ?u.12924} → {β : ι → Type ?u.12923} → [inst : (i : ι) → Zero (β i)] → Dfinsupp β → (i : ι) → β i
toFun = 
f: Dfinsupp fun i => β i
f :=
  
rfl: ∀ {α : Sort ?u.13190} {a : α}, a = a
rfl
#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 = ↑f
Dfinsupp.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 = g
ext {
f: Dfinsupp fun i => β i
f 
g: Dfinsupp fun i => β i
g : Π₀ 
i: ?m.13258
i, 
β: ι → Type v
β 
i: ?m.13258
i} (
h: ∀ (i : ι), ↑f i = ↑g i
h : ∀ 
i: ?m.13318
i, 
f: Dfinsupp fun i => β i
f 
i: ?m.13318
i = 
g: Dfinsupp fun i => β i
g 
i: ?m.13318
i) : 
f: Dfinsupp fun i => β i
f = 
g: Dfinsupp fun i => β i
g :=
  
FunLike.ext: ∀ {F : Sort ?u.13422} {α : Sort ?u.13423} {β : α → Sort ?u.13421} [i : FunLike F α β] (f g : F),
  (∀ (x : α), ↑f x = ↑g x) → f = g
FunLike.ext 
_: ?m.13424
_ 
_: ?m.13424
_ 
h: ∀ (i : ι), ↑f i = ↑g i
h
#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 = g
Dfinsupp.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 x
FunLike.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 i
ext_iff {
f: Dfinsupp fun i => β i
f 
g: Dfinsupp fun i => β i
g : Π₀ 
i: ?m.13668
i, 
β: ι → Type v
β 
i: ?m.13668
i} : 
f: Dfinsupp fun i => β i
f = 
g: Dfinsupp fun i => β i
g ↔ ∀ 
i: ?m.13735
i, 
f: Dfinsupp fun i => β i
f 
i: ?m.13735
i = 
g: Dfinsupp fun i => β i
g 
i: ?m.13735
i :=
  
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 x
FunLike.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 i
Dfinsupp.ext_iff

@[deprecated 
FunLike.coe_injective: ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : FunLike F α β], Function.Injective fun f => ↑f
FunLike.coe_injective]
theorem 
coeFn_injective: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)], Function.Injective FunLike.coe
coeFn_injective : @
Function.Injective: {α : Sort ?u.14057} → {β : Sort ?u.14056} → (α → β) → Prop
Function.Injective (Π₀ 
i: ?m.14062
i, 
β: ι → Type v
β 
i: ?m.14062
i) (∀ 
i: ?m.14105
i, 
β: ι → Type v
β 
i: ?m.14105
i) 
(⇑): (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 => ↑f
FunLike.coe_injective
#align dfinsupp.coe_fn_injective 
Dfinsupp.coeFn_injective: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)], Function.Injective FunLike.coe
Dfinsupp.coeFn_injective

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

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.14879
i, 
β: ι → Type v
β 
i: ?m.14879
i) :=
  ⟨
0: ?m.14929
0⟩

@[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 } = f
coe_mk' (
f: (i : ι) → β i
f : ∀ 
i: ?m.15123
i, 
β: ι → Type v
β 
i: ?m.15123
i) (
s: Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s) : ⇑(⟨
f: (i : ι) → β i
f, 
s: ?m.15128
s⟩ : Π₀ 
i: ?m.15137
i, 
β: ι → Type v
β 
i: ?m.15137
i) = 
f: (i : ι) → β i
f :=
  
rfl: ∀ {α : Sort ?u.15346} {a : α}, a = a
rfl
#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 } = f
Dfinsupp.coe_mk'

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

theorem 
zero_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (i : ι), ↑0 i = 0
zero_apply (
i: ι
i : 
ι: Type u
ι) : (
0: ?m.15809
0 : Π₀ 
i: ?m.15766
i, 
β: ι → Type v
β 
i: ?m.15766
i) 
i: ι
i = 
0: ?m.15911
0 :=
  
rfl: ∀ {α : Sort ?u.15959} {a : α}, a = a
rfl
#align dfinsupp.zero_apply 
Dfinsupp.zero_apply: ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (i : ι), ↑0 i = 0
Dfinsupp.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.addMonoidHom`
* `Dfinsupp.mapRange.addEquiv`
* `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 => β₂ i
mapRange (
f: (i : ι) → β₁ i → β₂ i
f : ∀ 
i: ?m.16020
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.16020
i → 
β₂: ι → Type v₂
β₂ 
i: ?m.16020
i) (
hf: ∀ (i : ι), f i 0 = 0
hf : ∀ 
i: ?m.16028
i, 
f: (i : ι) → β₁ i → β₂ i
f 
i: ?m.16028
i 
0: ?m.16033
0 = 
0: ?m.16066
0) (
x: Dfinsupp fun i => β₁ i
x : Π₀ 
i: ?m.16117
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.16117
i) : Π₀ 
i: ?m.16160
i, 
β₂: ι → Type v₂
β₂ 
i: ?m.16160
i :=
  ⟨fun 
i: ?m.16273
i => 
f: (i : ι) → β₁ i → β₂ i
f 
i: ?m.16273
i (
x: Dfinsupp fun i => β₁ i
x 
i: ?m.16273
i),
    
x: Dfinsupp fun i => β₁ i
x.
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.16376
s => ⟨
s: ?m.16376
s.
1: {α : Sort ?u.16436} → {p : α → Prop} → Subtype p → α
1, fun 
i: ?m.16393
i => (
s: ?m.16376
s.
2: ∀ {α : Sort ?u.16442} {p : α → Prop} (self : Subtype p), p ↑self
2 
i: ?m.16393
i).
imp_right: ∀ {b c a : Prop}, (b → c) → a ∨ b → a ∨ c
imp_right fun 
h: ↑x i = 0
h : 
x: Dfinsupp fun i => β₁ i
x 
i: ?m.16393
i = 
0: ?m.16495
0 => by
Goals 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

hf: ∀ (i : ι), f i 0 = 0

x: Dfinsupp fun i => β₁ i

s: { 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 → β₂ i

hf: ∀ (i : ι), f i 0 = 0

x: Dfinsupp fun i => β₁ i

s: { 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 = 0
hf 
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 → β₂ i

hf: ∀ (i : ι), f i 0 = 0

x: Dfinsupp fun i => β₁ i

s: { 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 → β₂ i

hf: ∀ (i : ι), f i 0 = 0

x: Dfinsupp fun i => β₁ i

s: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

i: ι

h: ↑x i = 0

(fun i => f i (↑x i)) i = 0← 
h: ↑x i = 0
h
ι: 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

hf: ∀ (i : ι), f i 0 = 0

x: Dfinsupp fun i => β₁ i

s: { 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 => β₂ i
Dfinsupp.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 → β₂ i
f : ∀ 
i: ?m.16855
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.16855
i → 
β₂: ι → Type v₂
β₂ 
i: ?m.16855
i) (
hf: ∀ (i : ι), f i 0 = 0
hf : ∀ 
i: ?m.16863
i, 
f: (i : ι) → β₁ i → β₂ i
f 
i: ?m.16863
i 
0: ?m.16868
0 = 
0: ?m.16901
0) (
g: Dfinsupp fun i => β₁ i
g : Π₀ 
i: ?m.16952
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.16952
i) (
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 => β₂ i
mapRange 
f: (i : ι) → β₁ i → β₂ i
f 
hf: ∀ (i : ι), f i 0 = 0
hf 
g: Dfinsupp fun i => β₁ i
g 
i: ι
i = 
f: (i : ι) → β₁ i → β₂ i
f 
i: ι
i (
g: Dfinsupp fun i => β₁ i
g 
i: ι
i) :=
  
rfl: ∀ {α : Sort ?u.17202} {a : α}, a = a
rfl
#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 = g
mapRange_id (
h: optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)
h : ∀ 
i: ?m.17319
i, 
id: {α : Sort ?u.17323} → α → α
id (
0: ?m.17327
0 : 
β₁: ι → Type v₁
β₁ 
i: ?m.17319
i) = 
0: ?m.17360
0 := fun 
i: ?m.17378
i => 
rfl: ∀ {α : Sort ?u.17380} {a : α}, a = a
rfl) (
g: Dfinsupp fun i => β₁ i
g : Π₀ 
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 => β₂ i
mapRange (fun 
i: ?m.17443
i => (
id: {α : Sort ?u.17448} → α → α
id : 
β₁: ι → Type v₁
β₁ 
i: ?m.17443
i → 
β₁: ι → Type v₁
β₁ 
i: ?m.17443
i)) 
h: optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)
h 
g: Dfinsupp fun i => β₁ i
g = 
g: Dfinsupp fun i => β₁ i
g := by
Goals 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 => β₁ i

mapRange (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 => β₁ i

i✝: ι

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 => β₁ i

mapRange (fun i => id) h g = grfl
Goals 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 = g
Dfinsupp.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 → β₂ i
f : ∀ 
i: ?m.17661
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.17661
i → 
β₂: ι → Type v₂
β₂ 
i: ?m.17661
i) (
f₂: (i : ι) → β i → β₁ i
f₂ : ∀ 
i: ?m.17669
i, 
β: ι → Type v
β 
i: ?m.17669
i → 
β₁: ι → Type v₁
β₁ 
i: ?m.17669
i) (
hf: ∀ (i : ι), f i 0 = 0
hf : ∀ 
i: ?m.17677
i, 
f: (i : ι) → β₁ i → β₂ i
f 
i: ?m.17677
i 
0: ?m.17682
0 = 
0: ?m.17715
0)
    (
hf₂: ∀ (i : ι), f₂ i 0 = 0
hf₂ : ∀ 
i: ?m.17763
i, 
f₂: (i : ι) → β i → β₁ i
f₂ 
i: ?m.17763
i 
0: ?m.17768
0 = 
0: ?m.17802
0) (
h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
h : ∀ 
i: ?m.17843
i, (
f: (i : ι) → β₁ i → β₂ i
f 
i: ?m.17843
i ∘ 
f₂: (i : ι) → β i → β₁ i
f₂ 
i: ?m.17843
i) 
0: ?m.17861
0 = 
0: ?m.17887
0) (
g: Dfinsupp fun i => β i
g : Π₀ 
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 => β₂ i
mapRange (fun 
i: ?m.17980
i => 
f: (i : ι) → β₁ i → β₂ i
f 
i: ?m.17980
i ∘ 
f₂: (i : ι) → β i → β₁ i
f₂ 
i: ?m.17980
i) 
h: ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
h 
g: Dfinsupp fun i => β i
g = 
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 => β₂ i
mapRange 
f: (i : ι) → β₁ i → β₂ i
f 
hf: ∀ (i : ι), f i 0 = 0
hf (
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 => β₂ i
mapRange 
f₂: (i : ι) → β i → β₁ i
f₂ 
hf₂: ∀ (i : ι), f₂ i 0 = 0
hf₂ 
g: Dfinsupp fun i => β i
g) := by
Goals 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

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)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 → β₂ 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

i✝: ι

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 → β₂ 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)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 → β₂ 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

i✝: ι

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 → β₂ 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

i✝: ι

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 → β₂ 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)rfl
Goals 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 = 0
mapRange_zero (
f: (i : ι) → β₁ i → β₂ i
f : ∀ 
i: ?m.19146
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.19146
i → 
β₂: ι → Type v₂
β₂ 
i: ?m.19146
i) (
hf: ∀ (i : ι), f i 0 = 0
hf : ∀ 
i: ?m.19154
i, 
f: (i : ι) → β₁ i → β₂ i
f 
i: ?m.19154
i 
0: ?m.19159
0 = 
0: ?m.19192
0) :
    
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 => β₂ i
mapRange 
f: (i : ι) → β₁ i → β₂ i
f 
hf: ∀ (i : ι), f i 0 = 0
hf (
0: ?m.19374
0 : Π₀ 
i: ?m.19338
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.19338
i) = 
0: ?m.19439
0 := by
Goals 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

hf: ∀ (i : ι), f i 0 = 0

mapRange 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 → β₂ i

hf: ∀ (i : ι), f i 0 = 0

i✝: ι

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 → β₂ i

hf: ∀ (i : ι), f i 0 = 0

mapRange 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 = 0
coe_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 = 0
Pi.zero_apply, 
hf: ∀ (i : ι), f i 0 = 0
hf]
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 = 0
Dfinsupp.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 => β i
zipWith (
f: (i : ι) → β₁ i → β₂ i → β i
f : ∀ 
i: ?m.20230
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.20230
i → 
β₂: ι → Type v₂
β₂ 
i: ?m.20230
i → 
β: ι → Type v
β 
i: ?m.20230
i) (
hf: ∀ (i : ι), f i 0 0 = 0
hf : ∀ 
i: ?m.20240
i, 
f: (i : ι) → β₁ i → β₂ i → β i
f 
i: ?m.20240
i 
0: ?m.20245
0 
0: ?m.20278
0 = 
0: ?m.20310
0) (
x: Dfinsupp fun i => β₁ i
x : Π₀ 
i: ?m.20363
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.20363
i) (
y: Dfinsupp fun i => β₂ i
y : Π₀ 
i: ?m.20406
i, 
β₂: ι → Type v₂
β₂ 
i: ?m.20406
i) :
    Π₀ 
i: ?m.20446
i, 
β: ι → Type v
β 
i: ?m.20446
i :=
  ⟨fun 
i: ?m.20564
i => 
f: (i : ι) → β₁ i → β₂ i → β i
f 
i: ?m.20564
i (
x: Dfinsupp fun i => β₁ i
x 
i: ?m.20564
i) (
y: Dfinsupp fun i => β₂ i
y 
i: ?m.20564
i), by
Goals 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

Trunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }refine' 
x: Dfinsupp fun i => β₁ i
x.
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.20743
xs => 
_: 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

Trunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }refine' 
y: Dfinsupp fun i => β₂ i
y.
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.20793
ys => 
_: ?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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

Trunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }refine' ⟨
xs: ?m.20743
xs + 
ys: ?m.20793
ys, fun 
i: ?m.21388
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

Trunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }obtain 
h1: i ∈ ↑xs
h1
h1 | (h1 : x i = 0): i ∈ ↑xs ∨ toFun x i = 0
 | (
h1: ↑x i = 0
h1
h1 : x i = 0: toFun x i = 0
 : 
x: Dfinsupp fun i => β₁ i
x
h1 : x i = 0: toFun x i = 0
 
i: ?m.21388
i
h1 : x i = 0: toFun x i = 0
 = 
0: ?m.21524
0
h1 | (h1 : x i = 0): i ∈ ↑xs ∨ toFun x i = 0
) := 
xs: ?m.20743
xs.
prop: ∀ {α : Sort ?u.21396} {p : α → Prop} (x : Subtype p), p ↑x
prop 
i: ?m.21388
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 → β₂ i → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

inr
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

inr
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl.h
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl.h
i ∈ ↑xs + ↑ys
Multiset.mem_add: ∀ {α : Type ?u.21574} {a : α} {s t : Multiset α}, a ∈ s + t ↔ a ∈ s ∨ a ∈ t
Multiset.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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl.h
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl.h
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl.h.h
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: i ∈ ↑xs

inl
i ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0exact 
h1: i ∈ ↑xs
h1
Goals 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

Trunc { s // ∀ (i : ι), i ∈ s ∨ (fun i => f i (↑x i) (↑y i)) i = 0 }obtain 
h2: i ∈ ↑ys
h2
h2 | (h2 : y i = 0): i ∈ ↑ys ∨ toFun y i = 0
 | (
h2: ↑y i = 0
h2
h2 : y i = 0: toFun y i = 0
 : 
y: Dfinsupp fun i => β₂ i
y
h2 : y i = 0: toFun y i = 0
 
i: ?m.21388
i
h2 : y i = 0: toFun y i = 0
 = 
0: ?m.21709
0
h2 | (h2 : y i = 0): i ∈ ↑ys ∨ toFun y i = 0
) := 
ys: ?m.20793
ys.
prop: ∀ {α : Sort ?u.21613} {p : α → Prop} (x : Subtype p), p ↑x
prop 
i: ?m.21388
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 → β₂ i → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.inr
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.inr
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl.h
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl.h
i ∈ ↑xs + ↑ys
Multiset.mem_add: ∀ {α : Type ?u.21758} {a : α} {s t : Multiset α}, a ∈ s + t ↔ a ∈ s ∨ a ∈ t
Multiset.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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl.h
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl.h
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl
i ∈ ↑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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl.h.h
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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: i ∈ ↑ys

inr.inl
i ∈ ↑xs + ↑ys ∨ (fun i => f i (↑x i) (↑y i)) i = 0exact 
h2: i ∈ ↑ys
h2
Goals 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

Trunc { 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

Trunc { 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.inr.h
(fun i => f i (↑x i) (↑y i)) i = 0← 
hf: ∀ (i : ι), f i 0 0 = 0
hf,
ι: 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.inr.h
(fun i => f i (↑x i) (↑y i)) i = 0← 
h1: ↑x i = 0
h1,
ι: 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.inr.h
(fun i => f i (↑x i) (↑y i)) i = 0← 
h2: ↑y i = 0
h2
ι: 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 → β i

hf: ∀ (i : ι), f i 0 0 = 0

x: Dfinsupp fun i => β₁ i

y: Dfinsupp fun i => β₂ i

xs: { s // ∀ (i : ι), i ∈ s ∨ toFun x i = 0 }

ys: { s // ∀ (i : ι), i ∈ s ∨ toFun y i = 0 }

i: ι

h1: ↑x i = 0

h2: ↑y i = 0

inr.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 => β i
Dfinsupp.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 → β i
f : ∀ 
i: ?m.22294
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.22294
i → 
β₂: ι → Type v₂
β₂ 
i: ?m.22294
i → 
β: ι → Type v
β 
i: ?m.22294
i) (
hf: ∀ (i : ι), f i 0 0 = 0
hf : ∀ 
i: ?m.22304
i, 
f: (i : ι) → β₁ i → β₂ i → β i
f 
i: ?m.22304
i 
0: ?m.22309
0 
0: ?m.22342
0 = 
0: ?m.22374
0) (
g₁: Dfinsupp fun i => β₁ i
g₁ : Π₀ 
i: ?m.22427
i, 
β₁: ι → Type v₁
β₁ 
i: ?m.22427
i)
    (
g₂: Dfinsupp fun i => β₂ i
g₂ : Π₀ 
i: ?m.22470
i, 
β₂: ι → Type v₂
β₂ 
i: ?m.22470
i) (
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 => β i
zipWith 
f: (i : ι) → β₁ i → β₂ i → β i
f 
hf: ∀ (i : ι), f i 0 0 = 0
hf 
g₁: Dfinsupp fun i => β₁ i
g₁ 
g₂: Dfinsupp fun i => β₂ i
g₂ 
i: ι
i = 
f: (i : ι) → β₁ i → β₂ i → β i
f 
i: ι
i (
g₁: Dfinsupp fun i => β₁ i
g₁ 
i: ι
i) (
g₂: Dfinsupp fun i => β₂ i
g₂ 
i: ι
i) :=
  
rfl: ∀ {α : Sort ?u.22817} {a : α}, a = a
rfl
#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 => β i
x 
y: Dfinsupp fun i => β i
y : Π₀ 
i: ?m.23806
i, 
β: ι → Type v
β 
i: ?m.22957
i) (
s: Set ι
s : 
Set: Type ?u.24396 → Type ?u.24396
Set 
ι: Type u
ι) [∀ 
i: ?m.23153
i, 
Decidable: Prop → Type
Decidable (
i: ?m.23020
i ∈ 
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 => β i
piecewise : Π₀ 
i: ?m.23183
i, 
β: ι → Type v
β 
i: ?m.23183
i :=
  
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 => β i
zipWith (fun 
i: ?m.23416
i 
x: ?m.23419
x 
y: ?m.23422
y => if 
i: ?m.23416
i ∈ 
s: Set ι
s then 
x: ?m.23419
x else 
y: ?m.23422
y) (fun 
_: ?m.23465
_ => 
ite_self: ∀ {α : Sort ?u.23467} {c : Prop} {d : Decidable c} (a : α), (if c then a else a) = a
ite_self 
0: ?m.23472
0) 
x: Dfinsupp fun i => β i
x 
y: Dfinsupp fun i => β i
y
#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 => β i
Dfinsupp.piecewise

theorem 
piecewise_apply: ∀ (i : ι), ↑(piecewise x y s) i = if i ∈ s then ↑x i else ↑y i
piecewise_apply (
i: ι
i : 
ι: Type u
ι) : 
x: Dfinsupp fun i => β i
x.
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 => β i
piecewise 
y: Dfinsupp fun i => β i
y 
s: Set ι
s 
i: ι
i = if 
i: ι
i ∈ 
s: Set ι
s then 
x: Dfinsupp fun i => β i
x 
i: ι
i else 
y: Dfinsupp fun i => β i
y 
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 => β i
x 
y: Dfinsupp fun i => β i
y 
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 i
Dfinsupp.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 ↑y
coe_piecewise : ⇑(
x: Dfinsupp fun i => β i
x.
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 => β i
piecewise 
y: Dfinsupp fun i => β i
y 
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 : α) → β i
piecewise 
x: Dfinsupp fun i => β i
x 
y: Dfinsupp fun i => β i
y := by
Goals 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 => β i

s: 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 => β i

s: 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 => β i

s: 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 i
piecewise_apply
Goals 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 ↑y
Dfinsupp.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.25073
i, 
AddZeroClass: Type ?u.25076 → Type ?u.25076
AddZeroClass (
β: ι → Type v
β 
i: ?m.25073
i)] : 
Add: Type ?u.25080 → Type ?u.25080
Add (Π₀ 
i: ?m.25085
i, 
β: ι → Type v
β 
i: ?m.25085
i) :=
  ⟨
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 => β i
zipWith (fun 
_: ?m.26666
_ => 
(· + ·): β x✝ → β x✝ → β x✝
(· + ·)) fun 
_: ?m.27131
_ => 
add_zero: ∀ {M : Type ?u.27133} [inst : AddZeroClass M] (a : M), a + 0 = a
add_zero 
0: ?m.27137
0⟩

theorem 
add_apply: ∀ [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Dfinsupp fun i => β i) (i : ι), ↑(g₁ + g₂) i = ↑g₁ i + ↑g₂ i
add_apply [∀ 
i: ?m.29153
i, 
AddZeroClass: Type ?u.29156 → Type ?u.29156
AddZeroClass (
β: ι → Type v
β 
i: ?m.29153
i)] (
g₁: Dfinsupp fun i => β i
g₁ 
g₂: Dfinsupp fun i => β i
g₂ : Π₀ 
i: ?m.30547
i, 
β: ι → Type v
β 
i: ?m.30547
i) (
i: ι
i : 
ι: Type u
ι) :
    (
g₁: Dfinsupp fun i => β i
g₁ + 
g₂: Dfinsupp fun i => β i
g₂) 
i: ι
i = 
g₁: Dfinsupp fun i => β i
g₁ 
i: ι
i + 
g₂: Dfinsupp fun i => β i
g₂ 
i: ι
i :=
  
rfl: ∀ {α : Sort ?u.31221} {a : α}, a = a
rfl
#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₂ i
Dfinsupp.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.31264
i, 
AddZeroClass: Type ?u.31267 → Type ?u.31267
AddZeroClass (
β: ι → Type v
β 
i: ?m.31264
i)] (
g₁: Dfinsupp fun i => β i
g₁ 
g₂: Dfinsupp fun i => β i
g₂ : Π₀ 
i: ?m.32658
i, 
β: ι → Type v
β 
i: ?m.31275
i) : ⇑(
g₁: Dfinsupp fun i => β i
g₁ + 
g₂: Dfinsupp fun i => β i
g₂) = 
g₁: Dfinsupp fun i => β i
g₁ + 
g₂: Dfinsupp fun i => β i
g₂ :=
  
rfl: ∀ {α : Sort ?u.34291} {a : α}, a = a
rfl
#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.34368
i, 
AddZeroClass: Type ?u.34371 → Type ?u.34371
AddZeroClass (
β: ι → Type v
β 
i: ?m.34368
i)] : 
AddZeroClass: Type ?u.34375 → Type ?u.34375
AddZeroClass (Π₀ 
i: ?m.34380
i, 
β: ι → Type v
β 
i: ?m.34380
i) :=
  
FunLike.coe_injective: ∀ {F : Sort ?u.35760} {α : Sort ?u.35761} {β : α → Sort ?u.35762} [i : FunLike F α β], Function.Injective fun f => ↑f
FunLike.coe_injective.
addZeroClass: {M₁ : Type ?u.35835} →
  {M₂ : Type ?u.35834} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : AddZeroClass 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 = 0
coe_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.37744
i, 
AddMonoid: Type ?u.37747 → Type ?u.37747
AddMonoid (
β: ι → Type v
β 
i: ?m.37744
i)] : 
SMul: Type ?u.37752 → Type ?u.37751 → Type (max?u.37752?u.37751)
SMul 
ℕ: Type
ℕ (Π₀ 
i: ?m.37757
i, 
β: ι → Type v
β 
i: ?m.37757
i) :=
  ⟨fun 
c: ?m.38898
c 
v: ?m.38901
v => 
v: ?m.38901
v.
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 => β₂ i
mapRange (fun 
_: ?m.39038
_ => 
(· • ·): ℕ → β x✝ → β x✝
(· • ·) 
c: ?m.38898
c) fun 
_: ?m.39258
_ => 
nsmul_zero: ∀ {A : Type ?u.39260} [inst : AddMonoid A] (n : ℕ), n • 0 = 0
nsmul_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 i
nsmul_apply [∀ 
i: ?m.40766
i, 
AddMonoid: Type ?u.40769 → Type ?u.40769
AddMonoid (
β: ι → Type v
β 
i: ?m.40766
i)] (
b: ℕ
b : 
ℕ: Type
ℕ) (
v: Dfinsupp fun i => β i
v : Π₀ 
i: ?m.40779
i, 
β: ι → Type v
β 
i: ?m.40779
i) (
i: ι
i : 
ι: Type u
ι) : (
b: ℕ
b • 
v: Dfinsupp fun i => β i
v) 
i: ι
i = 
b: ℕ
b • 
v: Dfinsupp fun i => β i
v 
i: ι
i :=
  
rfl: ∀ {α : Sort ?u.42118} {a : α}, a = a
rfl
#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 i
Dfinsupp.nsmul_apply

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

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddMonoid (β i)] → AddMonoid (Dfinsupp fun i => β i)
instance [∀ 
i: ?m.43615
i, 
AddMonoid: Type ?u.43618 → Type ?u.43618
AddMonoid (
β: ι → Type v
β 
i: ?m.43615
i)] : 
AddMonoid: Type ?u.43622 → Type ?u.43622
AddMonoid (Π₀ 
i: ?m.43627
i, 
β: ι → Type v
β 
i: ?m.43627
i) :=
  
FunLike.coe_injective: ∀ {F : Sort ?u.44758} {α : Sort ?u.44759} {β : α → Sort ?u.44760} [i : FunLike F α β], Function.Injective fun f => ↑f
FunLike.coe_injective.
addMonoid: {M₁ : Type ?u.44833} →
  {M₂ : Type ?u.44832} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : AddMonoid 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 = 0
coe_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 • ↑v
coe_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 : ι) → β i
coeFnAddMonoidHom [∀ 
i: ?m.46729
i, 
AddZeroClass: Type ?u.46732 → Type ?u.46732
AddZeroClass (
β: ι → Type v
β 
i: ?m.46729
i)] : (Π₀ 
i: ?m.46742
i, 
β: ι → Type v
β 
i: ?m.46742
i) →+ ∀ 
i: ?m.48120
i, 
β: ι → Type v
β 
i: ?m.48120
i
    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 = 0
coe_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 : ι) → β i
Dfinsupp.coeFnAddMonoidHom

/-- Evaluation at a point is an `AddMonoidHom`. This is the finitely-supported version of
`Pi.evalAddMonoidHom`. -/
def 
evalAddMonoidHom: [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → (Dfinsupp fun i => β i) →+ β i
evalAddMonoidHom [∀ 
i: ?m.51185
i, 
AddZeroClass: Type ?u.51188 → Type ?u.51188
AddZeroClass (
β: ι → Type v
β 
i: ?m.51185
i)] (
i: ι
i : 
ι: Type u
ι) : (Π₀ 
i: ?m.51200
i, 
β: ι → Type v
β 
i: ?m.51200
i) →+ 
β: ι → 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 i
Pi.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 →+ P
comp 
coeFnAddMonoidHom: {ι : Type ?u.52719} →
  {β : ι → Type ?u.52718} → [inst : (i : ι) → AddZeroClass (β i)] → (Dfinsupp fun i => β i) →+ (i : ι) → β i
coeFnAddMonoidHom
#align dfinsupp.eval_add_monoid_hom 
Dfinsupp.evalAddMonoidHom: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → (Dfinsupp fun i => β i) →+ β i
Dfinsupp.evalAddMonoidHom

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddCommMonoid (β i)] → AddCommMonoid (Dfinsupp fun i => β i)
instance [∀ 
i: ?m.52895
i, 
AddCommMonoid: Type ?u.52898 → Type ?u.52898
AddCommMonoid (
β: ι → Type v
β 
i: ?m.52895
i)] : 
AddCommMonoid: Type ?u.52902 → Type ?u.52902
AddCommMonoid (Π₀ 
i: ?m.52907
i, 
β: ι → Type v
β 
i: ?m.52907
i) :=
  
FunLike.coe_injective: ∀ {F : Sort ?u.54147} {α : Sort ?u.54148} {β : α → Sort ?u.54149} [i : FunLike F α β], Function.Injective fun f => ↑f
FunLike.coe_injective.
addCommMonoid: {M₁ : Type ?u.54222} →
  {M₂ : Type ?u.54221} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : AddCommMonoid 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 = 0
coe_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 • ↑v
coe_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.57978
i, 
AddCommMonoid: Type ?u.57981 → Type ?u.57981
AddCommMonoid (
β: ι → Type v
β 
i: ?m.57978
i)] (
s: Finset α
s : 
Finset: Type ?u.57985 → Type ?u.57985
Finset 
α: ?m.57974
α) (
g: α → Dfinsupp fun i => β i
g : 
α: ?m.57974
α → Π₀ 
i: ?m.57994
i, 
β: ι → Type v
β 
i: ?m.57994
i) :
    ⇑(∑ 
a: ?m.59242
a in 
s: Finset α
s, 
g: α → Dfinsupp fun i => β i
g 
a: ?m.59242
a) = ∑ 
a: ?m.59353
a in 
s: Finset α
s, ⇑
g: α → Dfinsupp fun i => β i
g 
a: ?m.59353
a :=
  (
coeFnAddMonoidHom: {ι : Type ?u.60314} →
  {β : ι → Type ?u.60313} → [inst : (i : ι) → AddZeroClass (β i)] → (Dfinsupp fun i => β i) →+ (i : ι) → β i
coeFnAddMonoidHom : 
_: Type ?u.59443
_ →+ ∀ 
i: ?m.59446
i, 
β: ι → Type v
β 
i: ?m.59446
i).
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 => β i
g 
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) i
finset_sum_apply {
α: ?m.61441
α} [∀ 
i: ?m.61445
i, 
AddCommMonoid: Type ?u.61448 → Type ?u.61448
AddCommMonoid (
β: ι → Type v
β 
i: ?m.61445
i)] (
s: Finset α
s : 
Finset: Type ?u.61452 → Type ?u.61452
Finset 
α: ?m.61441
α) (
g: α → Dfinsupp fun i => β i
g : 
α: ?m.61441
α → Π₀ 
i: ?m.61461
i, 
β: ι → Type v
β 
i: ?m.61461
i) (
i: ι
i : 
ι: Type u
ι) :
    (∑ 
a: ?m.62711
a in 
s: Finset α
s, 
g: α → Dfinsupp fun i => β i
g 
a: ?m.62711
a) 
i: ι
i = ∑ 
a: ?m.62822
a in 
s: Finset α
s, 
g: α → Dfinsupp fun i => β i
g 
a: ?m.62822
a 
i: ι
i :=
  (
evalAddMonoidHom: {ι : Type ?u.63270} →
  {β : ι → Type ?u.63269} → [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → (Dfinsupp fun i => β i) →+ β i
evalAddMonoidHom 
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 => β i
g 
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) i
Dfinsupp.finset_sum_apply

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddGroup (β i)] → Neg (Dfinsupp fun i => β i)
instance [∀ 
i: ?m.64351
i, 
AddGroup: Type ?u.64354 → Type ?u.64354
AddGroup (
β: ι → Type v
β 
i: ?m.64351
i)] : 
Neg: Type ?u.64358 → Type ?u.64358
Neg (Π₀ 
i: ?m.64363
i, 
β: ι → Type v
β 
i: ?m.64363
i) :=
  ⟨fun 
f: ?m.65345
f => 
f: ?m.65345
f.
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 => β₂ i
mapRange (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 = 0
neg_zero⟩

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

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

instance: {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddGroup (β i)] → Sub (Dfinsupp fun i => β i)
instance [∀ 
i: ?m.70393
i, 
AddGroup: Type ?u.70396 → Type ?u.70396
AddGroup (
β: ι → Type v
β 
i: ?m.70393
i)] : 
Sub: Type ?u.70400 → Type ?u.70400
Sub (Π₀ 
i: ?m.70405
i, 
β: ι → Type v
β 
i: ?m.70405
i) :=
  ⟨
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 => β i
zipWith (