case a
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
a✝ : G × G
⊢ a✝ ∈ Finset.filter (fun p => p.fst * p.snd = x) (f.support ×ˢ g.support) ↔
    a✝ ∈ Finset.filter (fun p => p.fst ∈ f.support ∧ p.snd ∈ g.support) s
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
⊢ Finset.filter (fun p => p.fst * p.snd = x) (f.support ×ˢ g.support) =
    Finset.filter (fun p => p.fst ∈ f.support ∧ p.snd ∈ g.support) s
ext
no goals
case a
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
a✝ : G × G
⊢ a✝ ∈ Finset.filter (fun p => p.fst * p.snd = x) (f.support ×ˢ g.support) ↔
    a✝ ∈ Finset.filter (fun p => p.fst ∈ f.support ∧ p.snd ∈ g.support) s
simp only [mem_filter, mem_product, hs, and_comm]
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → ↑f p.fst ≠ 0 → ↑g p.snd = 0
⊢ ↑f p.fst * ↑g p.snd = 0
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
p : G × G
hps : p ∈ s
hp : ¬p ∈ Finset.filter (fun p => p.fst ∈ f.support ∧ p.snd ∈ g.support) s
⊢ ↑f p.fst * ↑g p.snd = 0
simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp⊢
case pos
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → ↑f p.fst ≠ 0 → ↑g p.snd = 0
h1 : ↑f p.fst = 0
⊢ ↑f p.fst * ↑g p.snd = 0

case neg
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → ↑f p.fst ≠ 0 → ↑g p.snd = 0
h1 : ¬↑f p.fst = 0
⊢ ↑f p.fst * ↑g p.snd = 0
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → ↑f p.fst ≠ 0 → ↑g p.snd = 0
⊢ ↑f p.fst * ↑g p.snd = 0
by_cases h1 : f p.1 = 0
no goals
case pos
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → ↑f p.fst ≠ 0 → ↑g p.snd = 0
h1 : ↑f p.fst = 0
⊢ ↑f p.fst * ↑g p.snd = 0
rw [h1, zero_mul]
no goals
case neg
k : Type u₁
G : Type u₂
R : Type ?u.357749
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x
F : G × G → k := fun p => if p.fst * p.snd = x then ↑f p.fst * ↑g p.snd else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → ↑f p.fst ≠ 0 → ↑g p.snd = 0
h1 : ¬↑f p.fst = 0
⊢ ↑f p.fst * ↑g p.snd = 0
rw [hp hps h1, mul_zero]