-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem coeff_rename_eq_zero (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ)
    (h : ∀ u : σ →₀ ℕ, u.mapDomain f = d → φ.coeff u = 0) : (rename f φ).coeff d = 0

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d
⊢ False

Tactic:
obtain ⟨u, hu, rfl⟩ := H

Result:
case intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0
⊢ False

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)

Tactic:
intro H

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
⊢ False

Proof state:
case intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
⊢ False

Tactic:
simp only [Finsupp.mem_support_iff, ne_eq] at h hu

Result:
case intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
h : coeff u φ = 0
hu : ¬φ u = 0
⊢ False

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d ((rename f) φ) = 0

Tactic:
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 says simp only [Finsupp.mem_support_iff, ne_eq] at h hu
contradiction

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d ((rename f) φ) = 0

Tactic:
rw [rename_eq, ← not_mem_support_iff]

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)

Proof state:
case intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0
⊢ False

Tactic:
specialize h u rfl

Result:
case intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
⊢ False

Proof state:
case intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
h : coeff u φ = 0
hu : ¬φ u = 0
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support
⊢ False

Tactic:
rw [Finset.mem_image] at H

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d
⊢ False

Proof state:
case intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
⊢ False

Tactic:
simp? at h hu says simp only [Finsupp.mem_support_iff, ne_eq] at h hu

Result:
case intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
h : coeff u φ = 0
hu : ¬φ u = 0
⊢ False

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
⊢ False

Tactic:
replace H := mapDomain_support H

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support
⊢ False