-- Mathlib/Data/DFinsupp/Submonoid.lean
theorem AddSubmonoid.bsupr_eq_mrange_dfinsupp_sumAddHom (p : ι → Prop) [DecidablePred p]
    [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :
    ⨆ (i) (_ : p i), S i =
      AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom _ p))

Proof state:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ ⨆ i, ⨆ (_ : p i), S i ≤
    AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p))

Tactic:
refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩

Result:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p)) (single i ⟨y, hy⟩) = y

Proof state:
case a.intro
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p)) v ∈ ⨆ i, ⨆ (_ : p i), S i

Tactic:
refine dfinsupp_sumAddHom_mem _ _ _ fun i _ => ?_

Result:
case a.intro
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i => ↥(S i)) p) v) i ≠ 0
⊢ (S i).subtype (((filterAddMonoidHom (fun i => ↥(S i)) p) v) i) ∈ ⨆ i, ⨆ (_ : p i), S i

Proof state:
case a.intro
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i => ↥(S i)) p) v) i ≠ 0
⊢ (S i).subtype (((filterAddMonoidHom (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
by_cases hp : p i

Result:
case pos
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i => ↥(S i)) p) v) i ≠ 0
hp : p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

case neg
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i => ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Proof state:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ ⨆ i, ⨆ (_ : p i), S i =
    AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p))

Tactic:
apply le_antisymm

Result:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ ⨆ i, ⨆ (_ : p i), S i ≤
    AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p))

case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i

Proof state:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i => (S i).subtype) (single i ⟨y, hy⟩) = y

Tactic:
exact sumAddHom_single _ _ _

Result:
no goals

Proof state:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i

Tactic:
rintro x ⟨v, rfl⟩

Result:
case a.intro
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p)) v ∈ ⨆ i, ⨆ (_ : p i), S i

Proof state:
case pos
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i => ↥(S i)) p) v) i ≠ 0
hp : p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
simp [hp]

Result:
no goals

Proof state:
case a.intro
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i => ↥(S i)) p) v) i ≠ 0
⊢ (S i).subtype (((filterAddMonoidHom (fun i => ↥(S i)) p) v) i) ∈ ⨆ i, ⨆ (_ : p i), S i

Tactic:
refine AddSubmonoid.mem_iSup_of_mem i ?_

Result:
case a.intro
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i => ↥(S i)) p) v) i ≠ 0
⊢ (S i).subtype (((filterAddMonoidHom (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Proof state:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom (fun i => ↥(S i)) p)) (single i ⟨y, hy⟩) = y

Tactic:
rw [AddMonoidHom.comp_apply, filterAddMonoidHom_apply, filter_single_pos _ _ hi]

Result:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i => (S i).subtype) (single i ⟨y, hy⟩) = y

Proof state:
case neg
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i => ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
simp [hp]

Result:
no goals