case a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ (⨆ (i : ι) (_ : p i), S i) ≤
    AddMonoidHom.mrange
      (AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
        (filterAddMonoidHom (fun i => { x // x ∈ S i }) p))

case a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange
      (AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
        (filterAddMonoidHom (fun i => { x // x ∈ S i }) p)) ≤
    ⨆ (i : ι) (_ : p i), S i
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ (⨆ (i : ι) (_ : p i), S i) =
    AddMonoidHom.mrange
      (AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
        (filterAddMonoidHom (fun i => { x // x ∈ S i }) p))
apply le_antisymm
case a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ ↑(AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
          (filterAddMonoidHom (fun i => { x // x ∈ S i }) p))
      (single i { val := y, property := hy }) =
    y
case a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ (⨆ (i : ι) (_ : p i), S i) ≤
    AddMonoidHom.mrange
      (AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
        (filterAddMonoidHom (fun i => { x // x ∈ S i }) p))
refine' iSup₂_le fun i hi y hy => ⟨Dfinsupp.single i ⟨y, hy⟩, _⟩
case a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ ↑(sumAddHom fun i => AddSubmonoid.subtype (S i)) (single i { val := y, property := hy }) = y
case a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ ↑(AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
          (filterAddMonoidHom (fun i => { x // x ∈ S i }) p))
      (single i { val := y, property := hy }) =
    y
rw [AddMonoidHom.comp_apply, filterAddMonoidHom_apply, filter_single_pos _ _ hi]
no goals
case a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ ↑(sumAddHom fun i => AddSubmonoid.subtype (S i)) (single i { val := y, property := hy }) = y
exact sumAddHom_single _ _ _
case a.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
⊢ ↑(AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
          (filterAddMonoidHom (fun i => { x // x ∈ S i }) p))
      v ∈
    ⨆ (i : ι) (_ : p i), S i
case a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange
      (AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
        (filterAddMonoidHom (fun i => { x // x ∈ S i }) p)) ≤
    ⨆ (i : ι) (_ : p i), S i
rintro x ⟨v, rfl⟩
case a.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i ≠ 0
⊢ ↑((fun i => AddSubmonoid.subtype (S i)) i) (↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (i : ι) (_ : p i), S i
case a.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
⊢ ↑(AddMonoidHom.comp (sumAddHom fun i => AddSubmonoid.subtype (S i))
          (filterAddMonoidHom (fun i => { x // x ∈ S i }) p))
      v ∈
    ⨆ (i : ι) (_ : p i), S i
refine' dfinsupp_sumAddHom_mem _ _ _ fun i _ => _
case a.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i ≠ 0
⊢ ↑((fun i => AddSubmonoid.subtype (S i)) i) (↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
case a.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i ≠ 0
⊢ ↑((fun i => AddSubmonoid.subtype (S i)) i) (↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (i : ι) (_ : p i), S i
refine' AddSubmonoid.mem_iSup_of_mem i _
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i ≠ 0
hp : p i
⊢ ↑((fun i => AddSubmonoid.subtype (S i)) i) (↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i

case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i ≠ 0
hp : ¬p i
⊢ ↑((fun i => AddSubmonoid.subtype (S i)) i) (↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
case a.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i ≠ 0
⊢ ↑((fun i => AddSubmonoid.subtype (S i)) i) (↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
by_cases hp : p i
no goals
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i ≠ 0
hp : p i
⊢ ↑((fun i => AddSubmonoid.subtype (S i)) i) (↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
simp [hp]
no goals
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i ≠ 0
hp : ¬p i
⊢ ↑((fun i => AddSubmonoid.subtype (S i)) i) (↑(↑(filterAddMonoidHom (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
simp [hp]