no goals
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d (↑(rename f) φ) = 0
classical
rw [rename_eq, ← not_mem_support_iff]
intro H
replace H := mapDomain_support H
rw [Finset.mem_image] at H
obtain ⟨u, hu, rfl⟩ := H
specialize h u rfl
simp at h hu
contradiction
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ ¬d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d (↑(rename f) φ) = 0
rw [rename_eq, ← not_mem_support_iff]
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
⊢ False
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ ¬d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
intro H
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support
⊢ False
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
⊢ False
replace H := mapDomain_support H
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a, a ∈ φ.support ∧ Finsupp.mapDomain f a = d
⊢ False
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support
⊢ False
rw [Finset.mem_image] at H
case intro.intro
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0
⊢ False
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a, a ∈ φ.support ∧ Finsupp.mapDomain f a = d
⊢ False
obtain ⟨u, hu, rfl⟩ := H
case intro.intro
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
⊢ False
case intro.intro
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0
⊢ False
specialize h u rfl
case intro.intro
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
h : coeff u φ = 0
hu : ¬↑φ u = 0
⊢ False
case intro.intro
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
⊢ False
simp at h hu
no goals
case intro.intro
σ : Type u_1
τ : Type u_3
α : Type ?u.944555
R : Type u_2
S : Type ?u.944561
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
h : coeff u φ = 0
hu : ¬↑φ u = 0
⊢ False
contradiction