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: Kenny Lau

! This file was ported from Lean 3 source module algebra.direct_sum.basic
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Dfinsupp.Basic
import Mathlib.GroupTheory.Submonoid.Operations

/-!
# Direct sum

This file defines the direct sum of abelian groups, indexed by a discrete type.

## Notation

`⨁ i, β i` is the n-ary direct sum `DirectSum`.
This notation is in the `DirectSum` locale, accessible after `open DirectSum`.

## References

* https://en.wikipedia.org/wiki/Direct_sum
-/

open BigOperators

universe u v w u₁

variable (ι: Type vι : Type v: Type (v+1)Type v) [dec_ι: DecidableEq ιdec_ι : DecidableEq: Sort ?u.4 → Sort (max1?u.4)DecidableEq ι: Type vι] (β: ι → Type wβ : ι: Type vι → Type w: Type (w+1)Type w)

/-- `DirectSum β` is the direct sum of a family of additive commutative monoids `β i`.

Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum β`. -/
def DirectSum: (ι : Type v) → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → Type (maxwv)DirectSum [∀ i: ?m.33i, AddCommMonoid: Type ?u.36 → Type ?u.36AddCommMonoid (β: ι → Type wβ i: ?m.33i)] : Type _: Type (?u.40+1)Type _ :=
-- Porting note: Failed to synthesize
-- Π₀ i, β i deriving AddCommMonoid, Inhabited
Π₀ i: ?m.47i, β: ι → Type wβ i: ?m.47i
#align direct_sum DirectSum: (ι : Type v) → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → Type (maxwv)DirectSum

-- Porting note: Added inhabited instance manually
instance: (ι : Type v) → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → Inhabited (DirectSum ι β)instance [∀ i: ?m.1313i, AddCommMonoid: Type ?u.1316 → Type ?u.1316AddCommMonoid (β: ι → Type wβ i: ?m.1313i)] : Inhabited: Sort ?u.1320 → Sort (max1?u.1320)Inhabited (DirectSum: (ι : Type ?u.1322) → (β : ι → Type ?u.1321) → [inst : (i : ι) → AddCommMonoid (β i)] → Type (max?u.1321?u.1322)DirectSum ι: Type vι β: ι → Type wβ) :=
inferInstanceAs: (α : Sort ?u.1356) → [i : α] → αinferInstanceAs (Inhabited: Sort ?u.1357 → Sort (max1?u.1357)Inhabited (Π₀ i: ?m.1362i, β: ι → Type wβ i: ?m.1362i))

instance: (ι : Type v) → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → AddCommMonoid (DirectSum ι β)instance [∀ i: ?m.2864i, AddCommMonoid: Type ?u.2867 → Type ?u.2867AddCommMonoid (β: ι → Type wβ i: ?m.2864i)] : AddCommMonoid: Type ?u.2871 → Type ?u.2871AddCommMonoid (DirectSum: (ι : Type ?u.2873) → (β : ι → Type ?u.2872) → [inst : (i : ι) → AddCommMonoid (β i)] → Type (max?u.2872?u.2873)DirectSum ι: Type vι β: ι → Type wβ) :=
inferInstanceAs: (α : Sort ?u.2907) → [i : α] → αinferInstanceAs (AddCommMonoid: Type ?u.2908 → Type ?u.2908AddCommMonoid (Π₀ i: ?m.2913i, β: ι → Type wβ i: ?m.2913i))

instance: (ι : Type v) → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → CoeFun (DirectSum ι β) fun x => (i : ι) → β iinstance [∀ i: ?m.4297i, AddCommMonoid: Type ?u.4300 → Type ?u.4300AddCommMonoid (β: ι → Type wβ i: ?m.4297i)] : CoeFun: (α : Sort ?u.4305) → outParam (α → Sort ?u.4304) → Sort (max(max1?u.4305)?u.4304)CoeFun (DirectSum: (ι : Type ?u.4307) → (β : ι → Type ?u.4306) → [inst : (i : ι) → AddCommMonoid (β i)] → Type (max?u.4306?u.4307)DirectSum ι: Type vι β: ι → Type wβ) fun _: ?m.4340_ => ∀ i: ιi : ι: Type vι, β: ι → Type wβ i: ιi :=
inferInstanceAs: (α : Sort ?u.4358) → [i : α] → αinferInstanceAs (CoeFun: (α : Sort ?u.4360) → outParam (α → Sort ?u.4359) → Sort (max(max1?u.4360)?u.4359)CoeFun (Π₀ i: ?m.4365i, β: ι → Type wβ i: ?m.4365i) fun _: ?m.5597_ => ∀ i: ιi : ι: Type vι, β: ι → Type wβ i: ιi)

-- Porting note: scoped does not work with notation3; TODO rewrite as lean4 notation?
-- scoped[DirectSum]
/-- `⨁ i, f i` is notation for `DirectSum _ f` and equals the direct sum of `fun i ↦ f i`.
Taking the direct sum over multiple arguments is possible, e.g. `⨁ (i) (j), f i j`. -/
notation3"⨁ "(...)", "r: ?m.5920r:(scoped f => DirectSum _ f) => r

-- Porting note: The below recreates some of the lean3 notation, not fully yet
-- section
-- open Std.ExtendedBinder
-- syntax (name := bigdirectsum) "⨁ " extBinders ", " term : term
-- macro_rules (kind := bigdirectsum)
--   | `(⨁ \$_:ident, \$y:ident → \$z:ident) => `(DirectSum _ (fun \$y ↦ \$z))
--   | `(⨁ \$x:ident, \$p) => `(DirectSum _ (fun \$x ↦ \$p))
--   | `(⨁ \$_:ident : \$t:ident, \$p) => `(DirectSum _ (fun \$t ↦ \$p))
--   | `(⨁ (\$x:ident) (\$y:ident), \$p) => `(DirectSum _ (fun \$x ↦ fun \$y ↦ \$p))
-- end

namespace DirectSum

variable {ι: ?m.8747ι}

variable [∀ i: ?m.8766i, AddCommGroup: Type ?u.8792 → Type ?u.8792AddCommGroup (β: ι → Type wβ i: ?m.8789i)]

instance: {ι : Type v} → (β : ι → Type w) → [inst : (i : ι) → AddCommGroup (β i)] → AddCommGroup (DirectSum ι β)instance : AddCommGroup: Type ?u.8796 → Type ?u.8796AddCommGroup (DirectSum: (ι : Type ?u.8798) → (β : ι → Type ?u.8797) → [inst : (i : ι) → AddCommMonoid (β i)] → Type (max?u.8797?u.8798)DirectSum ι: Type vι β: ι → Type wβ) :=
inferInstanceAs: (α : Sort ?u.9613) → [i : α] → αinferInstanceAs (AddCommGroup: Type ?u.9614 → Type ?u.9614AddCommGroup (Π₀ i: ?m.9619i, β: ι → Type wβ i: ?m.9619i))
variable {β: ?m.10604β}

@[simp]
theorem sub_apply: ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommGroup (β i)] (g₁ g₂ : DirectSum ι fun i => β i) (i : ι),
↑(g₁ - g₂) i = ↑g₁ i - ↑g₂ isub_apply (g₁: DirectSum ι fun i => β ig₁ g₂: DirectSum ?m.11453 fun i => β ig₂ : ⨁ i: ?m.10634i, β: ι → Type wβ i: ?m.10634i) (i: ιi : ι: Type vι) : (g₁: DirectSum ?m.10632 fun i => β ig₁ - g₂: DirectSum ?m.11453 fun i => β ig₂) i: ιi = g₁: DirectSum ?m.10632 fun i => β ig₁ i: ιi - g₂: DirectSum ?m.11453 fun i => β ig₂ i: ιi :=
rfl: ∀ {α : Sort ?u.12172} {a : α}, a = arfl
#align direct_sum.sub_apply DirectSum.sub_apply: ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommGroup (β i)] (g₁ g₂ : DirectSum ι fun i => β i) (i : ι),
↑(g₁ - g₂) i = ↑g₁ i - ↑g₂ iDirectSum.sub_apply

variable [∀ i: ?m.36167i, AddCommMonoid: Type ?u.154740 → Type ?u.154740AddCommMonoid (β: ι → Type wβ i: ?m.12254i)]

@[simp]
theorem zero_apply: ∀ {ι : Type v} (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i : ι), ↑0 i = 0zero_apply (i: ιi : ι: Type vι) : (0: ?m.123250 : ⨁ i: ?m.12292i, β: ι → Type wβ i: ?m.12292i) i: ιi = 0: ?m.132820 :=
rfl: ∀ {α : Sort ?u.13851} {a : α}, a = arfl
#align direct_sum.zero_apply DirectSum.zero_apply: ∀ {ι : Type v} (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i : ι), ↑0 i = 0DirectSum.zero_apply

variable {β: ?m.13927β}

@[simp]
theorem add_apply: ∀ (g₁ g₂ : DirectSum ι fun i => β i) (i : ι), ↑(g₁ + g₂) i = ↑g₁ i + ↑g₂ iadd_apply (g₁: DirectSum ?m.13955 fun i => β ig₁ g₂: DirectSum ι fun i => β ig₂ : ⨁ i: ?m.13995i, β: ι → Type wβ i: ?m.13957i) (i: ιi : ι: Type vι) : (g₁: DirectSum ?m.13955 fun i => β ig₁ + g₂: DirectSum ?m.13993 fun i => β ig₂) i: ιi = g₁: DirectSum ?m.13955 fun i => β ig₁ i: ιi + g₂: DirectSum ?m.13993 fun i => β ig₂ i: ιi :=
rfl: ∀ {α : Sort ?u.16125} {a : α}, a = arfl
#align direct_sum.add_apply DirectSum.add_apply: ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (g₁ g₂ : DirectSum ι fun i => β i) (i : ι),
↑(g₁ + g₂) i = ↑g₁ i + ↑g₂ iDirectSum.add_apply

variable (β: ?m.16213β)

-- Porting note: commented out
-- include dec_ι

/-- `mk β s x` is the element of `⨁ i, β i` that is zero outside `s`
and has coefficient `x i` for `i` in `s`. -/
def mk: (s : Finset ι) → ((i : ↑↑s) → β ↑i) →+ DirectSum ι fun i => β imk (s: Finset ιs : Finset: Type ?u.16239 → Type ?u.16239Finset ι: Type vι) : (∀ i: ↑↑si : (↑s: Finset ιs : Set: Type ?u.16246 → Type ?u.16246Set ι: Type vι), β: ι → Type wβ i: ↑↑si.1: {α : Sort ?u.16367} → {p : α → Prop} → Subtype p → α1) →+ ⨁ i: ?m.16380i, β: ι → Type wβ i: ?m.16380i
where
toFun := Dfinsupp.mk: {ι : Type ?u.20834} →
{β : ι → Type ?u.20833} →
[dec : DecidableEq ι] → [inst : (i : ι) → Zero (β i)] → (s : Finset ι) → ((i : ↑↑s) → β ↑i) → Dfinsupp fun i => β iDfinsupp.mk s: Finset ιs
map_add' _: ?m.22295_ _: ?m.22298_ := Dfinsupp.mk_add: ∀ {ι : Type ?u.22301} {β : ι → Type ?u.22300} [dec : DecidableEq ι] [inst : (i : ι) → AddZeroClass (β i)] {s : Finset ι}
{x y : (i : ↑↑s) → β ↑i}, Dfinsupp.mk s (x + y) = Dfinsupp.mk s x + Dfinsupp.mk s yDfinsupp.mk_add
map_zero' := Dfinsupp.mk_zero: ∀ {ι : Type ?u.22058} {β : ι → Type ?u.22057} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)] {s : Finset ι},
Dfinsupp.mk s 0 = 0Dfinsupp.mk_zero
#align direct_sum.mk DirectSum.mk: {ι : Type v} →
[dec_ι : DecidableEq ι] →
(β : ι → Type w) →
[inst : (i : ι) → AddCommMonoid (β i)] → (s : Finset ι) → ((i : ↑↑s) → β ↑i) →+ DirectSum ι fun i => β iDirectSum.mk

/-- `of i` is the natural inclusion map from `β i` to `⨁ i, β i`. -/
def of: (i : ι) → β i →+ DirectSum ι fun i => β iof (i: ιi : ι: Type vι) : β: ι → Type wβ i: ιi →+ ⨁ i: ?m.23720i, β: ι → Type wβ i: ?m.23720i :=
Dfinsupp.singleAddHom: {ι : Type ?u.24863} →
(β : ι → Type ?u.24862) →
[dec : DecidableEq ι] → [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → β i →+ Dfinsupp fun i => β iDfinsupp.singleAddHom β: ι → Type wβ i: ιi
#align direct_sum.of DirectSum.of: {ι : Type v} →
[dec_ι : DecidableEq ι] →
(β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iDirectSum.of

@[simp]
theorem of_eq_same: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i : ι) (x : β i),
↑(↑(of β i) x) i = xof_eq_same (i: ιi : ι: Type vι) (x: β ix : β: ι → Type wβ i: ιi) : (of: {ι : Type ?u.25964} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.25963) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.25965 → Type ?u.25963_ i: ιi x: β ix) i: ιi = x: β ix :=
Dfinsupp.single_eq_same: ∀ {ι : Type ?u.34582} {β : ι → Type ?u.34581} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)] {i : ι} {b : β i},
↑(Dfinsupp.single i b) i = bDfinsupp.single_eq_same
#align direct_sum.of_eq_same DirectSum.of_eq_same: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i : ι) (x : β i),
↑(↑(of β i) x) i = xDirectSum.of_eq_same

theorem of_eq_of_ne: ∀ (i j : ι) (x : β i), i ≠ j → ↑(↑(of β i) x) j = 0of_eq_of_ne (i: ιi j: ιj : ι: Type vι) (x: β ix : β: ι → Type wβ i: ιi) (h: i ≠ jh : i: ιi ≠ j: ιj) : (of: {ι : Type ?u.36186} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.36185) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.36187 → Type ?u.36185_ i: ιi x: β ix) j: ιj = 0: ?m.447980 :=
Dfinsupp.single_eq_of_ne: ∀ {ι : Type ?u.45406} {β : ι → Type ?u.45405} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)] {i i' : ι} {b : β i},
i ≠ i' → ↑(Dfinsupp.single i b) i' = 0Dfinsupp.single_eq_of_ne h: i ≠ jh
#align direct_sum.of_eq_of_ne DirectSum.of_eq_of_ne: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i j : ι) (x : β i),
i ≠ j → ↑(↑(of β i) x) j = 0DirectSum.of_eq_of_ne

@[simp]
theorem support_zero: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)], Dfinsupp.support 0 = ∅support_zero [∀ (i: ιi : ι: Type vι) (x: β ix : β: ι → Type wβ i: ιi), Decidable: Prop → TypeDecidable (x: β ix ≠ 0: ?m.468460)] : (0: ?m.474730 : ⨁ i: ?m.47443i, β: ι → Type wβ i: ?m.47443i).support: {ι : Type ?u.48351} →
{β : ι → Type ?u.48350} →
[dec : DecidableEq ι] →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] → (Dfinsupp fun i => β i) → Finset ιsupport = ∅: ?m.49586∅ :=
Dfinsupp.support_zero: ∀ {ι : Type ?u.49671} {β : ι → Type ?u.49670} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)], Dfinsupp.support 0 = ∅Dfinsupp.support_zero
#align direct_sum.support_zero DirectSum.support_zero: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)], Dfinsupp.support 0 = ∅DirectSum.support_zero

@[simp]
theorem support_of: ∀ [inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (x : β i), x ≠ 0 → Dfinsupp.support (↑(of β i) x) = {i}support_of [∀ (i: ιi : ι: Type vι) (x: β ix : β: ι → Type wβ i: ιi), Decidable: Prop → TypeDecidable (x: β ix ≠ 0: ?m.511890)] (i: ιi : ι: Type vι) (x: β ix : β: ι → Type wβ i: ιi) (h: x ≠ 0h : x: β ix ≠ 0: ?m.517870) :
(of: {ι : Type ?u.52250} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.52249) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.52251 → Type ?u.52249_ i: ιi x: β ix).support: {ι : Type ?u.60810} →
{β : ι → Type ?u.60809} →
[dec : DecidableEq ι] →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] → (Dfinsupp fun i => β i) → Finset ιsupport = {i: ιi} :=
Dfinsupp.support_single_ne_zero: ∀ {ι : Type ?u.62084} {β : ι → Type ?u.62083} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i},
b ≠ 0 → Dfinsupp.support (Dfinsupp.single i b) = {i}Dfinsupp.support_single_ne_zero h: x ≠ 0h
#align direct_sum.support_of DirectSum.support_of: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (x : β i), x ≠ 0 → Dfinsupp.support (↑(of β i) x) = {i}DirectSum.support_of

theorem support_of_subset: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i}, Dfinsupp.support (↑(of β i) b) ⊆ {i}support_of_subset [∀ (i: ιi : ι: Type vι) (x: β ix : β: ι → Type wβ i: ιi), Decidable: Prop → TypeDecidable (x: β ix ≠ 0: ?m.637360)] {i: ιi : ι: Type vι} {b: β ib : β: ι → Type wβ i: ιi} :
(of: {ι : Type ?u.64342} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.64341) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.64343 → Type ?u.64341_ i: ιi b: β ib).support: {ι : Type ?u.72902} →
{β : ι → Type ?u.72901} →
[dec : DecidableEq ι] →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] → (Dfinsupp fun i => β i) → Finset ιsupport ⊆ {i: ιi} :=
Dfinsupp.support_single_subset: ∀ {ι : Type ?u.74134} {β : ι → Type ?u.74133} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i}, Dfinsupp.support (Dfinsupp.single i b) ⊆ {i}Dfinsupp.support_single_subset
#align direct_sum.support_of_subset DirectSum.support_of_subset: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i}, Dfinsupp.support (↑(of β i) b) ⊆ {i}DirectSum.support_of_subset

theorem sum_support_of: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (x : DirectSum ι fun i => β i),
∑ i in Dfinsupp.support x, ↑(of β i) (↑x i) = xsum_support_of [∀ (i: ιi : ι: Type vι) (x: β ix : β: ι → Type wβ i: ιi), Decidable: Prop → TypeDecidable (x: β ix ≠ 0: ?m.756940)] (x: DirectSum ι fun i => β ix : ⨁ i: ?m.76289i, β: ι → Type wβ i: ?m.76289i) :
(∑ i: ?m.77564i in x: DirectSum ?m.76287 fun i => β ix.support: {ι : Type ?u.76327} →
{β : ι → Type ?u.76326} →
[dec : DecidableEq ι] →
[inst : (i : ι) → Zero (β i)] →
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] → (Dfinsupp fun i => β i) → Finset ιsupport, of: {ι : Type ?u.77567} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.77566) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof β: ι → Type wβ i: ?m.77564i (x: DirectSum ?m.76287 fun i => β ix i: ?m.77564i)) = x: DirectSum ?m.76287 fun i => β ix :=
Dfinsupp.sum_single: ∀ {ι : Type ?u.86128} {β : ι → Type ?u.86127} [dec : DecidableEq ι] [inst : (i : ι) → AddCommMonoid (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Dfinsupp fun i => β i}, Dfinsupp.sum f Dfinsupp.single = fDfinsupp.sum_single
#align direct_sum.sum_support_of DirectSum.sum_support_of: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)]
[inst_1 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (x : DirectSum ι fun i => β i),
∑ i in Dfinsupp.support x, ↑(of β i) (↑x i) = xDirectSum.sum_support_of

variable {β: ?m.86822β}

theorem mk_injective: ∀ (s : Finset ι), Function.Injective ↑(mk β s)mk_injective (s: Finset ιs : Finset: Type ?u.86848 → Type ?u.86848Finset ι: Type vι) : Function.Injective: {α : Sort ?u.86852} → {β : Sort ?u.86851} → (α → β) → PropFunction.Injective (mk: {ι : Type ?u.86856} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.86855) →
[inst : (i : ι) → AddCommMonoid (β i)] → (s : Finset ι) → ((i : ↑↑s) → β ↑i) →+ DirectSum ι fun i => β imk β: ι → Type wβ s: Finset ιs) :=
Dfinsupp.mk_injective: ∀ {ι : Type ?u.95385} {β : ι → Type ?u.95384} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)] (s : Finset ι),
Function.Injective (Dfinsupp.mk s)Dfinsupp.mk_injective s: Finset ιs
#align direct_sum.mk_injective DirectSum.mk_injective: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset ι),
Function.Injective ↑(mk β s)DirectSum.mk_injective

theorem of_injective: ∀ (i : ι), Function.Injective ↑(of β i)of_injective (i: ιi : ι: Type vι) : Function.Injective: {α : Sort ?u.96829} → {β : Sort ?u.96828} → (α → β) → PropFunction.Injective (of: {ι : Type ?u.96833} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.96832) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof β: ι → Type wβ i: ιi) :=
Dfinsupp.single_injective: ∀ {ι : Type ?u.105350} {β : ι → Type ?u.105349} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)] {i : ι},
Function.Injective (Dfinsupp.single i)Dfinsupp.single_injective
#align direct_sum.of_injective DirectSum.of_injective: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (i : ι),
Function.Injective ↑(of β i)DirectSum.of_injective

@[elab_as_elim]
protected theorem induction_on: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)]
{C : (DirectSum ι fun i => β i) → Prop} (x : DirectSum ι fun i => β i),
C 0 → (∀ (i : ι) (x : β i), C (↑(of β i) x)) → (∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)) → C xinduction_on {C: (DirectSum ?m.106872 fun i => β i) → PropC : (⨁ i: ?m.106874i, β: ι → Type wβ i: ?m.106874i) → Prop: TypeProp} (x: DirectSum ?m.106911 fun i => β ix : ⨁ i: ?m.106913i, β: ι → Type wβ i: ?m.106913i) (H_zero: C 0H_zero : C: (DirectSum ?m.106872 fun i => β i) → PropC 0: ?m.1069250)
(H_basic: ∀ (i : ι) (x : β i), C (↑(of β i) x)H_basic : ∀ (i: ιi : ι: Type vι) (x: β ix : β: ι → Type wβ i: ιi), C: (DirectSum ?m.106872 fun i => β i) → PropC (of: {ι : Type ?u.107841} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.107840) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof β: ι → Type wβ i: ιi x: β ix))
(H_plus: ∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)H_plus : ∀ x: ?m.116348x y: ?m.116351y, C: (DirectSum ?m.106872 fun i => β i) → PropC x: ?m.116348x → C: (DirectSum ?m.106872 fun i => β i) → PropC y: ?m.116351y → C: (DirectSum ?m.106872 fun i => β i) → PropC (x: ?m.116348x + y: ?m.116351y)) : C: (DirectSum ?m.106872 fun i => β i) → PropC x: DirectSum ?m.106911 fun i => β ix := byGoals accomplished! 🐙
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝: (i : ι) → AddCommMonoid (β i)C: (DirectSum ι fun i => β i) → Propx: DirectSum ι fun i => β iH_zero: C 0H_basic: ∀ (i : ι) (x : β i), C (↑(of β i) x)H_plus: ∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)C xapply Dfinsupp.induction: ∀ {ι : Type ?u.117154} {β : ι → Type ?u.117153} [dec : DecidableEq ι] [inst : (i : ι) → AddZeroClass (β i)]
{p : (Dfinsupp fun i => β i) → Prop} (f : Dfinsupp fun i => β i),
p 0 → (∀ (i : ι) (b : β i) (f : Dfinsupp fun i => β i), ↑f i = 0 → b ≠ 0 → p f → p (Dfinsupp.single i b + f)) → p fDfinsupp.induction x: DirectSum ι fun i => β ix H_zero: C 0H_zeroι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝: (i : ι) → AddCommMonoid (β i)C: (DirectSum ι fun i => β i) → Propx: DirectSum ι fun i => β iH_zero: C 0H_basic: ∀ (i : ι) (x : β i), C (↑(of β i) x)H_plus: ∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)∀ (i : ι) (b : (fun i => β i) i) (f : Dfinsupp fun i => (fun i => β i) i),
↑f i = 0 → b ≠ 0 → C f → C (Dfinsupp.single i b + f)
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝: (i : ι) → AddCommMonoid (β i)C: (DirectSum ι fun i => β i) → Propx: DirectSum ι fun i => β iH_zero: C 0H_basic: ∀ (i : ι) (x : β i), C (↑(of β i) x)H_plus: ∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)C xintro i: ιi b: β ib f: Dfinsupp fun i => (fun i => β i) if h1: ↑f i = 0h1 h2: b ≠ 0h2 ih: C fihι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝: (i : ι) → AddCommMonoid (β i)C: (DirectSum ι fun i => β i) → Propx: DirectSum ι fun i => β iH_zero: C 0H_basic: ∀ (i : ι) (x : β i), C (↑(of β i) x)H_plus: ∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)i: ιb: β if: Dfinsupp fun i => (fun i => β i) ih1: ↑f i = 0h2: b ≠ 0ih: C fC (Dfinsupp.single i b + f)
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝: (i : ι) → AddCommMonoid (β i)C: (DirectSum ι fun i => β i) → Propx: DirectSum ι fun i => β iH_zero: C 0H_basic: ∀ (i : ι) (x : β i), C (↑(of β i) x)H_plus: ∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)C xsolve_by_elimGoals accomplished! 🐙
#align direct_sum.induction_on DirectSum.induction_on: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)]
{C : (DirectSum ι fun i => β i) → Prop} (x : DirectSum ι fun i => β i),
C 0 → (∀ (i : ι) (x : β i), C (↑(of β i) x)) → (∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)) → C xDirectSum.induction_on

/-- If two additive homomorphisms from `⨁ i, β i` are equal on each `of β i y`,
then they are equal. -/
theorem addHom_ext: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u_1}
[inst_1 : AddMonoid γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
(∀ (i : ι) (y : β i), ↑f (↑(of β i) y) = ↑g (↑(of β i) y)) → f = gaddHom_ext {γ: Type u_1γ : Type _: Type (?u.118528+1)Type _} [AddMonoid: Type ?u.118531 → Type ?u.118531AddMonoid γ: Type ?u.118528γ] ⦃f: (DirectSum ?m.118538 fun i => β i) →+ γf g: (DirectSum ?m.119327 fun i => β i) →+ γg : (⨁ i: ?m.118540i, β: ι → Type wβ i: ?m.119329i) →+ γ: Type ?u.118528γ⦄
(H: ∀ (i : ι) (y : β i), ↑f (↑(of β i) y) = ↑g (↑(of β i) y)H : ∀ (i: ιi : ι: Type vι) (y: β iy : β: ι → Type wβ i: ιi), f: (DirectSum ?m.118538 fun i => β i) →+ γf (of: {ι : Type ?u.127784} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.127783) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.127785 → Type ?u.127783_ i: ιi y: β iy) = g: (DirectSum ?m.119327 fun i => β i) →+ γg (of: {ι : Type ?u.144741} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.144740) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.144742 → Type ?u.144740_ i: ιi y: β iy)) : f: (DirectSum ?m.118538 fun i => β i) →+ γf = g: (DirectSum ?m.119327 fun i => β i) →+ γg :=
Dfinsupp.addHom_ext: ∀ {ι : Type ?u.153254} {β : ι → Type ?u.153253} [dec : DecidableEq ι] [inst : (i : ι) → AddZeroClass (β i)]
{γ : Type ?u.153252} [inst_1 : AddZeroClass γ] ⦃f g : (Dfinsupp fun i => β i) →+ γ⦄,
(∀ (i : ι) (y : β i), ↑f (Dfinsupp.single i y) = ↑g (Dfinsupp.single i y)) → f = gDfinsupp.addHom_ext H: ∀ (i : ι) (y : β i), ↑f (↑(of β i) y) = ↑g (↑(of β i) y)H
#align direct_sum.add_hom_ext DirectSum.addHom_ext: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u_1}
[inst_1 : AddMonoid γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
(∀ (i : ι) (y : β i), ↑f (↑(of β i) y) = ↑g (↑(of β i) y)) → f = gDirectSum.addHom_ext

/-- If two additive homomorphisms from `⨁ i, β i` are equal on each `of β i y`,
then they are equal.

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem addHom_ext': ∀ {γ : Type u_1} [inst : AddMonoid γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
(∀ (i : ι), AddMonoidHom.comp f (of (fun i => β i) i) = AddMonoidHom.comp g (of (fun i => β i) i)) → f = gaddHom_ext' {γ: Type ?u.154744γ : Type _: Type (?u.154744+1)Type _} [AddMonoid: Type ?u.154747 → Type ?u.154747AddMonoid γ: Type ?u.154744γ] ⦃f: (DirectSum ?m.154754 fun i => β i) →+ γf g: (DirectSum ?m.155543 fun i => β i) →+ γg : (⨁ i: ?m.154756i, β: ι → Type wβ i: ?m.154756i) →+ γ: Type ?u.154744γ⦄
(H: ∀ (i : ι), AddMonoidHom.comp f (of (fun i => β i) i) = AddMonoidHom.comp g (of (fun i => β i) i)H : ∀ i: ιi : ι: Type vι, f: (DirectSum ?m.154754 fun i => β i) →+ γf.comp: {M : Type ?u.155564} →
{N : Type ?u.155563} →
{P : Type ?u.155562} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ Pcomp (of: {ι : Type ?u.155585} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.155584) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.155586 → Type ?u.155584_ i: ιi) = g: (DirectSum ?m.155543 fun i => β i) →+ γg.comp: {M : Type ?u.156424} →
{N : Type ?u.156423} →
{P : Type ?u.156422} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ Pcomp (of: {ι : Type ?u.156440} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.156439) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.156441 → Type ?u.156439_ i: ιi)) : f: (DirectSum ?m.154754 fun i => β i) →+ γf = g: (DirectSum ?m.155543 fun i => β i) →+ γg :=
addHom_ext: ∀ {ι : Type ?u.156523} [dec_ι : DecidableEq ι] {β : ι → Type ?u.156522} [inst : (i : ι) → AddCommMonoid (β i)]
{γ : Type ?u.156524} [inst_1 : AddMonoid γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
(∀ (i : ι) (y : β i), ↑f (↑(of β i) y) = ↑g (↑(of β i) y)) → f = gaddHom_ext fun i: ?m.156705i => FunLike.congr_fun: ∀ {F : Sort ?u.156707} {α : Sort ?u.156709} {β : α → Sort ?u.156708} [i : FunLike F α β] {f g : F},
f = g → ∀ (x : α), ↑f x = ↑g xFunLike.congr_fun <| H: ∀ (i : ι), AddMonoidHom.comp f (of (fun i => β i) i) = AddMonoidHom.comp g (of (fun i => β i) i)H i: ?m.156705i
#align direct_sum.add_hom_ext' DirectSum.addHom_ext': ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u_1}
[inst_1 : AddMonoid γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
(∀ (i : ι), AddMonoidHom.comp f (of (fun i => β i) i) = AddMonoidHom.comp g (of (fun i => β i) i)) → f = gDirectSum.addHom_ext'

variable {γ: Type u₁γ : Type u₁: Type (u₁+1)Type u₁} [AddCommMonoid: Type ?u.333812 → Type ?u.333812AddCommMonoid γ: Type u₁γ]

variable (φ: (i : ι) → β i →+ γφ : ∀ i: ?m.171386i, β: ι → Type wβ i: ?m.167171i →+ γ: Type u₁γ) (ψ: (DirectSum ?m.168006 fun i => β i) →+ γψ : (⨁ i: ?m.168008i, β: ι → Type wβ i: ?m.166411i) →+ γ: Type u₁γ)

-- Porting note: The elaborator is struggling with `liftAddHom`. Passing it `β` explicitly helps.
-- This applies to roughly the remainder of the file.

/-- `toAddMonoid φ` is the natural homomorphism from `⨁ i, β i` to `γ`
induced by a family `φ` of homomorphisms `β i → γ`. -/
def toAddMonoid: {ι : Type v} →
[dec_ι : DecidableEq ι] →
{β : ι → Type w} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type u₁} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γtoAddMonoid : (⨁ i: ?m.168745i, β: ι → Type wβ i: ?m.168745i) →+ γ: Type u₁γ :=
Dfinsupp.liftAddHom: {ι : Type ?u.169926} →
{γ : Type ?u.169924} →
{β : ι → Type ?u.169925} →
[dec : DecidableEq ι] →
[inst : (i : ι) → AddZeroClass (β i)] →
[inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) ≃+ ((Dfinsupp fun i => β i) →+ γ)Dfinsupp.liftAddHom (β := β: ι → Type wβ) φ: (i : ι) → β i →+ γφ
[dec_ι : DecidableEq ι] →
{β : ι → Type w} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type u₁} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γDirectSum.toAddMonoid

@[simp]
theorem toAddMonoid_of: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁}
[inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i), ↑(toAddMonoid φ) (↑(of β i) x) = ↑(φ i) xtoAddMonoid_of (i: ιi) (x: β ix : β: ι → Type wβ i: ?m.172954i) : toAddMonoid: {ι : Type ?u.172962} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.172961} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.172960} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γtoAddMonoid φ: (i : ι) → β i →+ γφ (of: {ι : Type ?u.181496} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.181495) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof β: ι → Type wβ i: ?m.172954i x: β ix) = φ: (i : ι) → β i →+ γφ i: ?m.172954i x: β ix :=
Dfinsupp.liftAddHom_apply_single: ∀ {ι : Type ?u.198348} {γ : Type ?u.198346} {β : ι → Type ?u.198347} [dec : DecidableEq ι]
[inst : (i : ι) → AddZeroClass (β i)] [inst_1 : AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι) (x : β i),
↑(↑Dfinsupp.liftAddHom f) (Dfinsupp.single i x) = ↑(f i) xDfinsupp.liftAddHom_apply_single φ: (i : ι) → β i →+ γφ i: ιi x: β ix
#align direct_sum.to_add_monoid_of DirectSum.toAddMonoid_of: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁}
[inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i), ↑(toAddMonoid φ) (↑(of β i) x) = ↑(φ i) xDirectSum.toAddMonoid_of

theorem toAddMonoid.unique: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁}
[inst_1 : AddCommMonoid γ] (ψ : (DirectSum ι fun i => β i) →+ γ) (f : DirectSum ι fun i => β i),
↑ψ f = ↑(toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)) ftoAddMonoid.unique (f: DirectSum ?m.201131 fun i => β if : ⨁ i: ?m.201133i, β: ι → Type wβ i: ?m.201133i) : ψ: (DirectSum ?m.200396 fun i => β i) →+ γψ f: DirectSum ?m.201131 fun i => β if = toAddMonoid: {ι : Type ?u.209606} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.209605} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.209604} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γtoAddMonoid (fun i: ?m.209614i => ψ: (DirectSum ?m.200396 fun i => β i) →+ γψ.comp: {M : Type ?u.209618} →
{N : Type ?u.209617} →
{P : Type ?u.209616} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ Pcomp (of: {ι : Type ?u.210815} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.210814) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof β: ι → Type wβ i: ?m.209614i)) f: DirectSum ?m.201131 fun i => β if := byGoals accomplished! 🐙
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γφ: (i : ι) → β i →+ γψ: (DirectSum ι fun i => β i) →+ γf: DirectSum ι fun i => β i↑ψ f = ↑(toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)) fcongrι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γφ: (i : ι) → β i →+ γψ: (DirectSum ι fun i => β i) →+ γf: DirectSum ι fun i => β ie_aψ = toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)
-- Porting note: ext applied unsuitable ext lemma
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γφ: (i : ι) → β i →+ γψ: (DirectSum ι fun i => β i) →+ γf: DirectSum ι fun i => β i↑ψ f = ↑(toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)) fapply Dfinsupp.addHom_ext': ∀ {ι : Type ?u.219982} {β : ι → Type ?u.219981} [dec : DecidableEq ι] [inst : (i : ι) → AddZeroClass (β i)]
{γ : Type ?u.219980} [inst_1 : AddZeroClass γ] ⦃f g : (Dfinsupp fun i => β i) →+ γ⦄,
(∀ (x : ι), AddMonoidHom.comp f (Dfinsupp.singleAddHom β x) = AddMonoidHom.comp g (Dfinsupp.singleAddHom β x)) → f = gDfinsupp.addHom_ext'ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γφ: (i : ι) → β i →+ γψ: (DirectSum ι fun i => β i) →+ γf: DirectSum ι fun i => β ie_a.H∀ (x : ι),
(Dfinsupp.singleAddHom (fun i => (fun i => β i) i) x)
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γφ: (i : ι) → β i →+ γψ: (DirectSum ι fun i => β i) →+ γf: DirectSum ι fun i => β i↑ψ f = ↑(toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)) fsimp [toAddMonoid: {ι : Type ?u.220830} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.220829} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.220828} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γtoAddMonoid, of: {ι : Type ?u.220833} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.220832) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof]Goals accomplished! 🐙
#align direct_sum.to_add_monoid.unique DirectSum.toAddMonoid.unique: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁}
[inst_1 : AddCommMonoid γ] (ψ : (DirectSum ι fun i => β i) →+ γ) (f : DirectSum ι fun i => β i),

/-- `fromAddMonoid φ` is the natural homomorphism from `γ` to `⨁ i, β i`
induced by a family `φ` of homomorphisms `γ → β i`.

Note that this is not an isomorphism. Not every homomorphism `γ →+ ⨁ i, β i` arises in this way. -/
def fromAddMonoid: (DirectSum ι fun i => γ →+ β i) →+ γ →+ DirectSum ι fun i => β ifromAddMonoid : (⨁ i: ?m.224425i, γ: Type u₁γ →+ β: ι → Type wβ i: ?m.224425i) →+ γ: Type u₁γ →+ ⨁ i: ?m.225655i, β: ι → Type wβ i: ?m.225655i :=
toAddMonoid: {ι : Type ?u.227794} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.227793} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.227792} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γtoAddMonoid fun i: ?m.228003i => AddMonoidHom.compHom: {M : Type ?u.228007} →
{N : Type ?u.228006} →
{P : Type ?u.228005} →
[inst : AddZeroClass M] → [inst_1 : AddCommMonoid N] → [inst_2 : AddCommMonoid P] → (N →+ P) →+ (M →+ N) →+ M →+ PAddMonoidHom.compHom (of: {ι : Type ?u.236548} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.236547) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof β: ι → Type wβ i: ?m.228003i)
[dec_ι : DecidableEq ι] →
{β : ι → Type w} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type u₁} → [inst_1 : AddCommMonoid γ] → (DirectSum ι fun i => γ →+ β i) →+ γ →+ DirectSum ι fun i => β iDirectSum.fromAddMonoid

@[simp]
theorem fromAddMonoid_of: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁}
[inst_1 : AddCommMonoid γ] (i : ι) (f : γ →+ β i),
↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) ffromAddMonoid_of (i: ιi : ι: Type vι) (f: γ →+ β if : γ: Type u₁γ →+ β: ι → Type wβ i: ιi) : fromAddMonoid: {ι : Type ?u.237818} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.237817} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.237816} →
[inst_1 : AddCommMonoid γ] → (DirectSum ι fun i => γ →+ β i) →+ γ →+ DirectSum ι fun i => β ifromAddMonoid (of: {ι : Type ?u.246440} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.246439) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.246441 → Type ?u.246439_ i: ιi f: γ →+ β if) = (of: {ι : Type ?u.255391} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.255390) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.255392 → Type ?u.255390_ i: ιi).comp: {M : Type ?u.255447} →
{N : Type ?u.255446} →
{P : Type ?u.255445} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ Pcomp f: γ →+ β if := byGoals accomplished! 🐙
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β i↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) frw [ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β i↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) ffromAddMonoid: {ι : Type ?u.256703} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.256702} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.256701} →
{γ : Type ?u.256704} [inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
↑(toAddMonoid φ) (↑(of β i) x) = ↑(φ i) xtoAddMonoid_ofι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β i↑(↑AddMonoidHom.compHom (of β i)) f = AddMonoidHom.comp (of β i) f]ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β i↑(↑AddMonoidHom.compHom (of β i)) f = AddMonoidHom.comp (of β i) f
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β i↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) frflGoals accomplished! 🐙
#align direct_sum.from_add_monoid_of DirectSum.fromAddMonoid_of: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁}
[inst_1 : AddCommMonoid γ] (i : ι) (f : γ →+ β i),
↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) fDirectSum.fromAddMonoid_of

theorem fromAddMonoid_of_apply: ∀ (i : ι) (f : γ →+ β i) (x : γ), ↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)fromAddMonoid_of_apply (i: ιi : ι: Type vι) (f: γ →+ β if : γ: Type u₁γ →+ β: ι → Type wβ i: ιi) (x: γx : γ: Type u₁γ) :
fromAddMonoid: {ι : Type ?u.258825} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.258824} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.258823} →
[inst_1 : AddCommMonoid γ] → (DirectSum ι fun i => γ →+ β i) →+ γ →+ DirectSum ι fun i => β ifromAddMonoid (of: {ι : Type ?u.267447} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.267446) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.267448 → Type ?u.267446_ i: ιi f: γ →+ β if) x: γx = of: {ι : Type ?u.284894} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.284893) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof _: ?m.284895 → Type ?u.284893_ i: ιi (f: γ →+ β if x: γx) := byGoals accomplished! 🐙
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β ix: γ↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)rw [ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β ix: γ↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)fromAddMonoid_of: ∀ {ι : Type ?u.301805} [dec_ι : DecidableEq ι] {β : ι → Type ?u.301804} [inst : (i : ι) → AddCommMonoid (β i)]
{γ : Type ?u.301803} [inst_1 : AddCommMonoid γ] (i : ι) (f : γ →+ β i),
[inst_2 : AddZeroClass P] (g : N →+ P) (f : M →+ N), ↑(AddMonoidHom.comp g f) = ↑g ∘ ↑fAddMonoidHom.coe_comp,ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β ix: γ(↑(of β i) ∘ ↑f) x = ↑(of β i) (↑f x) ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β ix: γ↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)Function.comp: {α : Sort ?u.303774} → {β : Sort ?u.303773} → {δ : Sort ?u.303772} → (β → δ) → (α → β) → α → δFunction.compι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γi: ιf: γ →+ β ix: γ↑(of β i) (↑f x) = ↑(of β i) (↑f x)]Goals accomplished! 🐙
#align direct_sum.from_add_monoid_of_apply DirectSum.fromAddMonoid_of_apply: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁}
[inst_1 : AddCommMonoid γ] (i : ι) (f : γ →+ β i) (x : γ),
↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)DirectSum.fromAddMonoid_of_apply

variable (β: ?m.303860β)

-- TODO: generalize this to remove the assumption `S ⊆ T`.
/-- `setToSet β S T h` is the natural homomorphism `⨁ (i : S), β i → ⨁ (i : T), β i`,
where `h : S ⊆ T`. -/
def setToSet: (S T : Set ι) → S ⊆ T → (DirectSum ↑S fun i => β ↑i) →+ DirectSum ↑T fun i => β ↑isetToSet (S: Set ιS T: Set ιT : Set: Type ?u.303891 → Type ?u.303891Set ι: Type vι) (H: S ⊆ TH : S: Set ιS ⊆ T: Set ιT) : (⨁ i: ↑Si : S: Set ιS, β: ι → Type wβ i: ↑Si) →+ ⨁ i: ↑Ti : T: Set ιT, β: ι → Type wβ i: ↑Ti :=
toAddMonoid: {ι : Type ?u.305499} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.305498} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.305497} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γtoAddMonoid fun i: ?m.305712i => of: {ι : Type ?u.305715} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.305714) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof (fun i: Subtype Ti : Subtype: {α : Sort ?u.305719} → (α → Prop) → Sort (max1?u.305719)Subtype T: Set ιT => β: ι → Type wβ i: Subtype Ti) ⟨↑i: ?m.305712i, H: S ⊆ TH i: ?m.305712i.2: ∀ {α : Sort ?u.305887} {p : α → Prop} (self : Subtype p), p ↑self2⟩
#align direct_sum.set_to_set DirectSum.setToSet: {ι : Type v} →
[dec_ι : DecidableEq ι] →
(β : ι → Type w) →
[inst : (i : ι) → AddCommMonoid (β i)] →
(S T : Set ι) → S ⊆ T → (DirectSum ↑S fun i => β ↑i) →+ DirectSum ↑T fun i => β ↑iDirectSum.setToSet

variable {β: ?m.306723β}

-- Porting note: commented out
-- omit dec_ι

instance unique: [inst : ∀ (i : ι), Subsingleton (β i)] → Unique (DirectSum ι fun i => β i)unique [∀ i: ?m.306755i, Subsingleton: Sort ?u.306758 → PropSubsingleton (β: ι → Type wβ i: ?m.306755i)] : Unique: Sort ?u.306762 → Sort (max1?u.306762)Unique (⨁ i: ?m.306767i, β: ι → Type wβ i: ?m.306767i) :=
Dfinsupp.unique: {ι : Type ?u.306804} →
{β : ι → Type ?u.306803} →
[inst : (i : ι) → Zero (β i)] → [inst_1 : ∀ (i : ι), Subsingleton (β i)] → Unique (Dfinsupp fun i => β i)Dfinsupp.unique
#align direct_sum.unique DirectSum.unique: {ι : Type v} →
{β : ι → Type w} →
[inst : (i : ι) → AddCommMonoid (β i)] →
[inst_1 : ∀ (i : ι), Subsingleton (β i)] → Unique (DirectSum ι fun i => β i)DirectSum.unique

/-- A direct sum over an empty type is trivial. -/
instance uniqueOfIsEmpty: [inst : IsEmpty ι] → Unique (DirectSum ι fun i => β i)uniqueOfIsEmpty [IsEmpty: Sort ?u.308305 → PropIsEmpty ι: Type vι] : Unique: Sort ?u.308308 → Sort (max1?u.308308)Unique (⨁ i: ?m.308313i, β: ι → Type wβ i: ?m.308313i) :=
Dfinsupp.uniqueOfIsEmpty: {ι : Type ?u.308350} →
{β : ι → Type ?u.308349} → [inst : (i : ι) → Zero (β i)] → [inst_1 : IsEmpty ι] → Unique (Dfinsupp fun i => β i)Dfinsupp.uniqueOfIsEmpty
#align direct_sum.unique_of_is_empty DirectSum.uniqueOfIsEmpty: {ι : Type v} →
{β : ι → Type w} → [inst : (i : ι) → AddCommMonoid (β i)] → [inst_1 : IsEmpty ι] → Unique (DirectSum ι fun i => β i)DirectSum.uniqueOfIsEmpty

/-- The natural equivalence between `⨁ _ : ι, M` and `M` when `Unique ι`. -/
protected def id: (M : Type v) →
(ι : optParam (Type u_1) PUnit) → [inst : AddCommMonoid M] → [inst_1 : Unique ι] → (DirectSum ι fun _x => M) ≃+ Mid (M: Type vM : Type v: Type (v+1)Type v) (ι: optParam (Type ?u.309819) PUnitι : Type _: Type (?u.309819+1)Type _ := PUnit: Sort ?u.309820PUnit) [AddCommMonoid: Type ?u.309823 → Type ?u.309823AddCommMonoid M: Type vM] [Unique: Sort ?u.309826 → Sort (max1?u.309826)Unique ι: optParam (Type ?u.309819) PUnitι] :
(⨁ _x: ι_x : ι: optParam (Type ?u.309819) PUnitι, M: Type vM) ≃+ M: Type vM :=
{
DirectSum.toAddMonoid: {ι : Type ?u.310939} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.310938} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.310937} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γDirectSum.toAddMonoid fun _: ?m.311108_ =>
M: Type vM with
toFun := DirectSum.toAddMonoid: {ι : Type ?u.312502} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.312501} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.312500} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γDirectSum.toAddMonoid fun _: ?m.312671_ => AddMonoidHom.id: (M : Type ?u.312673) → [inst : AddZeroClass M] → M →+ MAddMonoidHom.id M: Type vM
invFun := of: {ι : Type ?u.321290} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.321289) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof (fun _: ?m.321294_ => M: Type vM) default: {α : Sort ?u.321299} → [self : Inhabited α] → αdefault
left_inv := fun x: ?m.330297x =>
DirectSum.induction_on: ∀ {ι : Type ?u.330300} [dec_ι : DecidableEq ι] {β : ι → Type ?u.330299} [inst : (i : ι) → AddCommMonoid (β i)]
{C : (DirectSum ι fun i => β i) → Prop} (x : DirectSum ι fun i => β i),
{γ : Type ?u.332497} [inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
right_inv := fun x: ?m.330583x => toAddMonoid_of: ∀ {ι : Type ?u.330587} [dec_ι : DecidableEq ι] {β : ι → Type ?u.330586} [inst : (i : ι) → AddCommMonoid (β i)]
{γ : Type ?u.330585} [inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
↑(toAddMonoid φ) (↑(of β i) x) = ↑(φ i) xtoAddMonoid_of _: (i : ?m.330588) → ?m.330590 i →+ ?m.330592_ _: ?m.330588_ _: ?m.330590 ?m.330595_ }
#align direct_sum.id DirectSum.id: (M : Type v) →
(ι : optParam (Type u_1) PUnit) → [inst : AddCommMonoid M] → [inst_1 : Unique ι] → (DirectSum ι fun _x => M) ≃+ MDirectSum.id

section CongrLeft

variable {κ: Type ?u.333815κ : Type _: Type (?u.333784+1)Type _}

/-- Reindexing terms of a direct sum.-/
def equivCongrLeft: (h : ι ≃ κ) → (DirectSum ι fun i => β i) ≃+ DirectSum κ fun k => β (↑h.symm k)equivCongrLeft (h: ι ≃ κh : ι: Type vι ≃ κ: Type ?u.333815κ) : (⨁ i: ?m.333828i, β: ι → Type wβ i: ?m.333828i) ≃+ ⨁ k: ?m.333865k, β: ι → Type wβ (h: ι ≃ κh.symm: {α : Sort ?u.333868} → {β : Sort ?u.333867} → α ≃ β → β ≃ αsymm k: ?m.333865k) :=
{ Dfinsupp.equivCongrLeft: {ι : Type ?u.335577} →
{β : ι → Type ?u.335576} →
{κ : Type ?u.335575} →
[inst : (i : ι) → Zero (β i)] → (h : ι ≃ κ) → (Dfinsupp fun i => β i) ≃ Dfinsupp fun k => β (↑h.symm k)Dfinsupp.equivCongrLeft h: ι ≃ κh with map_add' := Dfinsupp.comapDomain'_add: ∀ {ι : Type ?u.336839} {β : ι → Type ?u.336838} {κ : Type ?u.336840} [inst : (i : ι) → AddZeroClass (β i)] (h : κ → ι)
{h' : ι → κ} (hh' : Function.LeftInverse h' h) (f g : Dfinsupp fun i => β i),
Dfinsupp.comapDomain' h hh' (f + g) = Dfinsupp.comapDomain' h hh' f + Dfinsupp.comapDomain' h hh' gDfinsupp.comapDomain'_add _: ?m.336843 → ?m.336841_ h: ι ≃ κh.right_inv: ∀ {α : Sort ?u.336848} {β : Sort ?u.336847} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv}
#align direct_sum.equiv_congr_left DirectSum.equivCongrLeft: {ι : Type v} →
{β : ι → Type w} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{κ : Type u_1} → (h : ι ≃ κ) → (DirectSum ι fun i => β i) ≃+ DirectSum κ fun k => β (↑h.symm k)DirectSum.equivCongrLeft

@[simp]
theorem equivCongrLeft_apply: ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι ≃ κ)
(f : DirectSum ι fun i => β i) (k : κ), ↑(↑(equivCongrLeft h) f) k = ↑f (↑h.symm k)equivCongrLeft_apply (h: ι ≃ κh : ι: Type vι ≃ κ: Type ?u.339448κ) (f: DirectSum ?m.339457 fun i => β if : ⨁ i: ?m.339459i, β: ι → Type wβ i: ?m.339459i) (k: κk : κ: Type ?u.339448κ) :
equivCongrLeft: {ι : Type ?u.339499} →
{β : ι → Type ?u.339498} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{κ : Type ?u.339497} → (h : ι ≃ κ) → (DirectSum ι fun i => β i) ≃+ DirectSum κ fun k => β (↑h.symm k)equivCongrLeft h: ι ≃ κh f: DirectSum ?m.339457 fun i => β if k: κk = f: DirectSum ?m.339457 fun i => β if (h: ι ≃ κh.symm: {α : Sort ?u.339784} → {β : Sort ?u.339783} → α ≃ β → β ≃ αsymm k: κk) := byGoals accomplished! 🐙
ι: Type vdec_ι: DecidableEq ιβ: ι → Type winst✝¹: (i : ι) → AddCommMonoid (β i)γ: Type u₁inst✝: AddCommMonoid γκ: Type u_1h: ι ≃ κf: DirectSum ι fun i => β ik: κ↑(↑(equivCongrLeft h) f) k = ↑f (↑h.symm k)exact Dfinsupp.comapDomain'_apply: ∀ {ι : Type ?u.339896} {β : ι → Type ?u.339895} {κ : Type ?u.339897} [inst : (i : ι) → Zero (β i)] (h : κ → ι)
{h' : ι → κ} (hh' : Function.LeftInverse h' h) (f : Dfinsupp fun i => β i) (k : κ),
↑(Dfinsupp.comapDomain' h hh' f) k = ↑f (h k)Dfinsupp.comapDomain'_apply _: ?m.339900 → ?m.339898_ h: ι ≃ κh.right_inv: ∀ {α : Sort ?u.339905} {β : Sort ?u.339904} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv _: Dfinsupp fun i => ?m.339899 i_ _: ?m.339900_Goals accomplished! 🐙
#align direct_sum.equiv_congr_left_apply DirectSum.equivCongrLeft_apply: ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι ≃ κ)
(f : DirectSum ι fun i => β i) (k : κ), ↑(↑(equivCongrLeft h) f) k = ↑f (↑h.symm k)DirectSum.equivCongrLeft_apply

end CongrLeft

section Option

variable {α: Option ι → Type wα : Option: Type ?u.341450 → Type ?u.341450Option ι: Type vι → Type w: Type (w+1)Type w} [∀ i: ?m.341414i, AddCommMonoid: Type ?u.341417 → Type ?u.341417AddCommMonoid (α: Option ι → Type wα i: ?m.341414i)]

-- Porting note: commented out
-- include dec_ι

/-- Isomorphism obtained by separating the term of index `none` of a direct sum over `Option ι`.-/
@[simps: ∀ {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ι → Type w} [inst : (i : Option ι) → AddCommMonoid (α i)]
(a : (fun i => α i) none × Dfinsupp fun i => (fun i => α i) (some i)),
noncomputable def addEquivProdDirectSum: (DirectSum (Option ι) fun i => α i) ≃+ α none × DirectSum ι fun i => α (some i)addEquivProdDirectSum : (⨁ i: ?m.341468i, α: Option ι → Type wα i: ?m.341468i) ≃+ α: Option ι → Type wα none: {α : Type ?u.341503} → Option αnone × ⨁ i: ?m.341510i, α: Option ι → Type wα (some: {α : Type ?u.341512} → α → Option αsome i: ?m.341510i) :=
{ Dfinsupp.equivProdDfinsupp: {ι : Type ?u.343394} →
[dec : DecidableEq ι] →
{α : Option ι → Type ?u.343393} →
[inst : (i : Option ι) → Zero (α i)] → (Dfinsupp fun i => α i) ≃ α none × Dfinsupp fun i => α (some i)Dfinsupp.equivProdDfinsupp with map_add' := Dfinsupp.equivProdDfinsupp_add: ∀ {ι : Type ?u.344873} [dec : DecidableEq ι] {α : Option ι → Type ?u.344872}
[inst : (i : Option ι) → AddZeroClass (α i)] (f g : Dfinsupp fun i => α i),
↑Dfinsupp.equivProdDfinsupp (f + g) = ↑Dfinsupp.equivProdDfinsupp f + ↑Dfinsupp.equivProdDfinsupp gDfinsupp.equivProdDfinsupp_add }
[dec_ι : DecidableEq ι] →
{α : Option ι → Type w} →
[inst : (i : Option ι) → AddCommMonoid (α i)] →
(DirectSum (Option ι) fun i => α i) ≃+ α none × DirectSum ι fun i => α (some i)DirectSum.addEquivProdDirectSum

end Option

section Sigma

variable {α: ι → Type uα : ι: Type vι → Type u: Type (u+1)Type u} {δ: (i : ι) → α i → Type wδ : ∀ i: ?m.347670i, α: ι → Type uα i: ?m.347670i → Type w: Type (w+1)Type w} [∀ i: ?m.347678i j: ?m.347681j, AddCommMonoid: Type ?u.347684 → Type ?u.347684AddCommMonoid (δ: (i : ι) → α i → Type wδ i: ?m.347730i j: ?m.347681j)]

/-- The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`.-/
noncomputable def sigmaCurry: {ι : Type v} →
{α : ι → Type u} →
{δ : (i : ι) → α i → Type w} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
(DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) →+ DirectSum ι fun i => DirectSum (α i) fun j => δ i jsigmaCurry : (⨁ i: (_i : ?m.347749) × ?m.347754 _ii : Σ _i: ?m.347751_i, _: Type ?u.347747_, δ: (i : ι) → α i → Type wδ i: (_i : ?m.347749) × ?m.347754 _ii.1: {α : Type ?u.347758} → {β : α → Type ?u.347757} → Sigma β → α1 i: (_i : ?m.347749) × ?m.347754 _ii.2: {α : Type ?u.347768} → {β : α → Type ?u.347767} → (self : Sigma β) → β self.fst2) →+ ⨁ (i: ?m.347827i) (j: ?m.347833j), δ: (i : ι) → α i → Type wδ i: ?m.347827i j: ?m.347833j
where
toFun := @Dfinsupp.sigmaCurry: {ι : Type ?u.351683} →
{α : ι → Type ?u.351681} →
{δ : (i : ι) → α i → Type ?u.351682} →
[inst : (i : ι) → (j : α i) → Zero (δ i j)] →
(Dfinsupp fun i => δ i.fst i.snd) → Dfinsupp fun i => Dfinsupp fun j => δ i jDfinsupp.sigmaCurry _: Type ?u.351683_ _: ?m.351684 → Type ?u.351681_ δ: (i : ι) → α i → Type wδ _
map_zero' := Dfinsupp.sigmaCurry_zero: ∀ {ι : Type ?u.353629} {α : ι → Type ?u.353630} {δ : (i : ι) → α i → Type ?u.353628}
[inst : (i : ι) → (j : α i) → Zero (δ i j)], Dfinsupp.sigmaCurry 0 = 0Dfinsupp.sigmaCurry_zero
map_add' f: ?m.354006f g: ?m.354009g := @Dfinsupp.sigmaCurry_add: ∀ {ι : Type ?u.354012} {α : ι → Type ?u.354013} {δ : (i : ι) → α i → Type ?u.354011}
[inst : (i : ι) → (j : α i) → AddZeroClass (δ i j)] (f g : Dfinsupp fun i => δ i.fst i.snd),
Dfinsupp.sigmaCurry (f + g) = Dfinsupp.sigmaCurry f + Dfinsupp.sigmaCurry gDfinsupp.sigmaCurry_add _: Type ?u.354012_ _: ?m.354014 → Type ?u.354013_ δ: (i : ι) → α i → Type wδ _ f: ?m.354006f g: ?m.354009g
#align direct_sum.sigma_curry DirectSum.sigmaCurry: {ι : Type v} →
{α : ι → Type u} →
{δ : (i : ι) → α i → Type w} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
(DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) →+ DirectSum ι fun i => DirectSum (α i) fun j => δ i jDirectSum.sigmaCurry

@[simp]
theorem sigmaCurry_apply: ∀ {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)]
(f : DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) (i : ι) (j : α i),
↑(↑(↑sigmaCurry f) i) j = ↑f { fst := i, snd := j }sigmaCurry_apply (f: DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.sndf : ⨁ i: (_i : ?m.357757) × ?m.357762 _ii : Σ _i: ?m.357759_i, _: Type ?u.357755_, δ: (i : ι) → α i → Type wδ i: (_i : ?m.357757) × ?m.357762 _ii.1: {α : Type ?u.357766} → {β : α → Type ?u.357765} → Sigma β → α1 i: (_i : ?m.357757) × ?m.357762 _ii.2: {α : Type ?u.357776} → {β : α → Type ?u.357775} → (self : Sigma β) → β self.fst2) (i: ιi : ι: Type vι) (j: α ij : α: ι → Type uα i: ιi) :
sigmaCurry: {ι : Type ?u.357839} →
{α : ι → Type ?u.357840} →
{δ : (i : ι) → α i → Type ?u.357838} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
(DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) →+ DirectSum ι fun i => DirectSum (α i) fun j => δ i jsigmaCurry f: DirectSum ?m.357753 fun i => δ i.fst i.sndf i: ιi j: α ij = f: DirectSum ?m.357753 fun i => δ i.fst i.sndf ⟨i: ιi, j: α ij⟩ :=
@Dfinsupp.sigmaCurry_apply: ∀ {ι : Type ?u.366676} {α : ι → Type ?u.366677} {δ : (i : ι) → α i → Type ?u.366675}
[inst : (i : ι) → (j : α i) → Zero (δ i j)] (f : Dfinsupp fun i => δ i.fst i.snd) (i : ι) (j : α i),
↑(↑(Dfinsupp.sigmaCurry f) i) j = ↑f { fst := i, snd := j }Dfinsupp.sigmaCurry_apply _: Type ?u.366676_ _: ?m.366678 → Type ?u.366677_ δ: (i : ι) → α i → Type wδ _ _: Dfinsupp fun i => δ i.fst i.snd_ i: ιi j: α ij
#align direct_sum.sigma_curry_apply DirectSum.sigmaCurry_apply: ∀ {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)]
(f : DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) (i : ι) (j : α i),
↑(↑(↑sigmaCurry f) i) j = ↑f { fst := i, snd := j }DirectSum.sigmaCurry_apply

/-- The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
`curry`.-/
def sigmaUncurry: {ι : Type v} →
{α : ι → Type u} →
{δ : (i : ι) → α i → Type w} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
[inst_1 : (i : ι) → DecidableEq (α i)] →
[inst_2 : (i : ι) → (j : α i) → DecidableEq (δ i j)] →
(DirectSum ι fun i => DirectSum (α i) fun j => δ i j) →+ DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.sndsigmaUncurry [∀ i: ?m.369399i, DecidableEq: Sort ?u.369402 → Sort (max1?u.369402)DecidableEq (α: ι → Type uα i: ?m.369399i)] [∀ i: ?m.369415i j: ?m.369418j, DecidableEq: Sort ?u.369421 → Sort (max1?u.369421)DecidableEq (δ: (i : ι) → α i → Type wδ i: ?m.369415i j: ?m.369418j)] :
(⨁ (i: ?m.369442i) (j: ?m.369448j), δ: (i : ι) → α i → Type wδ i: ?m.369442i j: ?m.369448j) →+ ⨁ i: (_i : ?m.369552) × ?m.369557 _ii : Σ _i: ?m.369554_i, _: Type ?u.369550_, δ: (i : ι) → α i → Type wδ i: (_i : ?m.369552) × ?m.369557 _ii.1: {α : Type ?u.369561} → {β : α → Type ?u.369560} → Sigma β → α1 i: (_i : ?m.369552) × ?m.369557 _ii.2: {α : Type ?u.369571} → {β : α → Type ?u.369570} → (self : Sigma β) → β self.fst2
where
toFun := Dfinsupp.sigmaUncurry: {ι : Type ?u.374326} →
{α : ι → Type ?u.374324} →
{δ : (i : ι) → α i → Type ?u.374325} →
[inst : (i : ι) → (j : α i) → Zero (δ i j)] →
[inst_1 : (i : ι) → DecidableEq (α i)] →
[inst_2 : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] →
(Dfinsupp fun i => Dfinsupp fun j => δ i j) → Dfinsupp fun i => δ i.fst i.sndDfinsupp.sigmaUncurry
map_zero' := Dfinsupp.sigmaUncurry_zero: ∀ {ι : Type ?u.376800} {α : ι → Type ?u.376801} {δ : (i : ι) → α i → Type ?u.376799}
[inst : (i : ι) → (j : α i) → Zero (δ i j)] [inst_1 : (i : ι) → DecidableEq (α i)]
[inst_2 : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)], Dfinsupp.sigmaUncurry 0 = 0Dfinsupp.sigmaUncurry_zero
map_add' := Dfinsupp.sigmaUncurry_add: ∀ {ι : Type ?u.377441} {α : ι → Type ?u.377442} {δ : (i : ι) → α i → Type ?u.377440}
[inst : (i : ι) → (j : α i) → AddZeroClass (δ i j)] [inst_1 : (i : ι) → DecidableEq (α i)]
[inst_2 : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] (f g : Dfinsupp fun i => Dfinsupp fun j => δ i j),
Dfinsupp.sigmaUncurry (f + g) = Dfinsupp.sigmaUncurry f + Dfinsupp.sigmaUncurry gDfinsupp.sigmaUncurry_add
#align direct_sum.sigma_uncurry DirectSum.sigmaUncurry: {ι : Type v} →
{α : ι → Type u} →
{δ : (i : ι) → α i → Type w} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
[inst_1 : (i : ι) → DecidableEq (α i)] →
[inst_2 : (i : ι) → (j : α i) → DecidableEq (δ i j)] →
(DirectSum ι fun i => DirectSum (α i) fun j => δ i j) →+ DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.sndDirectSum.sigmaUncurry

@[simp]
theorem sigmaUncurry_apply: ∀ {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)]
[inst_1 : (i : ι) → DecidableEq (α i)] [inst_2 : (i : ι) → (j : α i) → DecidableEq (δ i j)]
(f : DirectSum ι fun i => DirectSum (α i) fun j => δ i j) (i : ι) (j : α i),
↑(↑sigmaUncurry f) { fst := i, snd := j } = ↑(↑f i) jsigmaUncurry_apply [∀ i: ?m.380546i, DecidableEq: Sort ?u.380549 → Sort (max1?u.380549)DecidableEq (α: ι → Type uα i: ?m.380546i)] [∀ i: ?m.380562i j: ?m.380565j, DecidableEq: Sort ?u.380568 → Sort (max1?u.380568)DecidableEq (δ: (i : ι) → α i → Type wδ i: ?m.380562i j: ?m.380565j)]
(f: DirectSum ι fun i => DirectSum (α i) fun j => δ i jf : ⨁ (i: ?m.380587i) (j: ?m.380593j), δ: (i : ι) → α i → Type wδ i: ?m.380587i j: ?m.380593j) (i: ιi : ι: Type vι) (j: α ij : α: ι → Type uα i: ιi) : sigmaUncurry: {ι : Type ?u.380699} →
{α : ι → Type ?u.380700} →
{δ : (i : ι) → α i → Type ?u.380698} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
[inst_1 : (i : ι) → DecidableEq (α i)] →
[inst_2 : (i : ι) → (j : α i) → DecidableEq (δ i j)] →
(DirectSum ι fun i => DirectSum (α i) fun j => δ i j) →+ DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.sndsigmaUncurry f: DirectSum ?m.380585 fun i => DirectSum (α i) fun j => δ i jf ⟨i: ιi, j: α ij⟩ = f: DirectSum ?m.380585 fun i => DirectSum (α i) fun j => δ i jf i: ιi j: α ij :=
Dfinsupp.sigmaUncurry_apply: ∀ {ι : Type ?u.389915} {α : ι → Type ?u.389916} {δ : (i : ι) → α i → Type ?u.389914}
[inst : (i : ι) → (j : α i) → Zero (δ i j)] [inst_1 : (i : ι) → DecidableEq (α i)]
[inst_2 : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] (f : Dfinsupp fun i => Dfinsupp fun j => δ i j)
(i : ι) (j : α i), ↑(Dfinsupp.sigmaUncurry f) { fst := i, snd := j } = ↑(↑f i) jDfinsupp.sigmaUncurry_apply f: DirectSum ι fun i => DirectSum (α i) fun j => δ i jf i: ιi j: α ij
#align direct_sum.sigma_uncurry_apply DirectSum.sigmaUncurry_apply: ∀ {ι : Type v} {α : ι → Type u} {δ : (i : ι) → α i → Type w} [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)]
[inst_1 : (i : ι) → DecidableEq (α i)] [inst_2 : (i : ι) → (j : α i) → DecidableEq (δ i j)]
(f : DirectSum ι fun i => DirectSum (α i) fun j => δ i j) (i : ι) (j : α i),
↑(↑sigmaUncurry f) { fst := i, snd := j } = ↑(↑f i) jDirectSum.sigmaUncurry_apply

/-- The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`.-/
noncomputable def sigmaCurryEquiv: {ι : Type v} →
{α : ι → Type u} →
{δ : (i : ι) → α i → Type w} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
[inst_1 : (i : ι) → DecidableEq (α i)] →
[inst_2 : (i : ι) → (j : α i) → DecidableEq (δ i j)] →
(DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) ≃+ DirectSum ι fun i => DirectSum (α i) fun j => δ i jsigmaCurryEquiv [∀ i: ?m.392298i, DecidableEq: Sort ?u.392301 → Sort (max1?u.392301)DecidableEq (α: ι → Type uα i: ?m.392298i)] [∀ i: ?m.392314i j: ?m.392317j, DecidableEq: Sort ?u.392320 → Sort (max1?u.392320)DecidableEq (δ: (i : ι) → α i → Type wδ i: ?m.392314i j: ?m.392317j)] :
(⨁ i: (_i : ?m.392343) × ?m.392348 _ii : Σ _i: ?m.392345_i, _: Type ?u.392341_, δ: (i : ι) → α i → Type wδ i: (_i : ?m.392343) × ?m.392348 _ii.1: {α : Type ?u.392352} → {β : α → Type ?u.392351} → Sigma β → α1 i: (_i : ?m.392343) × ?m.392348 _ii.2: {α : Type ?u.392362} → {β : α → Type ?u.392361} → (self : Sigma β) → β self.fst2) ≃+ ⨁ (i: ?m.392421i) (j: ?m.392427j), δ: (i : ι) → α i → Type wδ i: ?m.392421i j: ?m.392427j :=
{ sigmaCurry, Dfinsupp.sigmaCurryEquiv with }: ?m.395252 ≃+ ?m.395253{ sigmaCurry: {ι : Type ?u.394521} →
{α : ι → Type ?u.394522} →
{δ : (i : ι) → α i → Type ?u.394520} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
(DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) →+ DirectSum ι fun i => DirectSum (α i) fun j => δ i jsigmaCurry{ sigmaCurry, Dfinsupp.sigmaCurryEquiv with }: ?m.395252 ≃+ ?m.395253, Dfinsupp.sigmaCurryEquiv: {ι : Type ?u.394629} →
{α : ι → Type ?u.394627} →
{δ : (i : ι) → α i → Type ?u.394628} →
[inst : (i : ι) → (j : α i) → Zero (δ i j)] →
[inst_1 : (i : ι) → DecidableEq (α i)] →
[inst_2 : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] →
(Dfinsupp fun i => δ i.fst i.snd) ≃ Dfinsupp fun i => Dfinsupp fun j => δ i jDfinsupp.sigmaCurryEquiv{ sigmaCurry, Dfinsupp.sigmaCurryEquiv with }: ?m.395252 ≃+ ?m.395253 { sigmaCurry, Dfinsupp.sigmaCurryEquiv with }: ?m.395252 ≃+ ?m.395253with{ sigmaCurry, Dfinsupp.sigmaCurryEquiv with }: ?m.395252 ≃+ ?m.395253 }
#align direct_sum.sigma_curry_equiv DirectSum.sigmaCurryEquiv: {ι : Type v} →
{α : ι → Type u} →
{δ : (i : ι) → α i → Type w} →
[inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
[inst_1 : (i : ι) → DecidableEq (α i)] →
[inst_2 : (i : ι) → (j : α i) → DecidableEq (δ i j)] →
(DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) ≃+ DirectSum ι fun i => DirectSum (α i) fun j => δ i jDirectSum.sigmaCurryEquiv

end Sigma

/-- The canonical embedding from `⨁ i, A i` to `M` where `A` is a collection of `AddSubmonoid M`
indexed by `ι`.

When `S = Submodule _ M`, this is available as a `LinearMap`, `DirectSum.coe_linearMap`. -/
protected def coeAddMonoidHom: {ι : Type v} →
{M : Type u_1} →
{S : Type u_2} →
[inst : DecidableEq ι] →
[inst_1 : SetLike S M] →
[inst_2 : AddSubmonoidClass S M] → (A : ι → S) → (DirectSum ι fun i => { x // x ∈ A i }) →+ McoeAddMonoidHom {M: Type ?u.405588M S: Type ?u.405591S : Type _: Type (?u.405588+1)Type _} [DecidableEq: Sort ?u.405594 → Sort (max1?u.405594)DecidableEq ι: Type vι] [AddCommMonoid: Type ?u.405603 → Type ?u.405603AddCommMonoid M: Type ?u.405588M] [SetLike: Type ?u.405607 → outParam (Type ?u.405606) → Type (max?u.405607?u.405606)SetLike S: Type ?u.405591S M: Type ?u.405588M]
[AddSubmonoidClass: (S : Type ?u.405611) → (M : Type ?u.405610) → [inst : AddZeroClass M] → [inst : SetLike S M] → PropAddSubmonoidClass S: Type ?u.405591S M: Type ?u.405588M] (A: ι → SA : ι: Type vι → S: Type ?u.405591S) : (⨁ i: ?m.406042i, A: ι → SA i: ?m.406042i) →+ M: Type ?u.405588M :=
toAddMonoid: {ι : Type ?u.408698} →
[dec_ι : DecidableEq ι] →
{β : ι → Type ?u.408697} →
[inst : (i : ι) → AddCommMonoid (β i)] →
{γ : Type ?u.408696} → [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γtoAddMonoid fun i: ?m.408896i => AddSubmonoidClass.Subtype: {M : Type ?u.408899} →
{A : Type ?u.408898} → [inst_1 : SetLike A M] → [hA : AddSubmonoidClass A M] → (S' : A) → { x // x ∈ S' } →+ MAddSubmonoidClass.Subtype (A: ι → SA i: ?m.408896i)
{M : Type u_1} →
{S : Type u_2} →
[inst : DecidableEq ι] →
[inst_1 : SetLike S M] →
[inst_2 : AddSubmonoidClass S M] → (A : ι → S) → (DirectSum ι fun i => { x // x ∈ A i }) →+ MDirectSum.coeAddMonoidHom

@[simp]
theorem coeAddMonoidHom_of: ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike S M]
[inst_3 : AddSubmonoidClass S M] (A : ι → S) (i : ι) (x : { x // x ∈ A i }),
↑(DirectSum.coeAddMonoidHom A) (↑(of (fun i => { x // x ∈ A i }) i) x) = ↑xcoeAddMonoidHom_of {M: Type ?u.410729M S: Type ?u.410732S : Type _: Type (?u.410732+1)Type _} [DecidableEq: Sort ?u.410735 → Sort (max1?u.410735)DecidableEq ι: Type vι] [AddCommMonoid: Type ?u.410744 → Type ?u.410744AddCommMonoid M: Type ?u.410729M] [SetLike: Type ?u.410748 → outParam (Type ?u.410747) → Type (max?u.410748?u.410747)SetLike S: Type ?u.410732S M: Type ?u.410729M]
[AddSubmonoidClass: (S : Type ?u.410752) → (M : Type ?u.410751) → [inst : AddZeroClass M] → [inst : SetLike S M] → PropAddSubmonoidClass S: Type ?u.410732S M: Type ?u.410729M] (A: ι → SA : ι: Type vι → S: Type ?u.410732S) (i: ιi : ι: Type vι) (x: { x // x ∈ A i }x : A: ι → SA i: ιi) :
DirectSum.coeAddMonoidHom: {ι : Type ?u.411207} →
{M : Type ?u.411206} →
{S : Type ?u.411205} →
[inst : DecidableEq ι] →
[inst_1 : SetLike S M] →
[inst_2 : AddSubmonoidClass S M] → (A : ι → S) → (DirectSum ι fun i => { x // x ∈ A i }) →+ MDirectSum.coeAddMonoidHom A: ι → SA (of: {ι : Type ?u.419758} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.419757) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof (fun i: ?m.419762i => A: ι → SA i: ?m.419762i) i: ιi x: { x // x ∈ A i }x) = x: { x // x ∈ A i }x :=
toAddMonoid_of: ∀ {ι : Type ?u.429983} [dec_ι : DecidableEq ι] {β : ι → Type ?u.429982} [inst : (i : ι) → AddCommMonoid (β i)]
{γ : Type ?u.429981} [inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
↑(toAddMonoid φ) (↑(of β i) x) = ↑(φ i) xtoAddMonoid_of _: (i : ?m.429984) → ?m.429986 i →+ ?m.429988_ _: ?m.429984_ _: ?m.429986 ?m.429991_
#align direct_sum.coe_add_monoid_hom_of DirectSum.coeAddMonoidHom_of: ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike S M]
[inst_3 : AddSubmonoidClass S M] (A : ι → S) (i : ι) (x : { x // x ∈ A i }),
↑(DirectSum.coeAddMonoidHom A) (↑(of (fun i => { x // x ∈ A i }) i) x) = ↑xDirectSum.coeAddMonoidHom_of

theorem coe_of_apply: ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike S M]
[inst_3 : AddSubmonoidClass S M] {A : ι → S} (i j : ι) (x : { x // x ∈ A i }),
↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)coe_of_apply {M: Type u_1M S: Type u_2S : Type _: Type (?u.431776+1)Type _} [DecidableEq: Sort ?u.431779 → Sort (max1?u.431779)DecidableEq ι: Type vι] [AddCommMonoid: Type ?u.431788 → Type ?u.431788AddCommMonoid M: Type ?u.431773M] [SetLike: Type ?u.431792 → outParam (Type ?u.431791) → Type (max?u.431792?u.431791)SetLike S: Type ?u.431776S M: Type ?u.431773M]
[AddSubmonoidClass: (S : Type ?u.431796) → (M : Type ?u.431795) → [inst : AddZeroClass M] → [inst : SetLike S M] → PropAddSubmonoidClass S: Type ?u.431776S M: Type ?u.431773M] {A: ι → SA : ι: Type vι → S: Type ?u.431776S} (i: ιi j: ιj : ι: Type vι) (x: { x // x ∈ A i }x : A: ι → SA i: ιi) :
(of: {ι : Type ?u.432253} →
[dec_ι : DecidableEq ι] →
(β : ι → Type ?u.432252) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β iof (fun i: ?m.432257i ↦ {x: ?m.432262x // x: ?m.432262x ∈ A: ι → SA i: ?m.432257i}) i: ιi x: { x // x ∈ A i }x j: ιj : M: Type ?u.431773M) = if i: ιi = j: ιj then x: { x // x ∈ A i }x else 0: ?m.4424730 := byGoals accomplished! 🐙