-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_rename (f : σ → τ) (φ : MvPolynomial σ R) :
    (rename f φ).degrees ⊆ φ.degrees.map f

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
⊢ ((rename f) φ).degrees ⊆ Multiset.map f φ.degrees

Tactic:
classical
intro i
rw [mem_degrees, Multiset.mem_map]
rintro ⟨d, hd, hi⟩
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
rw [sum_apply, Finsupp.sum] at hi
contrapose! hi
rw [Finset.sum_eq_zero]
intro j hj
simp only [exists_prop, mem_degrees] at hi
specialize hi j ⟨x, hx, hj⟩
rw [Finsupp.single_apply, if_neg hi]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
j : σ
hj : j ∈ x.support
⊢ (Finsupp.single (f j) (x j)) i = 0

Tactic:
simp only [exists_prop, mem_degrees] at hi

Result:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : ∀ (a : σ), (∃ d, coeff d φ ≠ 0 ∧ a ∈ d.support) → f a ≠ i
⊢ (Finsupp.single (f j) (x j)) i = 0

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ (∃ d, coeff d ((rename f) φ) ≠ 0 ∧ i ∈ d.support) → ∃ a ∈ φ.degrees, f a = i

Tactic:
rintro ⟨d, hd, hi⟩

Result:
case intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : coeff d ((rename f) φ) ≠ 0
hi : i ∈ d.support
⊢ ∃ a ∈ φ.degrees, f a = i

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∀ x_1 ∈ x.support, (Finsupp.single (f x_1) (x x_1)) i = 0

Tactic:
intro j hj

Result:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
j : σ
hj : j ∈ x.support
⊢ (Finsupp.single (f j) (x j)) i = 0

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : ∀ (a : σ), (∃ d, coeff d φ ≠ 0 ∧ a ∈ d.support) → f a ≠ i
⊢ (Finsupp.single (f j) (x j)) i = 0

Tactic:
specialize hi j ⟨x, hx, hj⟩

Result:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
⊢ (Finsupp.single (f j) (x j)) i = 0

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
⊢ (Finsupp.single (f j) (x j)) i = 0

Tactic:
rw [Finsupp.single_apply, if_neg hi]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : (x.sum fun a => Finsupp.single (f a)) i ≠ 0
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
rw [sum_apply, Finsupp.sum] at hi

Result:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∑ a ∈ x.support, (Finsupp.single (f a) (x a)) i ≠ 0
⊢ ∃ a ∈ φ.degrees, f a = i

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : i ∈ (Finsupp.mapDomain f x).support
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi

Result:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : (x.sum fun a => Finsupp.single (f a)) i ≠ 0
⊢ ∃ a ∈ φ.degrees, f a = i

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ i ∈ ((rename f) φ).degrees → i ∈ Multiset.map f φ.degrees

Tactic:
rw [mem_degrees, Multiset.mem_map]

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ (∃ d, coeff d ((rename f) φ) ≠ 0 ∧ i ∈ d.support) → ∃ a ∈ φ.degrees, f a = i

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∑ a ∈ x.support, (Finsupp.single (f a) (x a)) i = 0

Tactic:
rw [Finset.sum_eq_zero]

Result:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∀ x_1 ∈ x.support, (Finsupp.single (f x_1) (x x_1)) i = 0

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∑ a ∈ x.support, (Finsupp.single (f a) (x a)) i ≠ 0
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
contrapose! hi

Result:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∑ a ∈ x.support, (Finsupp.single (f a) (x a)) i = 0

Proof state:
case intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : coeff d ((rename f) φ) ≠ 0
hi : i ∈ d.support
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd

Result:
case intro.intro.intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : i ∈ (Finsupp.mapDomain f x).support
⊢ ∃ a ∈ φ.degrees, f a = i

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
⊢ ((rename f) φ).degrees ⊆ Multiset.map f φ.degrees

Tactic:
intro i

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ i ∈ ((rename f) φ).degrees → i ∈ Multiset.map f φ.degrees