awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∉ p.support
d : σ →₀ ℕ
hd : d ∈ p.support
rw : ¬d = 0
⊢ d.support.Nonempty

Tactic:
rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]

Premises used: Ne, Finset.nonempty_iff_ne_empty, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∉ p.support
hd : 0 ∈ p.support
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
pos :
  ∀ (i : σ) (hi : i ∈ d.support),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0

Tactic:
obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) := by
      rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0
      rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]
      rintro rfl
      contradiction

Premises used: Finsupp.support, Finset.Nonempty
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
pos : HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0

Tactic:
rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]

Premises used: MulZeroClass.mul_zero, Finset.prod_eq_zero, Finsupp.prod
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
pos : i ∈ p.vars
⊢ HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0

Tactic:
rw [hp, zero_pow (Finsupp.mem_support_iff.1 hi)]

Premises used: Finsupp.mem_support_iff, Iff.mp, zero_pow
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
pos : ∃ d ∈ p.support, i ∈ d.support
⊢ i ∈ p.vars

Tactic:
rw [mem_vars_iff_mem_support]

Premises used: MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p.support, i ∈ d.support

Tactic:
⟨d, hd, hi⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p.support, i ∈ d.support

Tactic:
exact ⟨d, hd, hi⟩
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
rw : ∀ (h0 : ¬0 ∉ p.support) (d : σ →₀ ℕ) (hd : d ∈ p.support) (hd0 : d ≠ 0), d.support.Nonempty
⊢ d.support.Nonempty

Tactic:
rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0

Premises used: Finsupp.notMem_support_iff, MvPolynomial.coeff, MvPolynomial.constantCoeff_eq
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬0 ∉ p.support
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
rw : ¬d = 0
⊢ d.support.Nonempty

Tactic:
rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]

Premises used: Ne, Finset.nonempty_iff_ne_empty, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬0 ∉ p.support
hd : 0 ∈ p.support
hd0 : Ne.{u_1 + 1} (α := σ →₀ ℕ) 0 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
neg :
  ∀ (i : σ) (hi : i ∈ d.support),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0

Tactic:
obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) := by
      rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0
      rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]
      rintro rfl
      contradiction

Premises used: Finsupp.support, Finset.Nonempty
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
neg : HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0

Tactic:
rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]

Premises used: MulZeroClass.mul_zero, Finset.prod_eq_zero, Finsupp.prod
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
neg : i ∈ p.vars
⊢ HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0

Tactic:
rw [hp, zero_pow (Finsupp.mem_support_iff.1 hi)]

Premises used: Finsupp.mem_support_iff, Iff.mp, zero_pow
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
neg : ∃ d ∈ p.support, i ∈ d.support
⊢ i ∈ p.vars

Tactic:
rw [mem_vars_iff_mem_support]

Premises used: MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p.support, i ∈ d.support

Tactic:
⟨d, hd, hi⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p.support, i ∈ d.support

Tactic:
exact ⟨d, hd, hi⟩
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
⊢ Eq.{v + 1} (α := S) ((aeval g : (a : MvPolynomial σ R) → S) p : S)
    ((algebraMap R S : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
eval₂Hom_eq_constantCoeff_of_vars _ hp

Premises used: MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
rw :
  Eq.{v + 1} (α := S)
    ((eval₂Hom f₁ g₁ : (a : MvPolynomial σ R) → S)
        (∑ v ∈ p₁.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p₁)) :
      S)
    ((eval₂Hom f₁ g₂ : (a : MvPolynomial σ R) → S)
        (∑ v ∈ p₁.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p₁)) :
      S)
⊢ Eq.{v + 1} (α := S) ((eval₂Hom f₁ g₁ : (a : MvPolynomial σ R) → S) p₁ : S)
    ((eval₂Hom f₁ g₂ : (a : MvPolynomial σ R) → S) p₁ : S)

Tactic:
rw [p₁.as_sum]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
simp :
  Eq.{v + 1} (α := S)
    (∑ x ∈ p₁.support,
      HMul.hMul (α := S) (β := S) ((f₁ : (a : R) → S) (coeff x p₁) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g₁ i ^ k : S))
    (∑ x ∈ p₁.support,
      HMul.hMul (α := S) (β := S) ((f₁ : (a : R) → S) (coeff x p₁) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g₂ i ^ k : S))
⊢ Eq.{v + 1} (α := S)
    ((eval₂Hom f₁ g₁ : (a : MvPolynomial σ R) → S)
        (∑ v ∈ p₁.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p₁)) :
      S)
    ((eval₂Hom f₁ g₂ : (a : MvPolynomial σ R) → S)
        (∑ v ∈ p₁.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p₁)) :
      S)

Tactic:
simp only [map_sum, eval₂Hom_monomial]

Premises used: MvPolynomial.eval₂Hom_monomial, map_sum
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
apply :
  ∀ x ∈ p₁.support,
    HMul.hMul (α := S) (β := S) ((f₁ : (a : R) → S) (coeff x p₁) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g₁ i ^ k : S) =
      HMul.hMul (α := S) (β := S) ((f₁ : (a : R) → S) (coeff x p₁) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g₂ i ^ k : S)
⊢ Eq.{v + 1} (α := S)
    (∑ x ∈ p₁.support,
      HMul.hMul (α := S) (β := S) ((f₁ : (a : R) → S) (coeff x p₁) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g₁ i ^ k : S))
    (∑ x ∈ p₁.support,
      HMul.hMul (α := S) (β := S) ((f₁ : (a : R) → S) (coeff x p₁) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g₂ i ^ k : S))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : 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
e_a : Eq.{v + 1} (α := S) (d.prod fun (i : σ) (k : ℕ) ↦ g₁ i ^ k) (d.prod fun (i : σ) (k : ℕ) ↦ g₂ i ^ k)
⊢ HMul.hMul (α := S) (β := S) ((f₁ : (a : R) → S) (coeff d p₁) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g₁ i ^ k : S) =
    HMul.hMul (α := S) (β := S) ((f₁ : (a : R) → S) (coeff d p₁) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g₂ i ^ k : S)

Tactic:
congr 1
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : 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
e_a :
  ∀ x ∈ d.support,
    HPow.hPow (β := ℕ) (g₁ x) ((d : (a : σ) → ℕ) x : ℕ) = HPow.hPow (β := ℕ) (g₂ x) ((d : (a : σ) → ℕ) x : ℕ)
⊢ Eq.{v + 1} (α := S) (∏ x ∈ d.support, HPow.hPow (β := ℕ) (g₁ x) ((d : (a : σ) → ℕ) x : ℕ))
    (∏ x ∈ d.support, HPow.hPow (β := ℕ) (g₂ x) ((d : (a : σ) → ℕ) x : ℕ))

Tactic:
apply Finset.prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : 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
rw : ∃ d ∈ p₁.support, i ∈ d.support
⊢ i ∈ p₁.vars

Tactic:
rw [mem_vars_iff_mem_support]

Premises used: MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : 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:
⟨d, hd, hi⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : 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⟩
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : 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:
have : i ∈ p₁.vars := by
    rw [mem_vars_iff_mem_support]
    exact ⟨d, hd, hi⟩
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : 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
e_a e_a₁ : HPow.hPow (β := ℕ) (g₂ i) ((d : (a : σ) → ℕ) i : ℕ) = HPow.hPow (β := ℕ) (g₂ i) ((d : (a : σ) → ℕ) i : ℕ)
⊢ HPow.hPow (β := ℕ) (g₁ i) ((d : (a : σ) → ℕ) i : ℕ) = HPow.hPow (β := ℕ) (g₂ i) ((d : (a : σ) → ℕ) i : ℕ)

Tactic:
rw [h i this this]
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv :
  ∀ i ∈ p₁.vars,
    i ∈ p₂.vars →
      Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S) ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
hp : p₁ = p₂
hC₁ :
  ∀ (x : R),
    Eq.{v + 1} (α := S) ((f₁.comp C : (a : R) → S) x : S)
      ((RingHom.comp (β := MvPolynomial σ R)
              (eval₂Hom (f₁.comp C) (comp (β := MvPolynomial σ R) (⇑f₁ : (a : MvPolynomial σ R) → S) X)) C :
            (a : R) → S)
          x :
        S)
hX :
  ∀ (i : σ),
    Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S)
      ((eval₂Hom (f₁.comp C) (comp (β := MvPolynomial σ R) (⇑f₁ : (a : MvPolynomial σ R) → S) X) :
            (a : MvPolynomial σ R) → S)
          (X i) :
        S)
⊢ f₁ = eval₂Hom (f₁.comp C) (comp (β := MvPolynomial σ R) (⇑f₁ : (a : MvPolynomial σ R) → S) X)

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv :
  ∀ i ∈ p₁.vars,
    i ∈ p₂.vars →
      Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S) ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
hp : p₁ = p₂
x : R
⊢ Eq.{v + 1} (α := S) ((f₁.comp C : (a : R) → S) x : S)
    ((RingHom.comp (β := MvPolynomial σ R)
            (eval₂Hom (f₁.comp C) (comp (β := MvPolynomial σ R) (⇑f₁ : (a : MvPolynomial σ R) → S) X)) C :
          (a : R) → S)
        x :
      S)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv :
  ∀ i ∈ p₁.vars,
    i ∈ p₂.vars →
      Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S) ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
hp : p₁ = p₂
i : σ
⊢ Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S)
    ((eval₂Hom (f₁.comp C) (comp (β := MvPolynomial σ R) (⇑f₁ : (a : MvPolynomial σ R) → S) X) :
          (a : MvPolynomial σ R) → S)
        (X i) :
      S)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv :
  ∀ i ∈ p₁.vars,
    i ∈ p₂.vars →
      Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S) ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
hp : p₁ = p₂
hC₁ :
  ∀ (x : R),
    Eq.{v + 1} (α := S)
      ((RingHom.comp (β := MvPolynomial σ R)
              (eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X)) C :
            (a : R) → S)
          x :
        S)
      ((f₂.comp C : (a : R) → S) x : S)
hX :
  ∀ (i : σ),
    Eq.{v + 1} (α := S)
      ((eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X) :
            (a : MvPolynomial σ R) → S)
          (X i) :
        S)
      ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
⊢ eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X) = f₂

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv :
  ∀ i ∈ p₁.vars,
    i ∈ p₂.vars →
      Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S) ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
hp : p₁ = p₂
x : R
⊢ Eq.{v + 1} (α := S)
    ((RingHom.comp (β := MvPolynomial σ R)
            (eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X)) C :
          (a : R) → S)
        x :
      S)
    ((f₂.comp C : (a : R) → S) x : S)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv :
  ∀ i ∈ p₁.vars,
    i ∈ p₂.vars →
      Eq.{v + 1} (α := S) ((f₁ : (a : MvPolynomial σ R) → S) (X i) : S) ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)
hp : p₁ = p₂
i : σ
⊢ Eq.{v + 1} (α := S)
    ((eval₂Hom (f₂.comp C) (comp (β := MvPolynomial σ R) (⇑f₂ : (a : MvPolynomial σ R) → S) X) :
          (a : MvPolynomial σ R) → S)
        (X i) :
      S)
    ((f₂ : (a : MvPolynomial σ R) → S) (X i) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
change :
  Eq (α := MvPolynomial σ R)
    ((RingHom.comp (AlgHom.toRingHom (rename f))
            (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        p :
      MvPolynomial σ R)
    ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
⊢ (rename f : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i) : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    p

Tactic:
change (rename f).toRingHom.comp _ p = RingHom.id _ p

Premises used: RingHom.comp, MvPolynomial.rename, AlgHom.toRingHom, RingHom.id, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
⊢ Eq (α := MvPolynomial σ R)
    ((RingHom.comp (AlgHom.toRingHom (rename f))
            (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        p :
      MvPolynomial σ R)
    ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)

Tactic:
hom_congr_vars ?_ ?_ ?_

Premises used: MvPolynomial.hom_congr_vars
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
refine_1 :
  Eq (α := R →+* MvPolynomial σ R)
    (RingHom.comp (β := MvPolynomial σ R)
      (RingHom.comp (AlgHom.toRingHom (rename f))
        (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))))
      C)
    (RingHom.comp (RingHom.id (MvPolynomial σ R)) C)
refine_2 :
  ∀ i ∈ p.vars,
    i ∈ p.vars →
      Eq (α := MvPolynomial σ R)
        ((RingHom.comp (AlgHom.toRingHom (rename f))
                (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
              (a : MvPolynomial σ R) → MvPolynomial σ R)
            (X i) :
          MvPolynomial σ R)
        ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
refine_3 : p = p
⊢ Eq (α := MvPolynomial σ R)
    ((RingHom.comp (AlgHom.toRingHom (rename f))
            (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        p :
      MvPolynomial σ R)
    ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)

Tactic:
refine hom_congr_vars ?_ ?_ ?_

Premises used: MvPolynomial.hom_congr_vars
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : (↑p.vars : Set σ) ⊆ range f
refine_1 :
  ∀ (x : R),
    Eq (α := MvPolynomial σ R)
      ((RingHom.comp (β := MvPolynomial σ R)
              (RingHom.comp (AlgHom.toRingHom (rename f))
                (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))))
              C :
            (a : R) → MvPolynomial σ R)
          x :
        MvPolynomial σ R)
      ((RingHom.comp (RingHom.id (MvPolynomial σ R)) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
⊢ Eq (α := R →+* MvPolynomial σ R)
    (RingHom.comp (β := MvPolynomial σ R)
      (RingHom.comp (AlgHom.toRingHom (rename f))
        (AlgHom.toRingHom (aeval fun (i : σ) ↦ Option.elim' 0 X (partialInv f i))))
      C)
    (RingHom.comp (RingHom.id (MvPolynomial σ R)) C)

Tactic:
ext1