no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f
classical
repeat' rw [degreeOf_eq_sup (R:=R) i]
rw [support_mul_X]
simp only [Finset.sup_map]
congr
ext
simp only [Finsupp.single, Nat.one_ne_zero, add_right_eq_self, addRightEmbedding_apply, coe_mk,
  Pi.add_apply, comp_apply, ite_eq_right_iff, Finsupp.coe_add, Pi.single_eq_of_ne h]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (support (f * X j)) fun m => ↑m i) = Finset.sup (support f) fun m => ↑m i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f
repeat' rw [degreeOf_eq_sup (R:=R) i]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (Finset.map (addRightEmbedding (Finsupp.single j 1)) (support f)) fun m => ↑m i) =
    Finset.sup (support f) fun m => ↑m i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (support (f * X j)) fun m => ↑m i) = Finset.sup (support f) fun m => ↑m i
rw [support_mul_X]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ Finset.sup (support f) ((fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1))) =
    Finset.sup (support f) fun m => ↑m i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (Finset.map (addRightEmbedding (Finsupp.single j 1)) (support f)) fun m => ↑m i) =
    Finset.sup (support f) fun m => ↑m i
simp only [Finset.sup_map]
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1)) = fun m => ↑m i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ Finset.sup (support f) ((fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1))) =
    Finset.sup (support f) fun m => ↑m i
congr
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
x✝ : σ →₀ ℕ
⊢ ((fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1))) x✝ = ↑x✝ i
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1)) = fun m => ↑m i
ext
no goals
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
x✝ : σ →₀ ℕ
⊢ ((fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1))) x✝ = ↑x✝ i
simp only [Finsupp.single, Nat.one_ne_zero, add_right_eq_self, addRightEmbedding_apply, coe_mk,
  Pi.add_apply, comp_apply, ite_eq_right_iff, Finsupp.coe_add, Pi.single_eq_of_ne h]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (support (f * X j)) fun m => ↑m i) = Finset.sup (support f) fun m => ↑m i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.313675
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (support (f * X j)) fun m => ↑m i) = Finset.sup (support f) fun m => ↑m i
rw [degreeOf_eq_sup (R:=R) i]