Theorem: MvPolynomial.Finsupp.support_mapDomain (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (Finsupp.mapDomain (⇑f) v).support ⊆ Finset.map f v.support
Tactic:
classical
rw [Finsupp.mapDomain]
refine' Finset.Subset.trans Finsupp.support_sum _
simp only [Finsupp.mem_support_iff, Finset.biUnion_subset_iff_forall_subset, Ne]
intro x hx
apply Finset.Subset.trans Finsupp.support_single_subset
simp [hx]
State after:
no goals

State before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (Finsupp.mapDomain (⇑f) v).support ⊆ Finset.map f v.support
Tactic:
rw [Finsupp.mapDomain]
State after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.sum fun a => Finsupp.single (f a)).support ⊆ Finset.map f v.support

State before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.sum fun a => Finsupp.single (f a)).support ⊆ Finset.map f v.support
Tactic:
refine' Finset.Subset.trans Finsupp.support_sum _
State after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.support.biUnion fun a => (Finsupp.single (f a) (v a)).support) ⊆ Finset.map f v.support

State before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.support.biUnion fun a => (Finsupp.single (f a) (v a)).support) ⊆ Finset.map f v.support
Tactic:
simp only [Finsupp.mem_support_iff, Finset.biUnion_subset_iff_forall_subset, Ne]
State after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ ∀ (x : α), ¬v x = 0 → (Finsupp.single (f x) (v x)).support ⊆ Finset.map f v.support

State before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ ∀ (x : α), ¬v x = 0 → (Finsupp.single (f x) (v x)).support ⊆ Finset.map f v.support
Tactic:
intro x hx
State after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ (Finsupp.single (f x) (v x)).support ⊆ Finset.map f v.support

State before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ (Finsupp.single (f x) (v x)).support ⊆ Finset.map f v.support
Tactic:
apply Finset.Subset.trans Finsupp.support_single_subset
State after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ {f x} ⊆ Finset.map f v.support

State before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ {f x} ⊆ Finset.map f v.support
Tactic:
simp [hx]
State after:
no goals