awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
rw : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ • n
rw₁ : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ * n
⊢ n * Fintype.card σ = ∑ _s : σ, n
have rw₂ : Fintype.card σ * n = Finset.card.{u_1} (α := σ) Finset.univ * n
Tactic: rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
rw : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ • n
rw₁ : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ * n
rw₂ : Fintype.card σ * n = Finset.card.{u_1} (α := σ) Finset.univ * n
⊢ n * Fintype.card σ = ∑ _s : σ, n
have rw₃ : Fintype.card σ * n = Fintype.card σ * n
Tactic: rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
⊢ LE.le (α := ℕ) (∑ s : σ, (d : (a : σ) → ℕ) s) (d.sum fun (x : σ) (e : ℕ) ↦ e)
have h₁ : ∀ (i : σ), Eq (α := ℕ) 0 0
Tactic: rw [Finsupp.sum_fintype]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
⊢ n * Fintype.card σ ≤ f.totalDegree
have n₁ : n * Fintype.card σ = ∑ _s : σ, n
Tactic: calc
    n * Fintype.card σ = ∑ _s : σ, n := by
      rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
    _ ≤ ∑ s, d s := Finset.sum_le_sum fun s _ => h s
    _ ≤ d.sum fun _ e => e := by
      rw [Finsupp.sum_fintype]
      intros
      rfl
    _ ≤ f.totalDegree := le_totalDegree hd
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
n₁ : n * Fintype.card σ = ∑ _s : σ, n
⊢ n * Fintype.card σ ≤ f.totalDegree
have n₂ : LE.le (α := ℕ) (∑ s : σ, (d : (a : σ) → ℕ) s) (d.sum fun (x : σ) (e : ℕ) ↦ e)
Tactic: calc
    n * Fintype.card σ = ∑ _s : σ, n := by
      rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
    _ ≤ ∑ s, d s := Finset.sum_le_sum fun s _ => h s
    _ ≤ d.sum fun _ e => e := by
      rw [Finsupp.sum_fintype]
      intros
      rfl
    _ ≤ f.totalDegree := le_totalDegree hd
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, (d : (a : σ) → ℕ) i
⊢ coeff d f = 0
have rw : ∀ (h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
  coeff d f = 0
Tactic: rw [totalDegree, Finset.sup_lt_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, (d : (a : σ) → ℕ) i
rw :
  ∀ (h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
⊢ coeff d f = 0
have rw₁ : ∀
  (h :
    LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
      (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
  LT.lt (α := ℕ) ⊥ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
Tactic: rw [totalDegree, Finset.sup_lt_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ coeff d f = 0
have h₁ : d ∈ f.support → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
Tactic: specialize h d
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : d ∈ f.support → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ coeff d f = 0
have h₁ : coeff d f ≠ 0 → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
Tactic: rw [mem_support_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ coeff d f = 0
have refine : ¬LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
Tactic: refine not_not.mp (mt h ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, (d : (a : σ) → ℕ) i
⊢ coeff d f = 0
have rw : ∀
  (h :
    LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
      (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
  coeff d f = 0
Tactic: classical
    rw [totalDegree, Finset.sup_lt_iff] at h
    · specialize h d
      rw [mem_support_iff] at h
      refine not_not.mp (mt h ?_)
      exact lt_irrefl _
    · exact lt_of_le_of_lt (Nat.zero_le _) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, (d : (a : σ) → ℕ) i
rw :
  ∀
    (h :
      LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
        (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
⊢ coeff d f = 0
have rw₁ : ∀ (h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
  coeff d f = 0
Tactic: classical
    rw [totalDegree, Finset.sup_lt_iff] at h
    · specialize h d
      rw [mem_support_iff] at h
      refine not_not.mp (mt h ?_)
      exact lt_irrefl _
    · exact lt_of_le_of_lt (Nat.zero_le _) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, (d : (a : σ) → ℕ) i
rw :
  ∀
    (h :
      LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
        (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
rw₁ :
  ∀ (h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
⊢ coeff d f = 0
have rw₂ : ∀
  (h :
    LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
      (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
  LT.lt (α := ℕ) ⊥ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
Tactic: classical
    rw [totalDegree, Finset.sup_lt_iff] at h
    · specialize h d
      rw [mem_support_iff] at h
      refine not_not.mp (mt h ?_)
      exact lt_irrefl _
    · exact lt_of_le_of_lt (Nat.zero_le _) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
have mp : p.totalDegree = 0 → p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
mp : p.totalDegree = 0 → p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
⊢ p.totalDegree = 0 ↔ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
have mpr : p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p) → p.totalDegree = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
⊢ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
have mp : ∀ (m : σ →₀ ℕ), coeff m p = coeff m ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))
have mp : coeff m p = if 0 = m then coeff 0 p else 0
Tactic: rw [coeff_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = if 0 = m then coeff 0 p else 0
have pos : ∀ (hm : 0 = m), coeff m p = coeff 0 p
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
pos : ∀ (hm : 0 = m), coeff m p = coeff 0 p
⊢ coeff m p = if 0 = m then coeff 0 p else 0
have neg : ∀ (hm : ¬0 = m), coeff m p = 0
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p
have pos : coeff 0 p = coeff 0 p
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))
have neg : ∀ (hm : ¬0 = m), coeff m p = 0
Tactic: classical rw [coeff_C]; split_ifs with hm; · rw [← hm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ coeff m p = 0
have neg : p.totalDegree < ∑ i ∈ m.support, (m : (a : σ) → ℕ) i
Tactic: apply coeff_eq_zero_of_totalDegree_lt
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ p.totalDegree < ∑ i ∈ m.support, (m : (a : σ) → ℕ) i
have neg : LT.lt (α := ℕ) 0 (∑ i ∈ m.support, (m : (a : σ) → ℕ) i)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
⊢ p.totalDegree = 0
have mpr : totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) (coeff 0 p)) = 0
Tactic: rw [h, totalDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
mpr : totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) (coeff 0 p)) = 0
⊢ p.totalDegree = 0
have mpr₁ : Eq (α := ℕ) 0 0
Tactic: rw [h, totalDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h :
  Membership.mem (γ := Finset (τ →₀ ℕ))
    (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b
⊢ (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
have h₁ : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
Tactic: rw [rename_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
have h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support
Tactic: have h' := Finsupp.mapDomain_support h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support
⊢ (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
have h'₁ : ∃ a ∈ p.support, Finsupp.mapDomain f a = b
Tactic: rw [Finset.mem_image] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : ∃ a ∈ p.support, Finsupp.mapDomain f a = b
⊢ (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
have rcases : ∀ (s : σ →₀ ℕ) (hs : s ∈ p.support) (h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)),
  ((Finsupp.mapDomain f s).sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
Tactic: rcases h' with ⟨s, hs, rfl⟩
Cleared hypotheses: b, h, h'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
intro :
  ∀
    (h :
      Membership.mem (γ := Finset (τ →₀ ℕ))
        (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b),
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ Membership.mem (γ := Finset (τ →₀ ℕ))
      (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b →
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
have intro₁ : ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)), (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
Tactic: classical
    intro h
    rw [rename_eq] at h
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
intro :
  ∀
    (h :
      Membership.mem (γ := Finset (τ →₀ ℕ))
        (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b),
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₁ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)), (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ Membership.mem (γ := Finset (τ →₀ ℕ))
      (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b →
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
have intro₂ : ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)) (h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support),
  (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
Tactic: classical
    intro h
    rw [rename_eq] at h
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
intro :
  ∀
    (h :
      Membership.mem (γ := Finset (τ →₀ ℕ))
        (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b),
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₁ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)), (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₂ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p))
    (h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support), (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ Membership.mem (γ := Finset (τ →₀ ℕ))
      (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b →
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
have intro₃ : ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)) (h' : ∃ a ∈ p.support, Finsupp.mapDomain f a = b),
  (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
Tactic: classical
    intro h
    rw [rename_eq] at h
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
intro :
  ∀
    (h :
      Membership.mem (γ := Finset (τ →₀ ℕ))
        (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b),
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₁ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)), (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₂ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p))
    (h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support), (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₃ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)) (h' : ∃ a ∈ p.support, Finsupp.mapDomain f a = b),
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ Membership.mem (γ := Finset (τ →₀ ℕ))
      (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b →
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
have intro₄ : ∀ (s : σ →₀ ℕ) (hs : s ∈ p.support) (h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)),
  ((Finsupp.mapDomain f s).sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
Tactic: classical
    intro h
    rw [rename_eq] at h
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} x
⊢ (c • x).degrees ≤ s
have rw : (HMul.hMul (α := MvPolynomial σ R) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
      x).degrees ≤
  s
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} x
⊢ (HMul.hMul (α := MvPolynomial σ R)
        ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) x).degrees ≤
    s
have refine : degrees.{u, u_1} (R := R) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c) + x.degrees ≤ s
Tactic: refine degrees_mul_le.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) = HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)
have rw : degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
  ∀ (m : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
      ∀ (n : MvPolynomial σ R),
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)
Tactic: rw [le_antisymm_iff, Submodule.mul_le]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    ∀ (m : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
        ∀ (n : MvPolynomial σ R),
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
            Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)
have refine : ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
  (i : σ →₀ ℕ) (hi : i ∈ x.support),
  Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
Tactic: refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : i ∈ x.support
⊢ Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
have hi₁ : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
Tactic: replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
⊢ Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
have this : a + b = i
Tactic: have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
⊢ Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
have ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
Tactic: have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi