[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
x y : Decomposition ℳ
⊢ x = y
[PROOFSTEP]
cases' x with x xl xr
[GOAL]
case mk
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
y : Decomposition ℳ
x : M → ⨁ (i : ι), { x // x ∈ ℳ i }
xl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
xr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
⊢ { decompose' := x, left_inv := xl, right_inv := xr } = y
[PROOFSTEP]
cases' y with y yl yr
[GOAL]
case mk.mk
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
x : M → ⨁ (i : ι), { x // x ∈ ℳ i }
xl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
xr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
y : M → ⨁ (i : ι), { x // x ∈ ℳ i }
yl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) y
yr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) y
⊢ { decompose' := x, left_inv := xl, right_inv := xr } = { decompose' := y, left_inv := yl, right_inv := yr }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_decompose'
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
x : M → ⨁ (i : ι), { x // x ∈ ℳ i }
xl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
xr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) x
y : M → ⨁ (i : ι), { x // x ∈ ℳ i }
yl : Function.LeftInverse (↑(DirectSum.coeAddMonoidHom ℳ)) y
yr : Function.RightInverse (↑(DirectSum.coeAddMonoidHom ℳ)) y
⊢ x = y
[PROOFSTEP]
exact Function.LeftInverse.eq_rightInverse xr yl
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
p : M → Prop
h_zero : p 0
h_homogeneous : ∀ {i : ι} (m : { x // x ∈ ℳ i }), p ↑m
h_add : ∀ (m m' : M), p m → p m' → p (m + m')
⊢ ∀ (m : M), p m
[PROOFSTEP]
let ℳ' : ι → AddSubmonoid M := fun i ↦
  (⟨⟨ℳ i, fun x y ↦ AddMemClass.add_mem x y⟩, (ZeroMemClass.zero_mem _)⟩ : AddSubmonoid M)
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
p : M → Prop
h_zero : p 0
h_homogeneous : ∀ {i : ι} (m : { x // x ∈ ℳ i }), p ↑m
h_add : ∀ (m m' : M), p m → p m' → p (m + m')
ℳ' : ι → AddSubmonoid M :=
  fun i =>
    { toAddSubsemigroup := { carrier := ↑(ℳ i), add_mem' := (_ : ∀ {a b : M}, a ∈ ↑(ℳ i) → b ∈ ↑(ℳ i) → a + b ∈ ℳ i) },
      zero_mem' := (_ : 0 ∈ ℳ i) }
⊢ ∀ (m : M), p m
[PROOFSTEP]
haveI t : DirectSum.Decomposition ℳ' :=
  { decompose' := DirectSum.decompose ℳ
    left_inv := fun _ ↦ (decompose ℳ).left_inv _
    right_inv := fun _ ↦ (decompose ℳ).right_inv _ }
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
p : M → Prop
h_zero : p 0
h_homogeneous : ∀ {i : ι} (m : { x // x ∈ ℳ i }), p ↑m
h_add : ∀ (m m' : M), p m → p m' → p (m + m')
ℳ' : ι → AddSubmonoid M :=
  fun i =>
    { toAddSubsemigroup := { carrier := ↑(ℳ i), add_mem' := (_ : ∀ {a b : M}, a ∈ ↑(ℳ i) → b ∈ ↑(ℳ i) → a + b ∈ ℳ i) },
      zero_mem' := (_ : 0 ∈ ℳ i) }
t : Decomposition ℳ'
⊢ ∀ (m : M), p m
[PROOFSTEP]
have mem : ∀ m, m ∈ iSup ℳ' := fun _m ↦
  (DirectSum.IsInternal.addSubmonoid_iSup_eq_top ℳ' (Decomposition.isInternal ℳ')).symm ▸ trivial
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
p : M → Prop
h_zero : p 0
h_homogeneous : ∀ {i : ι} (m : { x // x ∈ ℳ i }), p ↑m
h_add : ∀ (m m' : M), p m → p m' → p (m + m')
ℳ' : ι → AddSubmonoid M :=
  fun i =>
    { toAddSubsemigroup := { carrier := ↑(ℳ i), add_mem' := (_ : ∀ {a b : M}, a ∈ ↑(ℳ i) → b ∈ ↑(ℳ i) → a + b ∈ ℳ i) },
      zero_mem' := (_ : 0 ∈ ℳ i) }
t : Decomposition ℳ'
mem : ∀ (m : M), m ∈ iSup ℳ'
⊢ ∀ (m : M), p m
[PROOFSTEP]
exact fun m ↦ @AddSubmonoid.iSup_induction _ _ _ ℳ' _ _ (mem m) (fun i m h ↦ h_homogeneous ⟨m, h⟩) h_zero h_add
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
i : ι
x : { x // x ∈ ℳ i }
⊢ ↑(decompose ℳ) ↑x = ↑(of (fun i => { x // x ∈ ℳ i }) i) x
[PROOFSTEP]
rw [← decompose_symm_of _, Equiv.apply_symm_apply]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i : ι
hx : x ∈ ℳ i
⊢ ↑(↑(↑(decompose ℳ) x) i) = x
[PROOFSTEP]
rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hx : x ∈ ℳ i
hij : i ≠ j
⊢ ↑(↑(↑(decompose ℳ) x) j) = 0
[PROOFSTEP]
rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ _ hij, ZeroMemClass.coe_zero]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in DFinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) = r
[PROOFSTEP]
conv_rhs => rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
| r
[PROOFSTEP]
rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
| r
[PROOFSTEP]
rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
| r
[PROOFSTEP]
rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in DFinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) =
    ↑(decompose ℳ).symm
      (∑ i in DFinsupp.support (↑(decompose ℳ) r), ↑(of (fun i => { x // x ∈ ℳ i }) i) (↑(↑(decompose ℳ) r) i))
[PROOFSTEP]
rw [decompose_symm_sum]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in DFinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) =
    ∑ i in DFinsupp.support (↑(decompose ℳ) r),
      ↑(decompose ℳ).symm (↑(of (fun i => { x // x ∈ ℳ i }) i) (↑(↑(decompose ℳ) r) i))
[PROOFSTEP]
simp_rw [decompose_symm_of]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : SetLike σ M
inst✝ : AddSubgroupClass σ M
ℳ : ι → σ
⊢ AddCommGroup (⨁ (i : ι), { x // x ∈ ℳ i })
[PROOFSTEP]
infer_instance
