no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
⊢ b ∈ support (↑(rename f) p) → (sum b fun x e => e) ≤ totalDegree p
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⟩
rw [Finsupp.sum_mapDomain_index]
exact le_trans le_rfl (le_totalDegree hs)
exact fun _ => rfl
exact fun _ _ _ => rfl
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (↑(rename f) p)
⊢ (sum b fun x e => e) ≤ totalDegree p
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
⊢ b ∈ support (↑(rename f) p) → (sum b fun x e => e) ≤ totalDegree p
intro h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum b fun x e => e) ≤ totalDegree p
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (↑(rename f) p)
⊢ (sum b fun x e => e) ≤ totalDegree p
rw [rename_eq] at h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support
⊢ (sum b fun x e => e) ≤ totalDegree p
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum b fun x e => e) ≤ totalDegree p
have h' := Finsupp.mapDomain_support h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : ∃ a, a ∈ p.support ∧ Finsupp.mapDomain f a = b
⊢ (sum b fun x e => e) ≤ totalDegree p
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support
⊢ (sum b fun x e => e) ≤ totalDegree p
rw [Finset.mem_image] at h'
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum (Finsupp.mapDomain f s) fun x e => e) ≤ totalDegree p
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : ∃ a, a ∈ p.support ∧ Finsupp.mapDomain f a = b
⊢ (sum b fun x e => e) ≤ totalDegree p
rcases h' with ⟨s, hs, rfl⟩
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum s fun a m => m) ≤ totalDegree p

case intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → 0 = 0

case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum (Finsupp.mapDomain f s) fun x e => e) ≤ totalDegree p
rw [Finsupp.sum_mapDomain_index]
case intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → 0 = 0

case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum s fun a m => m) ≤ totalDegree p

case intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → 0 = 0

case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
exact le_trans le_rfl (le_totalDegree hs)
case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
case intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → 0 = 0

case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
exact fun _ => rfl
no goals
case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
exact fun _ _ _ => rfl