-- Mathlib/Algebra/MvPolynomial/Variables.lean
lemma aeval_ite_mem_eq_self (q : MvPolynomial σ R) {s : Set σ} (hs : q.vars.toSet ⊆ s)
    [∀ i, Decidable (i ∈ s)] :
    MvPolynomial.aeval (fun i ↦ if i ∈ s then .X i else 0) q = q

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ ∑ i ∈ q.support, (aeval fun i => if i ∈ s then X i else 0) ((monomial i) (coeff i q)) =
    ∑ v ∈ q.support, (monomial v) (coeff v q)

Tactic:
refine Finset.sum_congr rfl fun u hu ↦ ?_

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ (aeval fun i => if i ∈ s then X i else 0) ((monomial u) (coeff u q)) = (monomial u) (coeff u q)

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
i : σ
hi : i ∈ u.support
⊢ (if i ∈ s then X i else 0) ^ u i = X i ^ u i

Tactic:
simp [hs ((MvPolynomial.mem_vars _).mpr ⟨u, hu, hi⟩)]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ ((algebraMap R (MvPolynomial σ R)) (coeff u q) * u.prod fun i k => (if i ∈ s then X i else 0) ^ k) =
    C (coeff u q) * u.prod fun n e => X n ^ e

Tactic:
congr 1

Result:
case e_a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ (u.prod fun i k => (if i ∈ s then X i else 0) ^ k) = u.prod fun n e => X n ^ e

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ (aeval fun i => if i ∈ s then X i else 0) ((monomial u) (coeff u q)) = (monomial u) (coeff u q)

Tactic:
rw [MvPolynomial.aeval_monomial, MvPolynomial.monomial_eq]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ ((algebraMap R (MvPolynomial σ R)) (coeff u q) * u.prod fun i k => (if i ∈ s then X i else 0) ^ k) =
    C (coeff u q) * u.prod fun n e => X n ^ e

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ (aeval fun i => if i ∈ s then X i else 0) q = q

Tactic:
rw [MvPolynomial.as_sum q, MvPolynomial.aeval_sum]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ ∑ i ∈ q.support, (aeval fun i => if i ∈ s then X i else 0) ((monomial i) (coeff i q)) =
    ∑ v ∈ q.support, (monomial v) (coeff v q)

Proof state:
case e_a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ (u.prod fun i k => (if i ∈ s then X i else 0) ^ k) = u.prod fun n e => X n ^ e

Tactic:
exact Finsupp.prod_congr (fun i hi ↦ by simp [hs ((MvPolynomial.mem_vars _).mpr ⟨u, hu, hi⟩)])

Result:
no goals