case h0
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ 0 ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i))

case ha
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    ↑f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i))
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ x ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i))
apply Dfinsupp.induction x
case ha
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    ↑f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i))
case h0
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ 0 ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i))

case ha
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    ↑f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i))
exact AddSubmonoid.zero_mem _
no goals
case ha
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    ↑f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ (i : ι), Set.range (single i))
exact fun a b f _ _ hf =>
  AddSubmonoid.add_mem _
    (AddSubmonoid.subset_closure <| Set.mem_iUnion.2 ⟨a, Set.mem_range_self _⟩) hf