α : 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
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝¹ : MulZeroClass β
inst✝ : DecidableEq α
g₁ g₂ : α →₀ β
⊢ (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support
intro a h
α : 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
α : 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
simp only [mul_apply, mem_support_iff] at h
α : 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
α : 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
simp only [mem_support_iff, mem_inter, Ne.def]
α : 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)
α : 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
rw [← not_or]
α : 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
α : 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)
intro w
α : 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
α : 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
apply h
no goals
α : 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
cases' w with w w <;> (rw [w] ; simp)
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
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
rw [w]
no goals
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
simp