-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem support_sum_eq_biUnion {α : Type*} {ι : Type*} {M : Type*} [DecidableEq α]
    [AddCommMonoid M] {g : ι → α →₀ M} (s : Finset ι)
    (h : ∀ i₁ i₂, i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support) :
    (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support

Proof state:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
⊢ ((∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support) →
    (∑ i ∈ insert i s, g i).support = (insert i s).biUnion fun i => (g i).support

Tactic:
simp only [hi, sum_insert, not_false_iff, biUnion_insert]

Result:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
⊢ ((∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support) →
    (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun i => (g i).support

Proof state:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
⊢ ∀ i_1 ∈ s, Disjoint (g i).support (g i_1).support

Tactic:
intro j hj

Result:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
j : ι
hj : j ∈ s
⊢ Disjoint (g i).support (g j).support

Proof state:
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support

Tactic:
refine Finset.induction_on s ?_ ?_

Result:
case refine_1
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ (∑ i ∈ ∅, g i).support = ∅.biUnion fun i => (g i).support

case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support) →
        (∑ i ∈ insert a s, g i).support = (insert a s).biUnion fun i => (g i).support

Proof state:
case refine_1
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ (∑ i ∈ ∅, g i).support = ∅.biUnion fun i => (g i).support

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support) →
        (∑ i ∈ insert a s, g i).support = (insert a s).biUnion fun i => (g i).support

Tactic:
intro i s hi

Result:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
⊢ ((∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support) →
    (∑ i ∈ insert i s, g i).support = (insert i s).biUnion fun i => (g i).support

Proof state:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
⊢ Disjoint (g i).support (∑ i ∈ s, g i).support

Tactic:
rw [hs, Finset.disjoint_biUnion_right]

Result:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
⊢ ∀ i_1 ∈ s, Disjoint (g i).support (g i_1).support

Proof state:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
j : ι
hj : j ∈ s
⊢ Disjoint (g i).support (g j).support

Tactic:
exact h _ _ (ne_of_mem_of_not_mem hj hi).symm

Result:
no goals

Proof state:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
⊢ ((∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support) →
    (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun i => (g i).support

Tactic:
intro hs

Result:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
⊢ (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun i => (g i).support

Proof state:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
⊢ (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun i => (g i).support

Tactic:
rw [Finsupp.support_add_eq, hs]

Result:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
⊢ Disjoint (g i).support (∑ i ∈ s, g i).support