Theorem: Finsupp.mul_eq_zero_of_disjoint_support (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ f * g = 0
Tactic:
rw [← Finsupp.support_eq_empty, ← Finset.subset_empty]
State after:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ (f * g).support ⊆ ∅

State before:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ (f * g).support ⊆ ∅
Tactic:
refine Finsupp.support_mul.trans ?_
State after:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ f.support ∩ g.support ⊆ ∅

State before:
m : Type u → Type v
inst✝² : Monad m
ι : Type u_1
β : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : MulZeroClass β
f g : ι →₀ β
h : Disjoint f.support g.support
⊢ f.support ∩ g.support ⊆ ∅
Tactic:
rwa [Finset.subset_empty, ← Finset.disjoint_iff_inter_eq_empty]
State after:
no goals