/-
Copyright (c) 2019 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.33
i, AddCommMonoid: Type ?u.36 → Type ?u.36
AddCommMonoid (β: ι → Type w
β i: ?m.33
i)] : Type _: Type (?u.40+1)
Type _ :=
  -- Porting note: Failed to synthesize
  -- Π₀ i, β i deriving AddCommMonoid, Inhabited
  Π₀ i: ?m.47
i, β: ι → Type w
β i: ?m.47
i
#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.1313
i, AddCommMonoid: Type ?u.1316 → Type ?u.1316
AddCommMonoid (β: ι → Type w
β i: ?m.1313
i)] : 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.1362
i, β: ι → Type w
β i: ?m.1362
i))

-- Porting note: Added addCommMonoid instance manually
instance: (ι : Type v) → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → AddCommMonoid (DirectSum ι β)
instance [∀ i: ?m.2864
i, AddCommMonoid: Type ?u.2867 → Type ?u.2867
AddCommMonoid (β: ι → Type w
β i: ?m.2864
i)] : AddCommMonoid: Type ?u.2871 → Type ?u.2871
AddCommMonoid (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.2908
AddCommMonoid (Π₀ i: ?m.2913
i, β: ι → Type w
β i: ?m.2913
i))

instance: (ι : Type v) → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → CoeFun (DirectSum ι β) fun x => (i : ι) → β i
instance [∀ i: ?m.4297
i, AddCommMonoid: Type ?u.4300 → Type ?u.4300
AddCommMonoid (β: ι → Type w
β i: ?m.4297
i)] : 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.4365
i, β: ι → Type w
β i: ?m.4365
i) 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.5920
r:(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
ι}

section AddCommGroup

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

instance: {ι : Type v} → (β : ι → Type w) → [inst : (i : ι) → AddCommGroup (β i)] → AddCommGroup (DirectSum ι β)
instance : AddCommGroup: Type ?u.8796 → Type ?u.8796
AddCommGroup (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.9614
AddCommGroup (Π₀ i: ?m.9619
i, β: ι → Type w
β i: ?m.9619
i))
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₂ i
sub_apply (g₁: DirectSum ι fun i => β i
g₁ g₂: DirectSum ?m.11453 fun i => β i
g₂ : ⨁ i: ?m.10634
i, β: ι → Type w
β i: ?m.10634
i) (i: ι
i : ι: Type v
ι) : (g₁: DirectSum ?m.10632 fun i => β i
g₁ - g₂: DirectSum ?m.11453 fun i => β i
g₂) i: ι
i = g₁: DirectSum ?m.10632 fun i => β i
g₁ i: ι
i - g₂: DirectSum ?m.11453 fun i => β i
g₂ i: ι
i :=
  rfl: ∀ {α : Sort ?u.12172} {a : α}, a = a
rfl
#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₂ i
DirectSum.sub_apply

end AddCommGroup

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

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

variable {β: ?m.13927
β}

@[simp]
theorem add_apply: ∀ (g₁ g₂ : DirectSum ι fun i => β i) (i : ι), ↑(g₁ + g₂) i = ↑g₁ i + ↑g₂ i
add_apply (g₁: DirectSum ?m.13955 fun i => β i
g₁ g₂: DirectSum ι fun i => β i
g₂ : ⨁ i: ?m.13995
i, β: ι → Type w
β i: ?m.13957
i) (i: ι
i : ι: Type v
ι) : (g₁: DirectSum ?m.13955 fun i => β i
g₁ + g₂: DirectSum ?m.13993 fun i => β i
g₂) i: ι
i = g₁: DirectSum ?m.13955 fun i => β i
g₁ i: ι
i + g₂: DirectSum ?m.13993 fun i => β i
g₂ i: ι
i :=
  rfl: ∀ {α : Sort ?u.16125} {a : α}, a = a
rfl
#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₂ i
DirectSum.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 => β i
mk (s: Finset ι
s : Finset: Type ?u.16239 → Type ?u.16239
Finset ι: Type v
ι) : (∀ i: ↑↑s
i : (↑s: Finset ι
s : Set: Type ?u.16246 → Type ?u.16246
Set ι: Type v
ι), β: ι → Type w
β i: ↑↑s
i.1: {α : Sort ?u.16367} → {p : α → Prop} → Subtype p → α
1) →+ ⨁ i: ?m.16380
i, β: ι → Type w
β i: ?m.16380
i
    where
  toFun := Dfinsupp.mk: {ι : Type ?u.20834} →
  {β : ι → Type ?u.20833} →
    [dec : DecidableEq ι] → [inst : (i : ι) → Zero (β i)] → (s : Finset ι) → ((i : ↑↑s) → β ↑i) → Dfinsupp fun i => β i
Dfinsupp.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 y
Dfinsupp.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 = 0
Dfinsupp.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 => β i
DirectSum.mk

/-- `of i` is the natural inclusion map from `β i` to `⨁ i, β i`. -/
def of: (i : ι) → β i →+ DirectSum ι fun i => β i
of (i: ι
i : ι: Type v
ι) : β: ι → Type w
β i: ι
i →+ ⨁ i: ?m.23720
i, β: ι → Type w
β i: ?m.23720
i :=
  Dfinsupp.singleAddHom: {ι : Type ?u.24863} →
  (β : ι → Type ?u.24862) →
    [dec : DecidableEq ι] → [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → β i →+ Dfinsupp fun i => β i
Dfinsupp.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 => β i
DirectSum.of

@[simp]
theorem of_eq_same: ∀ {ι : Type v} [dec_ι : DecidableEq ι] (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] (i : ι) (x : β i),
  ↑(↑(of β i) x) i = x
of_eq_same (i: ι
i : ι: Type v
ι) (x: β i
x : β: ι → Type w
β i: ι
i) : (of: {ι : Type ?u.25964} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.25963) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?m.25965 → Type ?u.25963
_ i: ι
i x: β i
x) i: ι
i = x: β i
x :=
  Dfinsupp.single_eq_same: ∀ {ι : Type ?u.34582} {β : ι → Type ?u.34581} [dec : DecidableEq ι] [inst : (i : ι) → Zero (β i)] {i : ι} {b : β i},
  ↑(Dfinsupp.single i b) i = b
Dfinsupp.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 = x
DirectSum.of_eq_same

theorem of_eq_of_ne: ∀ (i j : ι) (x : β i), i ≠ j → ↑(↑(of β i) x) j = 0
of_eq_of_ne (i: ι
i j: ι
j : ι: Type v
ι) (x: β i
x : β: ι → Type w
β i: ι
i) (h: i ≠ j
h : i: ι
i ≠ j: ι
j) : (of: {ι : Type ?u.36186} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.36185) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?m.36187 → Type ?u.36185
_ i: ι
i x: β i
x) j: ι
j = 0: ?m.44798
0 :=
  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' = 0
Dfinsupp.single_eq_of_ne h: i ≠ j
h
#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 = 0
DirectSum.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: β i
x : β: ι → Type w
β i: ι
i), Decidable: Prop → Type
Decidable (x: β i
x ≠ 0: ?m.46846
0)] : (0: ?m.47473
0 : ⨁ i: ?m.47443
i, β: ι → Type w
β i: ?m.47443
i).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: β i
x : β: ι → Type w
β i: ι
i), Decidable: Prop → Type
Decidable (x: β i
x ≠ 0: ?m.51189
0)] (i: ι
i : ι: Type v
ι) (x: β i
x : β: ι → Type w
β i: ι
i) (h: x ≠ 0
h : x: β i
x ≠ 0: ?m.51787
0) :
    (of: {ι : Type ?u.52250} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.52249) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?m.52251 → Type ?u.52249
_ i: ι
i x: β i
x).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 ≠ 0
h
#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: β i
x : β: ι → Type w
β i: ι
i), Decidable: Prop → Type
Decidable (x: β i
x ≠ 0: ?m.63736
0)] {i: ι
i : ι: Type v
ι} {b: β i
b : β: ι → Type w
β i: ι
i} :
    (of: {ι : Type ?u.64342} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.64341) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?m.64343 → Type ?u.64341
_ i: ι
i b: β i
b).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) = x
sum_support_of [∀ (i: ι
i : ι: Type v
ι) (x: β i
x : β: ι → Type w
β i: ι
i), Decidable: Prop → Type
Decidable (x: β i
x ≠ 0: ?m.75694
0)] (x: DirectSum ι fun i => β i
x : ⨁ i: ?m.76289
i, β: ι → Type w
β i: ?m.76289
i) :
    (∑ i: ?m.77564
i in x: DirectSum ?m.76287 fun i => β i
x.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 => β i
of β: ι → Type w
β i: ?m.77564
i (x: DirectSum ?m.76287 fun i => β i
x i: ?m.77564
i)) = x: DirectSum ?m.76287 fun i => β i
x :=
  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 = f
Dfinsupp.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) = x
DirectSum.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.86848
Finset ι: Type v
ι) : Function.Injective: {α : Sort ?u.86852} → {β : Sort ?u.86851} → (α → β) → Prop
Function.Injective (mk: {ι : Type ?u.86856} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.86855) →
      [inst : (i : ι) → AddCommMonoid (β i)] → (s : Finset ι) → ((i : ↑↑s) → β ↑i) →+ DirectSum ι fun i => β i
mk β: ι → 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} → (α → β) → Prop
Function.Injective (of: {ι : Type ?u.96833} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.96832) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of β: ι → 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 x
induction_on {C: (DirectSum ?m.106872 fun i => β i) → Prop
C : (⨁ i: ?m.106874
i, β: ι → Type w
β i: ?m.106874
i) → Prop: Type
Prop} (x: DirectSum ?m.106911 fun i => β i
x : ⨁ i: ?m.106913
i, β: ι → Type w
β i: ?m.106913
i) (H_zero: C 0
H_zero : C: (DirectSum ?m.106872 fun i => β i) → Prop
C 0: ?m.106925
0)
    (H_basic: ∀ (i : ι) (x : β i), C (↑(of β i) x)
H_basic : ∀ (i: ι
i : ι: Type v
ι) (x: β i
x : β: ι → Type w
β i: ι
i), C: (DirectSum ?m.106872 fun i => β i) → Prop
C (of: {ι : Type ?u.107841} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.107840) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of β: ι → Type w
β i: ι
i x: β i
x))
    (H_plus: ∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)
H_plus : ∀ x: ?m.116348
x y: ?m.116351
y, C: (DirectSum ?m.106872 fun i => β i) → Prop
C x: ?m.116348
x → C: (DirectSum ?m.106872 fun i => β i) → Prop
C y: ?m.116351
y → C: (DirectSum ?m.106872 fun i => β i) → Prop
C (x: ?m.116348
x + y: ?m.116351
y)) : C: (DirectSum ?m.106872 fun i => β i) → Prop
C x: DirectSum ?m.106911 fun i => β i
x := by
Goals accomplished! 🐙
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝: (i : ι) → AddCommMonoid (β i)

C: (DirectSum ι fun i => β i) → Prop

x: DirectSum ι fun i => β i

H_zero: C 0

H_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 f
Dfinsupp.induction x: DirectSum ι fun i => β i
x H_zero: C 0
H_zeroι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝: (i : ι) → AddCommMonoid (β i)

C: (DirectSum ι fun i => β i) → Prop

x: DirectSum ι fun i => β i

H_zero: C 0

H_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 v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝: (i : ι) → AddCommMonoid (β i)

C: (DirectSum ι fun i => β i) → Prop

x: DirectSum ι fun i => β i

H_zero: C 0

H_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: β i
b f: Dfinsupp fun i => (fun i => β i) i
f h1: ↑f i = 0
h1 h2: b ≠ 0
h2 ih: C f
ihι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝: (i : ι) → AddCommMonoid (β i)

C: (DirectSum ι fun i => β i) → Prop

x: DirectSum ι fun i => β i

H_zero: C 0

H_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: β i

f: Dfinsupp fun i => (fun i => β i) i

h1: ↑f i = 0

h2: b ≠ 0

ih: C f

C (Dfinsupp.single i b + f)
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝: (i : ι) → AddCommMonoid (β i)

C: (DirectSum ι fun i => β i) → Prop

x: DirectSum ι fun i => β i

H_zero: C 0

H_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_elim
Goals 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 x
DirectSum.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 = g
addHom_ext {γ: Type u_1
γ : Type _: Type (?u.118528+1)
Type _} [AddMonoid: Type ?u.118531 → Type ?u.118531
AddMonoid γ: Type ?u.118528
γ] ⦃f: (DirectSum ?m.118538 fun i => β i) →+ γ
f g: (DirectSum ?m.119327 fun i => β i) →+ γ
g : (⨁ i: ?m.118540
i, β: ι → Type w
β i: ?m.119329
i) →+ γ: Type ?u.118528
γ⦄
    (H: ∀ (i : ι) (y : β i), ↑f (↑(of β i) y) = ↑g (↑(of β i) y)
H : ∀ (i: ι
i : ι: Type v
ι) (y: β i
y : β: ι → 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 => β i
of _: ?m.127785 → Type ?u.127783
_ i: ι
i y: β i
y) = 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 => β i
of _: ?m.144742 → Type ?u.144740
_ i: ι
i y: β i
y)) : 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 = g
Dfinsupp.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 = g
DirectSum.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 = g
addHom_ext' {γ: Type ?u.154744
γ : Type _: Type (?u.154744+1)
Type _} [AddMonoid: Type ?u.154747 → Type ?u.154747
AddMonoid γ: Type ?u.154744
γ] ⦃f: (DirectSum ?m.154754 fun i => β i) →+ γ
f g: (DirectSum ?m.155543 fun i => β i) →+ γ
g : (⨁ i: ?m.154756
i, β: ι → Type w
β i: ?m.154756
i) →+ γ: 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 →+ P
comp (of: {ι : Type ?u.155585} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.155584) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?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 →+ P
comp (of: {ι : Type ?u.156440} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.156439) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?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 = g
addHom_ext fun i: ?m.156705
i => 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 x
FunLike.congr_fun <| H: ∀ (i : ι), AddMonoidHom.comp f (of (fun i => β i) i) = AddMonoidHom.comp g (of (fun i => β i) i)
H i: ?m.156705
i
#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 = g
DirectSum.addHom_ext'

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

section ToAddMonoid

variable (φ: (i : ι) → β i →+ γ
φ : ∀ i: ?m.171386
i, β: ι → Type w
β i: ?m.167171
i →+ γ: Type u₁
γ) (ψ: (DirectSum ?m.168006 fun i => β i) →+ γ
ψ : (⨁ i: ?m.168008
i, β: ι → Type w
β i: ?m.166411
i) →+ γ: 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.168745
i, β: ι → Type w
β i: ?m.168745
i) →+ γ: 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 →+ γ
φ
#align direct_sum.to_add_monoid DirectSum.toAddMonoid: {ι : Type v} →
  [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) x
toAddMonoid_of (i: ι
i) (x: β i
x : β: ι → Type w
β i: ?m.172954
i) : 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 => β i
of β: ι → Type w
β i: ?m.172954
i x: β i
x) = φ: (i : ι) → β i →+ γ
φ i: ?m.172954
i x: β i
x :=
  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) x
Dfinsupp.liftAddHom_apply_single φ: (i : ι) → β i →+ γ
φ i: ι
i x: β i
x
#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) x
DirectSum.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)) f
toAddMonoid.unique (f: DirectSum ?m.201131 fun i => β i
f : ⨁ i: ?m.201133
i, β: ι → Type w
β i: ?m.201133
i) : ψ: (DirectSum ?m.200396 fun i => β i) →+ γ
ψ f: DirectSum ?m.201131 fun i => β i
f = 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.209614
i => ψ: (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 →+ P
comp (of: {ι : Type ?u.210815} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.210814) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of β: ι → Type w
β i: ?m.209614
i)) f: DirectSum ?m.201131 fun i => β i
f := by
Goals accomplished! 🐙
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (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 v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

φ: (i : ι) → β i →+ γ

ψ: (DirectSum ι fun i => β i) →+ γ

f: DirectSum ι fun i => β i

e_aψ = toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)
  -- Porting note: ext applied unsuitable ext lemma
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (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 = g
Dfinsupp.addHom_ext'ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

φ: (i : ι) → β i →+ γ

ψ: (DirectSum ι fun i => β i) →+ γ

f: DirectSum ι fun i => β i

e_a.H∀ (x : ι),
  AddMonoidHom.comp ψ (Dfinsupp.singleAddHom (fun i => (fun i => β i) i) x) =     AddMonoidHom.comp (toAddMonoid fun i => AddMonoidHom.comp ψ (of β i))
      (Dfinsupp.singleAddHom (fun i => (fun i => β i) i) x)
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (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 => β i
of]
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),
  ↑ψ f = ↑(toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)) f
DirectSum.toAddMonoid.unique

end ToAddMonoid

section FromAddMonoid

/-- `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 => β i
fromAddMonoid : (⨁ i: ?m.224425
i, γ: Type u₁
γ →+ β: ι → Type w
β i: ?m.224425
i) →+ γ: Type u₁
γ →+ ⨁ i: ?m.225655
i, β: ι → Type w
β i: ?m.225655
i :=
  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.228003
i => 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 →+ P
AddMonoidHom.compHom (of: {ι : Type ?u.236548} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.236547) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of β: ι → Type w
β i: ?m.228003
i)
#align direct_sum.from_add_monoid DirectSum.fromAddMonoid: {ι : Type v} →
  [dec_ι : DecidableEq ι] →
    {β : ι → Type w} →
      [inst : (i : ι) → AddCommMonoid (β i)] →
        {γ : Type u₁} → [inst_1 : AddCommMonoid γ] → (DirectSum ι fun i => γ →+ β i) →+ γ →+ DirectSum ι fun i => β i
DirectSum.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) f
fromAddMonoid_of (i: ι
i : ι: Type v
ι) (f: γ →+ β i
f : γ: 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 => β i
fromAddMonoid (of: {ι : Type ?u.246440} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.246439) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?m.246441 → Type ?u.246439
_ i: ι
i f: γ →+ β i
f) = (of: {ι : Type ?u.255391} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.255390) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?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 →+ P
comp f: γ →+ β i
f := by
Goals accomplished! 🐙
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) frw [ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (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} →
          [inst_1 : AddCommMonoid γ] → (DirectSum ι fun i => γ →+ β i) →+ γ →+ DirectSum ι fun i => β i
fromAddMonoid,ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

↑(toAddMonoid fun i => ↑AddMonoidHom.compHom (of β i)) (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) f ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) ftoAddMonoid_of: ∀ {ι : Type ?u.256706} [dec_ι : DecidableEq ι] {β : ι → Type ?u.256705} [inst : (i : ι) → AddCommMonoid (β i)]
  {γ : Type ?u.256704} [inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
  ↑(toAddMonoid φ) (↑(of β i) x) = ↑(φ i) x
toAddMonoid_ofι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

↑(↑AddMonoidHom.compHom (of β i)) f = AddMonoidHom.comp (of β i) f]ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

↑(↑AddMonoidHom.compHom (of β i)) f = AddMonoidHom.comp (of β i) f
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) frfl
Goals 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) f
DirectSum.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: γ →+ β i
f : γ: 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 => β i
fromAddMonoid (of: {ι : Type ?u.267447} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.267446) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?m.267448 → Type ?u.267446
_ i: ι
i f: γ →+ β i
f) x: γ
x = of: {ι : Type ?u.284894} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.284893) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of _: ?m.284895 → Type ?u.284893
_ i: ι
i (f: γ →+ β i
f x: γ
x) := by
Goals accomplished! 🐙
      ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

x: γ

↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)rw [ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

x: γ

↑(↑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),
  ↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) f
fromAddMonoid_of,ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

x: γ

↑(AddMonoidHom.comp (of β i) f) x = ↑(of β i) (↑f x) ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

x: γ

↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)AddMonoidHom.coe_comp: ∀ {M : Type ?u.302405} {N : Type ?u.302406} {P : Type ?u.302407} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (g : N →+ P) (f : M →+ N), ↑(AddMonoidHom.comp g f) = ↑g ∘ ↑f
AddMonoidHom.coe_comp,ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

x: γ

(↑(of β i) ∘ ↑f) x = ↑(of β i) (↑f x) ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

x: γ

↑(↑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 v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

i: ι

f: γ →+ β i

x: γ

↑(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

end FromAddMonoid

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 => β ↑i
setToSet (S: Set ι
S T: Set ι
T : Set: Type ?u.303891 → Type ?u.303891
Set ι: Type v
ι) (H: S ⊆ T
H : S: Set ι
S ⊆ T: Set ι
T) : (⨁ i: ↑S
i : S: Set ι
S, β: ι → Type w
β i: ↑S
i) →+ ⨁ i: ↑T
i : T: Set ι
T, β: ι → Type w
β i: ↑T
i :=
  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.305712
i => of: {ι : Type ?u.305715} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.305714) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of (fun i: Subtype T
i : Subtype: {α : Sort ?u.305719} → (α → Prop) → Sort (max1?u.305719)
Subtype T: Set ι
T => β: ι → Type w
β i: Subtype T
i) ⟨↑i: ?m.305712
i, H: S ⊆ T
H i: ?m.305712
i.2: ∀ {α : Sort ?u.305887} {p : α → Prop} (self : Subtype p), p ↑self
2⟩
#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 => β ↑i
DirectSum.setToSet

variable {β: ?m.306723
β}

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

instance unique: [inst : ∀ (i : ι), Subsingleton (β i)] → Unique (DirectSum ι fun i => β i)
unique [∀ i: ?m.306755
i, Subsingleton: Sort ?u.306758 → Prop
Subsingleton (β: ι → Type w
β i: ?m.306755
i)] : Unique: Sort ?u.306762 → Sort (max1?u.306762)
Unique (⨁ i: ?m.306767
i, β: ι → Type w
β i: ?m.306767
i) :=
  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 → Prop
IsEmpty ι: Type v
ι] : Unique: Sort ?u.308308 → Sort (max1?u.308308)
Unique (⨁ i: ?m.308313
i, β: ι → Type w
β i: ?m.308313
i) :=
  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) ≃+ M
id (M: Type v
M : Type v: Type (v+1)
Type v) (ι: optParam (Type ?u.309819) PUnit
ι : Type _: Type (?u.309819+1)
Type _ := PUnit: Sort ?u.309820
PUnit) [AddCommMonoid: Type ?u.309823 → Type ?u.309823
AddCommMonoid M: Type v
M] [Unique: Sort ?u.309826 → Sort (max1?u.309826)
Unique ι: optParam (Type ?u.309819) PUnit
ι] :
    (⨁ _x: ι
_x : ι: optParam (Type ?u.309819) PUnit
ι, M: Type v
M) ≃+ M: Type v
M :=
  {
    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
_ =>
      AddMonoidHom.id: (M : Type ?u.311110) → [inst : AddZeroClass M] → M →+ M
AddMonoidHom.id
        M: Type v
M 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 →+ M
AddMonoidHom.id M: Type v
M
    invFun := of: {ι : Type ?u.321290} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.321289) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of (fun _: ?m.321294
_ => M: Type v
M) default: {α : Sort ?u.321299} → [self : Inhabited α] → α
default
    left_inv := fun x: ?m.330297
x =>
      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),
  C 0 → (∀ (i : ι) (x : β i), C (↑(of β i) x)) → (∀ (x y : DirectSum ι fun i => β i), C x → C y → C (x + y)) → C x
DirectSum.induction_on x: ?m.330297
x (by
Goals accomplished! 🐙 ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x: DirectSum ι fun _x => M

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) 0) = 0rw [ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x: DirectSum ι fun _x => M

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) 0) = 0AddMonoidHom.map_zero: ∀ {M : Type ?u.331725} {N : Type ?u.331726} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N), ↑f 0 = 0
AddMonoidHom.map_zero,ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x: DirectSum ι fun _x => M

↑(of (fun x => M) default) 0 = 0 ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x: DirectSum ι fun _x => M

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) 0) = 0AddMonoidHom.map_zero: ∀ {M : Type ?u.332278} {N : Type ?u.332279} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N), ↑f 0 = 0
AddMonoidHom.map_zeroι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x: DirectSum ι fun _x => M

0 = 0]
Goals accomplished! 🐙)
        (fun p: ?m.331687
p x: ?m.331690
x => by
Goals accomplished! 🐙 ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝: DirectSum ι fun _x => M

p: ι

x: M

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (↑(of (fun i => M) p) x)) = ↑(of (fun i => M) p) xrw [ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝: DirectSum ι fun _x => M

p: ι

x: M

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (↑(of (fun i => M) p) x)) = ↑(of (fun i => M) p) xUnique.default_eq: ∀ {α : Sort ?u.332447} [inst : Unique α] (a : α), default = a
Unique.default_eq p: ι
p,ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝: DirectSum ι fun _x => M

p: ι

x: M

↑(of (fun x => M) p) (↑(toAddMonoid fun x => AddMonoidHom.id M) (↑(of (fun i => M) p) x)) = ↑(of (fun i => M) p) x ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝: DirectSum ι fun _x => M

p: ι

x: M

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (↑(of (fun i => M) p) x)) = ↑(of (fun i => M) p) xtoAddMonoid_of: ∀ {ι : Type ?u.332499} [dec_ι : DecidableEq ι] {β : ι → Type ?u.332498} [inst : (i : ι) → AddCommMonoid (β i)]
  {γ : Type ?u.332497} [inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
  ↑(toAddMonoid φ) (↑(of β i) x) = ↑(φ i) x
toAddMonoid_ofι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝: DirectSum ι fun _x => M

p: ι

x: M

↑(of (fun x => M) p) (↑(AddMonoidHom.id M) x) = ↑(of (fun i => M) p) x]ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝: DirectSum ι fun _x => M

p: ι

x: M

↑(of (fun x => M) p) (↑(AddMonoidHom.id M) x) = ↑(of (fun i => M) p) x;ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝: DirectSum ι fun _x => M

p: ι

x: M

↑(of (fun x => M) p) (↑(AddMonoidHom.id M) x) = ↑(of (fun i => M) p) x ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝: DirectSum ι fun _x => M

p: ι

x: M

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (↑(of (fun i => M) p) x)) = ↑(of (fun i => M) p) xrfl
Goals accomplished! 🐙) fun x: ?m.331697
x y: ?m.331700
y ihx: ?m.331703
ihx ihy: ?m.331706
ihy => by
Goals accomplished! 🐙
        ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (x + y)) = x + yrw [ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (x + y)) = x + yAddMonoidHom.map_add: ∀ {M : Type ?u.333021} {N : Type ?u.333022} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (a b : M),
  ↑f (a + b) = ↑f a + ↑f b
AddMonoidHom.map_add,ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x + ↑(toAddMonoid fun x => AddMonoidHom.id M) y) =   x + y ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (x + y)) = x + yAddMonoidHom.map_add: ∀ {M : Type ?u.333217} {N : Type ?u.333218} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (a b : M),
  ↑f (a + b) = ↑f a + ↑f b
AddMonoidHom.map_add,ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) +     ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) =   x + y ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (x + y)) = x + yihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x
ihx,ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

x + ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = x + y ι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (x + y)) = x + yihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y
ihyι✝: Type v

dec_ι: DecidableEq ι✝

β: ι✝ → Type w

inst✝³: (i : ι✝) → AddCommMonoid (β i)

γ: Type u₁

inst✝²: AddCommMonoid γ

M: Type v

ι: optParam (Type ?u.309819) PUnit

inst✝¹: AddCommMonoid M

inst✝: Unique ι

src✝:= toAddMonoid fun x => AddMonoidHom.id M: (DirectSum ι fun i => M) →+ M

x✝, x, y: DirectSum ι fun i => M

ihx: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x

ihy: ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y

x + y = x + y]
Goals accomplished! 🐙
    right_inv := fun x: ?m.330583
x => 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) x
toAddMonoid_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) ≃+ M
DirectSum.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.333828
i, β: ι → Type w
β i: ?m.333828
i) ≃+ ⨁ k: ?m.333865
k, β: ι → Type w
β (h: ι ≃ κ
h.symm: {α : Sort ?u.333868} → {β : Sort ?u.333867} → α ≃ β → β ≃ α
symm k: ?m.333865
k) :=
  { 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' g
Dfinsupp.comapDomain'_add _: ?m.336843 → ?m.336841
_ h: ι ≃ κ
h.right_inv: ∀ {α : Sort ?u.336848} {β : Sort ?u.336847} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
right_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 => β i
f : ⨁ i: ?m.339459
i, β: ι → Type w
β i: ?m.339459
i) (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 => β i
f k: κ
k = f: DirectSum ?m.339457 fun i => β i
f (h: ι ≃ κ
h.symm: {α : Sort ?u.339784} → {β : Sort ?u.339783} → α ≃ β → β ≃ α
symm k: κ
k) := by
Goals accomplished! 🐙
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝¹: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝: AddCommMonoid γ

κ: Type u_1

h: ι ≃ κ

f: DirectSum ι fun i => β i

k: κ

↑(↑(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.toFun
right_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.341450
Option ι: Type v
ι → Type w: Type (w+1)
Type w} [∀ i: ?m.341414
i, AddCommMonoid: Type ?u.341417 → Type ?u.341417
AddCommMonoid (α: Option ι → Type w
α i: ?m.341414
i)]

-- 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)),
  ↑(AddEquiv.symm addEquivProdDirectSum) a = Equiv.invFun Dfinsupp.equivProdDfinsupp a
simps]
noncomputable def addEquivProdDirectSum: (DirectSum (Option ι) fun i => α i) ≃+ α none × DirectSum ι fun i => α (some i)
addEquivProdDirectSum : (⨁ i: ?m.341468
i, α: Option ι → Type w
α i: ?m.341468
i) ≃+ α: Option ι → Type w
α none: {α : Type ?u.341503} → Option α
none × ⨁ i: ?m.341510
i, α: Option ι → Type w
α (some: {α : Type ?u.341512} → α → Option α
some i: ?m.341510
i) :=
  { 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 g
Dfinsupp.equivProdDfinsupp_add }
#align direct_sum.add_equiv_prod_direct_sum DirectSum.addEquivProdDirectSum: {ι : Type v} →
  [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.347670
i, α: ι → Type u
α i: ?m.347670
i → Type w: Type (w+1)
Type w} [∀ i: ?m.347678
i j: ?m.347681
j, AddCommMonoid: Type ?u.347684 → Type ?u.347684
AddCommMonoid (δ: (i : ι) → α i → Type w
δ i: ?m.347730
i j: ?m.347681
j)]

/-- 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 j
sigmaCurry : (⨁ i: (_i : ?m.347749) × ?m.347754 _i
i : Σ _i: ?m.347751
_i, _: Type ?u.347747
_, δ: (i : ι) → α i → Type w
δ i: (_i : ?m.347749) × ?m.347754 _i
i.1: {α : Type ?u.347758} → {β : α → Type ?u.347757} → Sigma β → α
1 i: (_i : ?m.347749) × ?m.347754 _i
i.2: {α : Type ?u.347768} → {β : α → Type ?u.347767} → (self : Sigma β) → β self.fst
2) →+ ⨁ (i: ?m.347827
i) (j: ?m.347833
j), δ: (i : ι) → α i → Type w
δ i: ?m.347827
i j: ?m.347833
j
    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 j
Dfinsupp.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 = 0
Dfinsupp.sigmaCurry_zero
  map_add' f: ?m.354006
f g: ?m.354009
g := @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 g
Dfinsupp.sigmaCurry_add _: Type ?u.354012
_ _: ?m.354014 → Type ?u.354013
_ δ: (i : ι) → α i → Type w
δ _ f: ?m.354006
f g: ?m.354009
g
#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 j
DirectSum.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.snd
f : ⨁ i: (_i : ?m.357757) × ?m.357762 _i
i : Σ _i: ?m.357759
_i, _: Type ?u.357755
_, δ: (i : ι) → α i → Type w
δ i: (_i : ?m.357757) × ?m.357762 _i
i.1: {α : Type ?u.357766} → {β : α → Type ?u.357765} → Sigma β → α
1 i: (_i : ?m.357757) × ?m.357762 _i
i.2: {α : Type ?u.357776} → {β : α → Type ?u.357775} → (self : Sigma β) → β self.fst
2) (i: ι
i : ι: Type v
ι) (j: α i
j : α: ι → 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 j
sigmaCurry f: DirectSum ?m.357753 fun i => δ i.fst i.snd
f i: ι
i j: α i
j = f: DirectSum ?m.357753 fun i => δ i.fst i.snd
f ⟨i: ι
i, j: α i
j⟩ :=
  @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: α i
j
#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.snd
sigmaUncurry [∀ i: ?m.369399
i, DecidableEq: Sort ?u.369402 → Sort (max1?u.369402)
DecidableEq (α: ι → Type u
α i: ?m.369399
i)] [∀ i: ?m.369415
i j: ?m.369418
j, DecidableEq: Sort ?u.369421 → Sort (max1?u.369421)
DecidableEq (δ: (i : ι) → α i → Type w
δ i: ?m.369415
i j: ?m.369418
j)] :
    (⨁ (i: ?m.369442
i) (j: ?m.369448
j), δ: (i : ι) → α i → Type w
δ i: ?m.369442
i j: ?m.369448
j) →+ ⨁ i: (_i : ?m.369552) × ?m.369557 _i
i : Σ _i: ?m.369554
_i, _: Type ?u.369550
_, δ: (i : ι) → α i → Type w
δ i: (_i : ?m.369552) × ?m.369557 _i
i.1: {α : Type ?u.369561} → {β : α → Type ?u.369560} → Sigma β → α
1 i: (_i : ?m.369552) × ?m.369557 _i
i.2: {α : Type ?u.369571} → {β : α → Type ?u.369570} → (self : Sigma β) → β self.fst
2
    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.snd
Dfinsupp.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 = 0
Dfinsupp.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 g
Dfinsupp.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.snd
DirectSum.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) j
sigmaUncurry_apply [∀ i: ?m.380546
i, DecidableEq: Sort ?u.380549 → Sort (max1?u.380549)
DecidableEq (α: ι → Type u
α i: ?m.380546
i)] [∀ i: ?m.380562
i j: ?m.380565
j, DecidableEq: Sort ?u.380568 → Sort (max1?u.380568)
DecidableEq (δ: (i : ι) → α i → Type w
δ i: ?m.380562
i j: ?m.380565
j)]
    (f: DirectSum ι fun i => DirectSum (α i) fun j => δ i j
f : ⨁ (i: ?m.380587
i) (j: ?m.380593
j), δ: (i : ι) → α i → Type w
δ i: ?m.380587
i j: ?m.380593
j) (i: ι
i : ι: Type v
ι) (j: α i
j : α: ι → 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.snd
sigmaUncurry f: DirectSum ?m.380585 fun i => DirectSum (α i) fun j => δ i j
f ⟨i: ι
i, j: α i
j⟩ = f: DirectSum ?m.380585 fun i => DirectSum (α i) fun j => δ i j
f i: ι
i j: α i
j :=
  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) j
Dfinsupp.sigmaUncurry_apply f: DirectSum ι fun i => DirectSum (α i) fun j => δ i j
f i: ι
i j: α i
j
#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) j
DirectSum.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 j
sigmaCurryEquiv [∀ i: ?m.392298
i, DecidableEq: Sort ?u.392301 → Sort (max1?u.392301)
DecidableEq (α: ι → Type u
α i: ?m.392298
i)] [∀ i: ?m.392314
i j: ?m.392317
j, DecidableEq: Sort ?u.392320 → Sort (max1?u.392320)
DecidableEq (δ: (i : ι) → α i → Type w
δ i: ?m.392314
i j: ?m.392317
j)] :
    (⨁ i: (_i : ?m.392343) × ?m.392348 _i
i : Σ _i: ?m.392345
_i, _: Type ?u.392341
_, δ: (i : ι) → α i → Type w
δ i: (_i : ?m.392343) × ?m.392348 _i
i.1: {α : Type ?u.392352} → {β : α → Type ?u.392351} → Sigma β → α
1 i: (_i : ?m.392343) × ?m.392348 _i
i.2: {α : Type ?u.392362} → {β : α → Type ?u.392361} → (self : Sigma β) → β self.fst
2) ≃+ ⨁ (i: ?m.392421
i) (j: ?m.392427
j), δ: (i : ι) → α i → Type w
δ i: ?m.392421
i j: ?m.392427
j :=
  { 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 j
sigmaCurry{ 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 j
Dfinsupp.sigmaCurryEquiv{ sigmaCurry, Dfinsupp.sigmaCurryEquiv with }: ?m.395252 ≃+ ?m.395253
 { sigmaCurry, Dfinsupp.sigmaCurryEquiv with }: ?m.395252 ≃+ ?m.395253
with{ 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 j
DirectSum.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 : AddCommMonoid M] →
          [inst_1 : SetLike S M] →
            [inst_2 : AddSubmonoidClass S M] → (A : ι → S) → (DirectSum ι fun i => { x // x ∈ A i }) →+ M
coeAddMonoidHom {M: Type ?u.405588
M S: Type ?u.405591
S : Type _: Type (?u.405588+1)
Type _} [DecidableEq: Sort ?u.405594 → Sort (max1?u.405594)
DecidableEq ι: Type v
ι] [AddCommMonoid: Type ?u.405603 → Type ?u.405603
AddCommMonoid M: Type ?u.405588
M] [SetLike: Type ?u.405607 → outParam (Type ?u.405606) → Type (max?u.405607?u.405606)
SetLike S: Type ?u.405591
S M: Type ?u.405588
M]
    [AddSubmonoidClass: (S : Type ?u.405611) → (M : Type ?u.405610) → [inst : AddZeroClass M] → [inst : SetLike S M] → Prop
AddSubmonoidClass S: Type ?u.405591
S M: Type ?u.405588
M] (A: ι → S
A : ι: Type v
ι → S: Type ?u.405591
S) : (⨁ i: ?m.406042
i, A: ι → S
A i: ?m.406042
i) →+ M: Type ?u.405588
M :=
  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.408896
i => AddSubmonoidClass.Subtype: {M : Type ?u.408899} →
  [inst : AddZeroClass M] →
    {A : Type ?u.408898} → [inst_1 : SetLike A M] → [hA : AddSubmonoidClass A M] → (S' : A) → { x // x ∈ S' } →+ M
AddSubmonoidClass.Subtype (A: ι → S
A i: ?m.408896
i)
#align direct_sum.coe_add_monoid_hom DirectSum.coeAddMonoidHom: {ι : Type v} →
  {M : Type u_1} →
    {S : Type u_2} →
      [inst : DecidableEq ι] →
        [inst : AddCommMonoid M] →
          [inst_1 : SetLike S M] →
            [inst_2 : AddSubmonoidClass S M] → (A : ι → S) → (DirectSum ι fun i => { x // x ∈ A i }) →+ M
DirectSum.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) = ↑x
coeAddMonoidHom_of {M: Type ?u.410729
M S: Type ?u.410732
S : Type _: Type (?u.410732+1)
Type _} [DecidableEq: Sort ?u.410735 → Sort (max1?u.410735)
DecidableEq ι: Type v
ι] [AddCommMonoid: Type ?u.410744 → Type ?u.410744
AddCommMonoid M: Type ?u.410729
M] [SetLike: Type ?u.410748 → outParam (Type ?u.410747) → Type (max?u.410748?u.410747)
SetLike S: Type ?u.410732
S M: Type ?u.410729
M]
    [AddSubmonoidClass: (S : Type ?u.410752) → (M : Type ?u.410751) → [inst : AddZeroClass M] → [inst : SetLike S M] → Prop
AddSubmonoidClass S: Type ?u.410732
S M: Type ?u.410729
M] (A: ι → S
A : ι: Type v
ι → S: Type ?u.410732
S) (i: ι
i : ι: Type v
ι) (x: { x // x ∈ A i }
x : A: ι → S
A i: ι
i) :
    DirectSum.coeAddMonoidHom: {ι : Type ?u.411207} →
  {M : Type ?u.411206} →
    {S : Type ?u.411205} →
      [inst : DecidableEq ι] →
        [inst : AddCommMonoid M] →
          [inst_1 : SetLike S M] →
            [inst_2 : AddSubmonoidClass S M] → (A : ι → S) → (DirectSum ι fun i => { x // x ∈ A i }) →+ M
DirectSum.coeAddMonoidHom A: ι → S
A (of: {ι : Type ?u.419758} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.419757) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of (fun i: ?m.419762
i => A: ι → S
A i: ?m.419762
i) 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) x
toAddMonoid_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) = ↑x
DirectSum.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_1
M S: Type u_2
S : Type _: Type (?u.431776+1)
Type _} [DecidableEq: Sort ?u.431779 → Sort (max1?u.431779)
DecidableEq ι: Type v
ι] [AddCommMonoid: Type ?u.431788 → Type ?u.431788
AddCommMonoid M: Type ?u.431773
M] [SetLike: Type ?u.431792 → outParam (Type ?u.431791) → Type (max?u.431792?u.431791)
SetLike S: Type ?u.431776
S M: Type ?u.431773
M]
    [AddSubmonoidClass: (S : Type ?u.431796) → (M : Type ?u.431795) → [inst : AddZeroClass M] → [inst : SetLike S M] → Prop
AddSubmonoidClass S: Type ?u.431776
S M: Type ?u.431773
M] {A: ι → S
A : ι: Type v
ι → S: Type ?u.431776
S} (i: ι
i j: ι
j : ι: Type v
ι) (x: { x // x ∈ A i }
x : A: ι → S
A i: ι
i) :
    (of: {ι : Type ?u.432253} →
  [dec_ι : DecidableEq ι] →
    (β : ι → Type ?u.432252) → [inst : (i : ι) → AddCommMonoid (β i)] → (i : ι) → β i →+ DirectSum ι fun i => β i
of (fun i: ?m.432257
i ↦ {x: ?m.432262
x // x: ?m.432262
x ∈ A: ι → S
A i: ?m.432257
i}) i: ι
i x: { x // x ∈ A i }
x j: ι
j : M: Type ?u.431773
M) = if i: ι
i = j: ι
j then x: { x // x ∈ A i }
x else 0: ?m.442473
0 := by
Goals accomplished! 🐙
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝⁵: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝⁴: AddCommMonoid γ

M: Type u_1

S: Type u_2

inst✝³: DecidableEq ι

inst✝²: AddCommMonoid M

inst✝¹: SetLike S M

inst✝: 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)obtain rfl: i = j
rflrfl | h: i = j ∨ i ≠ j
 | h: i ≠ j
h := Decidable.eq_or_ne: ∀ {α : Sort ?u.443475} (x y : α) [inst : Decidable (x = y)], x = y ∨ x ≠ y
Decidable.eq_or_ne i: ι
i j: ι
jι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝⁵: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝⁴: AddCommMonoid γ

M: Type u_1

S: Type u_2

inst✝³: DecidableEq ι

inst✝²: AddCommMonoid M

inst✝¹: SetLike S M

inst✝: AddSubmonoidClass S M

A: ι → S

i: ι

x: { x // x ∈ A i }

inl↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) i) = ↑(if i = i then x else 0)
ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝⁵: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝⁴: AddCommMonoid γ

M: Type u_1

S: Type u_2

inst✝³: DecidableEq ι

inst✝²: AddCommMonoid M

inst✝¹: SetLike S M

inst✝: AddSubmonoidClass S M

A: ι → S

i, j: ι

x: { x // x ∈ A i }

h: i ≠ j

inr↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)
  ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝⁵: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝⁴: AddCommMonoid γ

M: Type u_1

S: Type u_2

inst✝³: DecidableEq ι

inst✝²: AddCommMonoid M

inst✝¹: SetLike S M

inst✝: 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)·ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝⁵: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝⁴: AddCommMonoid γ

M: Type u_1

S: Type u_2

inst✝³: DecidableEq ι

inst✝²: AddCommMonoid M

inst✝¹: SetLike S M

inst✝: AddSubmonoidClass S M

A: ι → S

i: ι

x: { x // x ∈ A i }

inl↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) i) = ↑(if i = i then x else 0) ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝⁵: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝⁴: AddCommMonoid γ

M: Type u_1

S: Type u_2

inst✝³: DecidableEq ι

inst✝²: AddCommMonoid M

inst✝¹: SetLike S M

inst✝: AddSubmonoidClass S M

A: ι → S

i: ι

x: { x // x ∈ A i }

inl↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) i) = ↑(if i = i then x else 0)
ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝⁵: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝⁴: AddCommMonoid γ

M: Type u_1

S: Type u_2

inst✝³: DecidableEq ι

inst✝²: AddCommMonoid M

inst✝¹: SetLike S M

inst✝: AddSubmonoidClass S M

A: ι → S

i, j: ι

x: { x // x ∈ A i }

h: i ≠ j

inr↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)rw [ι: Type v

dec_ι: DecidableEq ι

β: ι → Type w

inst✝⁵: (i : ι) → AddCommMonoid (β i)

γ: Type u₁

inst✝⁴: AddCommMonoid γ

M: Type u_1

S: Type u_2

inst✝³: DecidableEq ι

inst✝²: