case H₁
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
⊢ support (↑(map f) p) ⊆ support p

case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
⊢ support p ⊆ support (↑(map f) p)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
⊢ support (↑(map f) p) = support p
apply Finset.Subset.antisymm
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : x ∈ support p
⊢ x ∈ support (↑(map f) p)
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
⊢ support p ⊆ support (↑(map f) p)
intro x hx
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : x ∈ support p
⊢ coeff x (↑(map f) p) ≠ 0
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : x ∈ support p
⊢ x ∈ support (↑(map f) p)
rw [mem_support_iff]
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : coeff x (↑(map f) p) = 0
⊢ ¬x ∈ support p
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : x ∈ support p
⊢ coeff x (↑(map f) p) ≠ 0
contrapose! hx
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : coeff x (↑(map f) p) = 0
⊢ coeff x p = 0
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : coeff x (↑(map f) p) = 0
⊢ ¬x ∈ support p
simp only [Classical.not_not, mem_support_iff]
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : coeff x (↑(map f) p) = 0
⊢ coeff x p = 0
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : coeff x (↑(map f) p) = 0
⊢ coeff x p = 0
replace hx : (map f p).coeff x = 0 := hx
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : ↑f (coeff x p) = ↑f 0
⊢ coeff x p = 0
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : coeff x (↑(map f) p) = 0
⊢ coeff x p = 0
rw [coeff_map, ← f.map_zero] at hx
no goals
case H₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
x : σ →₀ ℕ
hx : ↑f (coeff x p) = ↑f 0
⊢ coeff x p = 0
exact hf hx
no goals
case H₁
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
⊢ support (↑(map f) p) ⊆ support p
exact MvPolynomial.support_map_subset _ _