-- Mathlib/Data/Finsupp/Defs.lean
theorem support_add_eq [DecidableEq α] {g₁ g₂ : α →₀ M} (h : Disjoint g₁.support g₂.support) :
    (g₁ + g₂).support = g₁.support ∪ g₂.support :=
  le_antisymm support_zipWith fun a ha =>
    (Finset.mem_union.1 ha).elim
      (fun ha => by
        have : a ∉ g₂.support := disjoint_left.1 h ha
        simp only [mem_support_iff, not_not] at *; simpa only [add_apply, this, add_zero] )
      fun ha => by
      have : a ∉ g₁.support := disjoint_right.1 h ha
      simp only [mem_support_iff, not_not] at *; simpa only [add_apply, this, zero_add]

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₂.support
this : a ∉ g₁.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
simp only [mem_support_iff, not_not] at *

Result:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : g₂ a ≠ 0
this : g₁ a = 0
⊢ (g₁ + g₂) a ≠ 0

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₁.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
have : a ∉ g₂.support := disjoint_left.1 h ha

Result:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₁.support
this : a ∉ g₂.support
⊢ a ∈ (g₁ + g₂).support

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : g₁ a ≠ 0
this : g₂ a = 0
⊢ (g₁ + g₂) a ≠ 0

Tactic:
simpa only [add_apply, this, add_zero]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₁.support
this : a ∉ g₂.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
simp only [mem_support_iff, not_not] at *

Result:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : g₁ a ≠ 0
this : g₂ a = 0
⊢ (g₁ + g₂) a ≠ 0

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₂.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
have : a ∉ g₁.support := disjoint_right.1 h ha

Result:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : a ∈ g₂.support
this : a ∉ g₁.support
⊢ a ∈ (g₁ + g₂).support

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq α
g₁ g₂ : α →₀ M
h : Disjoint g₁.support g₂.support
a : α
ha✝ : a ∈ g₁.support ∪ g₂.support
ha : g₂ a ≠ 0
this : g₁ a = 0
⊢ (g₁ + g₂) a ≠ 0

Tactic:
simpa only [add_apply, this, zero_add]

Result:
no goals