α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
have : a ∉ g₂.support := disjoint_left.1 h ha
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
simp only [mem_support_iff, not_not] at *
no goals
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
simpa only [add_apply, this, add_zero]
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
have : a ∉ g₁.support := disjoint_right.1 h ha
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
simp only [mem_support_iff, not_not] at *
no goals
α : Type u_1
β : Type ?u.284137
γ : Type ?u.284140
ι : Type ?u.284143
M : Type u_2
M' : Type ?u.284149
N : Type ?u.284152
P : Type ?u.284155
G : Type ?u.284158
H : Type ?u.284161
R : Type ?u.284164
S : Type ?u.284167
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
simpa only [add_apply, this, zero_add]