ι : Type ?u.49490
R : Type ?u.49493
M : Type u_1
σ : Type u_2
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
ι : Type ?u.49490
R : Type ?u.49493
M : Type u_1
σ : Type u_2
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
let ℳ' : ι → AddSubmonoid M := fun i ↦
  (⟨⟨ℳ i, fun x y ↦ AddMemClass.add_mem x y⟩, (ZeroMemClass.zero_mem _)⟩ : AddSubmonoid M)
ι : Type ?u.49490
R : Type ?u.49493
M : Type u_1
σ : Type u_2
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
ι : Type ?u.49490
R : Type ?u.49493
M : Type u_1
σ : Type u_2
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
haveI t : DirectSum.Decomposition ℳ' :=
  { decompose' := DirectSum.decompose ℳ
    left_inv := fun _ ↦ (decompose ℳ).left_inv _
    right_inv := fun _ ↦ (decompose ℳ).right_inv _ }
ι : Type ?u.49490
R : Type ?u.49493
M : Type u_1
σ : Type u_2
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
ι : Type ?u.49490
R : Type ?u.49493
M : Type u_1
σ : Type u_2
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
have mem : ∀ m, m ∈ iSup ℳ' := fun _m ↦
  (DirectSum.IsInternal.addSubmonoid_iSup_eq_top ℳ' (Decomposition.isInternal ℳ')).symm ▸ trivial
no goals
ι : Type ?u.49490
R : Type ?u.49493
M : Type u_1
σ : Type u_2
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
exact fun m ↦ @AddSubmonoid.iSup_induction _ _ _ ℳ' _ _ (mem m)
  (fun i m h ↦ h_homogeneous ⟨m, h⟩) h_zero h_add