-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem eval₂Hom_congr' {f₁ f₂ : R →+* S} {g₁ g₂ : σ → S} {p₁ p₂ : MvPolynomial σ R} :
    f₁ = f₂ →
      (∀ i, i ∈ p₁.vars → i ∈ p₂.vars → g₁ i = g₂ i) →
        p₁ = p₂ → eval₂Hom f₁ g₁ p₁ = eval₂Hom f₂ g₂ p₂

Proof state:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ ∀ x ∈ d.support, g₁ x ^ d x = g₂ x ^ d x

Tactic:
intro i hi

Result:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ g₁ i ^ d i = g₂ i ^ d i

Proof state:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ (d.prod fun i k => g₁ i ^ k) = d.prod fun i k => g₂ i ^ k

Tactic:
simp only [Finsupp.prod]

Result:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ ∏ x ∈ d.support, g₁ x ^ d x = ∏ x ∈ d.support, g₂ x ^ d x

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₂) p₁

Tactic:
rw [p₁.as_sum]

Result:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (eval₂Hom f₁ g₁) (∑ v ∈ p₁.support, (monomial v) (coeff v p₁)) =
    (eval₂Hom f₁ g₂) (∑ v ∈ p₁.support, (monomial v) (coeff v p₁))

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ i ∈ p₁.vars

Tactic:
rw [mem_vars]

Result:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p₁.support, i ∈ d.support

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ ∀ x ∈ p₁.support, (f₁ (coeff x p₁) * x.prod fun i k => g₁ i ^ k) = f₁ (coeff x p₁) * x.prod fun i k => g₂ i ^ k

Tactic:
intro d hd

Result:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ (f₁ (coeff d p₁) * d.prod fun i k => g₁ i ^ k) = f₁ (coeff d p₁) * d.prod fun i k => g₂ i ^ k

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p₁.support, i ∈ d.support

Tactic:
exact ⟨d, hd, hi⟩

Result:
no goals

Proof state:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ ∏ x ∈ d.support, g₁ x ^ d x = ∏ x ∈ d.support, g₂ x ^ d x

Tactic:
apply Finset.prod_congr rfl

Result:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ ∀ x ∈ d.support, g₁ x ^ d x = g₂ x ^ d x

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (∑ x ∈ p₁.support, f₁ (coeff x p₁) * x.prod fun i k => g₁ i ^ k) =
    ∑ x ∈ p₁.support, f₁ (coeff x p₁) * x.prod fun i k => g₂ i ^ k

Tactic:
apply Finset.sum_congr rfl

Result:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ ∀ x ∈ p₁.support, (f₁ (coeff x p₁) * x.prod fun i k => g₁ i ^ k) = f₁ (coeff x p₁) * x.prod fun i k => g₂ i ^ k

Proof state:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
this : i ∈ p₁.vars
⊢ g₁ i ^ d i = g₂ i ^ d i

Tactic:
rw [h i this this]

Result:
no goals

Proof state:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ g₁ i ^ d i = g₂ i ^ d i

Tactic:
have : i ∈ p₁.vars := by
  rw [mem_vars]
  exact ⟨d, hd, hi⟩

Result:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
this : i ∈ p₁.vars
⊢ g₁ i ^ d i = g₂ i ^ d i

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R →+* S
g₁ g₂ : σ → S
p₁ p₂ : MvPolynomial σ R
⊢ f₁ = f₂ → (∀ i ∈ p₁.vars, i ∈ p₂.vars → g₁ i = g₂ i) → p₁ = p₂ → (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₂ g₂) p₂

Tactic:
rintro rfl h rfl

Result:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₂) p₁

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ (f₁ (coeff d p₁) * d.prod fun i k => g₁ i ^ k) = f₁ (coeff d p₁) * d.prod fun i k => g₂ i ^ k

Tactic:
congr 1

Result:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ (d.prod fun i k => g₁ i ^ k) = d.prod fun i k => g₂ i ^ k

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (eval₂Hom f₁ g₁) (∑ v ∈ p₁.support, (monomial v) (coeff v p₁)) =
    (eval₂Hom f₁ g₂) (∑ v ∈ p₁.support, (monomial v) (coeff v p₁))

Tactic:
simp only [map_sum, eval₂Hom_monomial]

Result:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (∑ x ∈ p₁.support, f₁ (coeff x p₁) * x.prod fun i k => g₁ i ^ k) =
    ∑ x ∈ p₁.support, f₁ (coeff x p₁) * x.prod fun i k => g₂ i ^ k