[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
⊢ (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support
[PROOFSTEP]
intro a h
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : a ∈ (g₁ * g₂).support
⊢ a ∈ g₁.support ∩ g₂.support
[PROOFSTEP]
simp only [mul_apply, mem_support_iff] at h 
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
⊢ a ∈ g₁.support ∩ g₂.support
[PROOFSTEP]
simp only [mem_support_iff, mem_inter, Ne.def]
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
⊢ ¬↑g₁ a = 0 ∧ ¬↑g₂ a = 0
[PROOFSTEP]
rw [← not_or]
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
⊢ ¬(↑g₁ a = 0 ∨ ↑g₂ a = 0)
[PROOFSTEP]
intro w
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
w : ↑g₁ a = 0 ∨ ↑g₂ a = 0
⊢ False
[PROOFSTEP]
apply h
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
w : ↑g₁ a = 0 ∨ ↑g₂ a = 0
⊢ ↑g₁ a * ↑g₂ a = 0
[PROOFSTEP]
cases' w with w w
[GOAL]
case inl
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
w : ↑g₁ a = 0
⊢ ↑g₁ a * ↑g₂ a = 0
[PROOFSTEP]
rw [w]
[GOAL]
case inl
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
w : ↑g₁ a = 0
⊢ 0 * ↑g₂ a = 0
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
w : ↑g₂ a = 0
⊢ ↑g₁ a * ↑g₂ a = 0
[PROOFSTEP]
rw [w]
[GOAL]
case inr
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
a : α
h : ↑g₁ a * ↑g₂ a ≠ 0
w : ↑g₂ a = 0
⊢ ↑g₁ a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
f : α → β
g : α →₀ β
⊢ Set.Finite (Function.support fun a => f a • ↑g a)
[PROOFSTEP]
apply Set.Finite.subset g.finite_support
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
f : α → β
g : α →₀ β
⊢ (Function.support fun a => f a • ↑g a) ⊆ Function.support ↑g
[PROOFSTEP]
simp only [Function.support_subset_iff, Finsupp.mem_support_iff, Ne.def, Finsupp.fun_support_eq, Finset.mem_coe]
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
f : α → β
g : α →₀ β
⊢ ∀ (x : α), ¬f x • ↑g x = 0 → ¬↑g x = 0
[PROOFSTEP]
intro x hx h
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
f : α → β
g : α →₀ β
x : α
hx : ¬f x • ↑g x = 0
h : ↑g x = 0
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
f : α → β
g : α →₀ β
x : α
hx : ¬f x • ↑g x = 0
h : ↑g x = 0
⊢ f x • ↑g x = 0
[PROOFSTEP]
rw [h, smul_zero]
