-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_rename_le (f : σ → τ) (p : MvPolynomial σ R) :
    (rename f p).totalDegree ≤ p.totalDegree :=
  Finset.sup_le fun b => by
    classical
    intro h
    rw [rename_eq] at h
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (b.sum fun x e => e) ≤ p.totalDegree

Tactic:
have h' := Finsupp.mapDomain_support h

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support
⊢ (b.sum fun x e => e) ≤ p.totalDegree

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
⊢ b ∈ ((rename f) p).support → (b.sum fun x e => e) ≤ p.totalDegree

Tactic:
classical
intro h
rw [rename_eq] at h
have h' := Finsupp.mapDomain_support h
rw [Finset.mem_image] at h'
rcases h' with ⟨s, hs, rfl⟩
exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support
⊢ (b.sum fun x e => e) ≤ p.totalDegree

Tactic:
rw [Finset.mem_image] at h'

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : ∃ a ∈ p.support, Finsupp.mapDomain f a = b
⊢ (b.sum fun x e => e) ≤ p.totalDegree

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
⊢ b ∈ ((rename f) p).support → (b.sum fun x e => e) ≤ p.totalDegree

Tactic:
intro h

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ ((rename f) p).support
⊢ (b.sum fun x e => e) ≤ p.totalDegree

Proof state:
case intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ ((Finsupp.mapDomain f s).sum fun x e => e) ≤ p.totalDegree

Tactic:
exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ ((rename f) p).support
⊢ (b.sum fun x e => e) ≤ p.totalDegree

Tactic:
rw [rename_eq] at h

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (b.sum fun x e => e) ≤ p.totalDegree

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : ∃ a ∈ p.support, Finsupp.mapDomain f a = b
⊢ (b.sum fun x e => e) ≤ p.totalDegree

Tactic:
rcases h' with ⟨s, hs, rfl⟩

Result:
case intro.intro
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ ((Finsupp.mapDomain f s).sum fun x e => e) ≤ p.totalDegree