awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have pos : ∀ (h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)),
  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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
Tactic: by_cases h0 : constantCoeff p = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
pos :
  ∀ (h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)),
    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) :
        S)
      ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have neg : ∀ (h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)),
  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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
Tactic: by_cases h0 : constantCoeff p = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
⊢ 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have pos : ∀ x ∈ p.support,
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
Tactic: rw [h0, f.map_zero, Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
⊢ 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have pos : ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support),
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
Tactic: on_goal 1 =>
    rw [h0, f.map_zero, Finset.sum_eq_zero]
    intro d hd
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
⊢ 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have neg : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
  (f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)
Tactic: rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
neg :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
    (f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)
⊢ 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have neg₁ : ∀ b ∈ p.support,
  b ≠ 0 → HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff b p) : S) (b.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
Tactic: rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
neg :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
    (f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)
neg₁ :
  ∀ b ∈ p.support,
    b ≠ 0 →
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff b p) : S) (b.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
⊢ 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have neg₂ : 0 ∉ p.support →
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
Tactic: rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
    (f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)
have neg : Eq.{v + 1} (α := S) ((f : (a : R) → S) (coeff 0 p) : S)
  ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
Tactic: rw [Finsupp.prod_zero_index, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
⊢ 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have neg : ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support) (hd0 : d ≠ 0),
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
Tactic: on_goal 2 =>
    rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
    · rw [Finsupp.prod_zero_index, mul_one]
      rfl
    on_goal 1 => intro d hd hd0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
neg :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support) (hd0 : d ≠ 0),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
⊢ 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) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have neg₁ : 0 ∉ p.support →
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
Tactic: on_goal 2 =>
    rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
    · rw [Finsupp.prod_zero_index, mul_one]
      rfl
    on_goal 1 => intro d hd hd0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (hypothesis)
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)
⊢ 0 ∉ p.support →
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
      0
have h0₁ : 0 ∈ p.support
Tactic: rw [constantCoeff_eq, coeff, ← Ne, ← Finsupp.mem_support_iff] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ d.support.Nonempty
have rw : ∀ (h0 : 0 ∉ p.support) (d : σ →₀ ℕ) (hd : d ∈ p.support), d.support.Nonempty
Tactic: rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0
Cleared hypotheses: h0, d, hd
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ d.support.Nonempty
have rw : ¬d = 0
Tactic: rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
have pos : HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0
Tactic: rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0
have pos : i ∈ p.vars
Tactic: rw [hp, zero_pow (Finsupp.mem_support_iff.1 hi)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ i ∈ p.vars
have pos : ∃ d ∈ p.support, i ∈ d.support
Tactic: rw [mem_vars_iff_mem_support]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ d.support.Nonempty
have rw : ∀ (h0 : ¬0 ∉ p.support) (d : σ →₀ ℕ) (hd : d ∈ p.support) (hd0 : d ≠ 0), d.support.Nonempty
Tactic: rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0
Cleared hypotheses: h0, d, hd, hd0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ d.support.Nonempty
have rw : ¬d = 0
Tactic: rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
have neg : HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0
Tactic: rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0
have neg : i ∈ p.vars
Tactic: rw [hp, zero_pow (Finsupp.mem_support_iff.1 hi)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ i ∈ p.vars
have neg : ∃ d ∈ p.support, i ∈ d.support
Tactic: rw [mem_vars_iff_mem_support]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ Eq.{v + 1} (α := S) ((eval₂Hom f₁ g₁ : (a : MvPolynomial σ R) → S) p₁ : S)
    ((eval₂Hom f₁ g₂ : (a : MvPolynomial σ R) → S) p₁ : S)
have 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)
Tactic: rw [p₁.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ 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)
have 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))
Tactic: simp only [map_sum, eval₂Hom_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ 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))
have 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)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ 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)
have e_a : Eq.{v + 1} (α := S) (d.prod fun (i : σ) (k : ℕ) ↦ g₁ i ^ k) (d.prod fun (i : σ) (k : ℕ) ↦ g₂ i ^ k)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ Eq.{v + 1} (α := S) (∏ x ∈ d.support, HPow.hPow (β := ℕ) (g₁ x) ((d : (a : σ) → ℕ) x : ℕ))
    (∏ x ∈ d.support, HPow.hPow (β := ℕ) (g₂ x) ((d : (a : σ) → ℕ) x : ℕ))
have e_a : ∀ x ∈ d.support,
  HPow.hPow (β := ℕ) (g₁ x) ((d : (a : σ) → ℕ) x : ℕ) = HPow.hPow (β := ℕ) (g₂ x) ((d : (a : σ) → ℕ) x : ℕ)
Tactic: apply Finset.prod_congr rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
have rw : ∃ d ∈ p₁.support, i ∈ d.support
Tactic: rw [mem_vars_iff_mem_support]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (hypothesis)
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
⊢ HPow.hPow (β := ℕ) (g₁ i) ((d : (a : σ) → ℕ) i : ℕ) = HPow.hPow (β := ℕ) (g₂ i) ((d : (a : σ) → ℕ) i : ℕ)
have this : i ∈ p₁.vars
Tactic: have : i ∈ p₁.vars := by
    rw [mem_vars_iff_mem_support]
    exact ⟨d, hd, hi⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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
⊢ HPow.hPow (β := ℕ) (g₁ i) ((d : (a : σ) → ℕ) i : ℕ) = HPow.hPow (β := ℕ) (g₂ i) ((d : (a : σ) → ℕ) i : ℕ)
have e_a : HPow.hPow (β := ℕ) (g₂ i) ((d : (a : σ) → ℕ) i : ℕ) = HPow.hPow (β := ℕ) (g₂ i) ((d : (a : σ) → ℕ) i : ℕ)
Tactic: rw [h i this this]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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₂
⊢ f₁ = eval₂Hom (f₁.comp C) (comp (β := MvPolynomial σ R) (⇑f₁ : (a : MvPolynomial σ R) → S) X)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
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)
⊢ f₁ = eval₂Hom (f₁.comp C) (comp (β := MvPolynomial σ R) (⇑f₁ : (a : MvPolynomial σ R) → S) X)
have 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)
Tactic: ext