awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
intro :
  ∀ ⦃i : τ⦄,
    Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
      i ∈ Multiset.map f φ.degrees
intro₁ :
  ∀ ⦃i : τ⦄,
    (∃ (d : τ →₀ ℕ),
        Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
      ∃ a ∈ φ.degrees, f a = i
intro₂ :
  ∀ ⦃i : τ⦄ (d : τ →₀ ℕ)
    (hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ d.support), ∃ a ∈ φ.degrees, f a = i
intro₃ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ (Finsupp.mapDomain f x).support), ∃ a ∈ φ.degrees, f a = i
intro₄ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)),
    ∃ a ∈ φ.degrees, f a = i
intro₅ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : Ne (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0),
    ∃ a ∈ φ.degrees, f a = i
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro₆ : ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
  (hd :
    Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
  (hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i),
  Eq (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
intro :
  ∀ ⦃i : τ⦄,
    Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
      i ∈ Multiset.map f φ.degrees
intro₁ :
  ∀ ⦃i : τ⦄,
    (∃ (d : τ →₀ ℕ),
        Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
      ∃ a ∈ φ.degrees, f a = i
intro₂ :
  ∀ ⦃i : τ⦄ (d : τ →₀ ℕ)
    (hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ d.support), ∃ a ∈ φ.degrees, f a = i
intro₃ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ (Finsupp.mapDomain f x).support), ∃ a ∈ φ.degrees, f a = i
intro₄ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)),
    ∃ a ∈ φ.degrees, f a = i
intro₅ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : Ne (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0),
    ∃ a ∈ φ.degrees, f a = i
intro₆ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i),
    Eq (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro₇ : ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
  (hd :
    Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
  (hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i),
  ∀ x_1 ∈ x.support,
    Eq (α := ℕ) (((Finsupp.single (f x_1) ((x : (a : σ) → ℕ) x_1) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = Multiset.map f p.degrees
have simp : p.support.sup ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) =
  p.support.sup (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ))
Tactic: simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
    support_rename_of_injective h, Finset.sup_image]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ p.support.sup ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) =
    p.support.sup (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ))
have refine : ∀ x ∈ p.support,
  ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) x =
    (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ)) x
Tactic: refine Finset.sup_congr rfl fun x _ => ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = Multiset.map f p.degrees
have simp : p.support.sup ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) =
  p.support.sup (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ))
Tactic: classical
  simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
    support_rename_of_injective h, Finset.sup_image]
  refine Finset.sup_congr rfl fun x _ => ?_
  exact (Finsupp.toMultiset_map _ _).symm
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
simp :
  p.support.sup ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) =
    p.support.sup (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ))
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = Multiset.map f p.degrees
have simp₁ : ∀ x ∈ p.support,
  ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) x =
    (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ)) x
Tactic: classical
  simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
    support_rename_of_injective h, Finset.sup_image]
  refine Finset.sup_congr rfl fun x _ => ?_
  exact (Finsupp.toMultiset_map _ _).symm
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
have rw : Eq (α := ℕ) (f.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
  (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
Tactic: rw [degreeOf_def, degrees, Multiset.count_finset_sup]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ Eq (α := ℕ) (f.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
have e_f : Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
  fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
have e_f : ∀ (x : σ →₀ ℕ), Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) x) = (x : (a : σ) → ℕ) n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
have rw : Multiset.count n f.degrees = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
Tactic: classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
rw : Multiset.count n f.degrees = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
⊢ degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
have rw₁ : Multiset.count n (f.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) =
  f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
Tactic: classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
rw : Multiset.count n f.degrees = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
rw₁ :
  Multiset.count n (f.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) =
    f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
⊢ degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
have rw₂ : Eq (α := ℕ) (f.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
  (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
Tactic: classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
rw : Multiset.count n f.degrees = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
rw₁ :
  Multiset.count n (f.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) =
    f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
rw₂ rw₃ rw₄ :
  Eq (α := ℕ) (f.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
⊢ degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
have e_f : Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
  fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
Tactic: classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
rw : Multiset.count n f.degrees = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
rw₁ :
  Multiset.count n (f.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) =
    f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
rw₂ rw₃ rw₄ :
  Eq (α := ℕ) (f.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
e_f :
  Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
⊢ degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
have e_f₁ : ∀ (x : σ →₀ ℕ), Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) x) = (x : (a : σ) → ℕ) n
Tactic: classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
⊢ degreeOf n f < d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
have rwa : (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) < d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
Tactic: rwa [degreeOf_eq_sup, Finset.sup_lt_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
rwa : (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) < d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
⊢ degreeOf n f < d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
have rwa₁ : (∀ b ∈ f.support, (b : (a : σ) → ℕ) n < d) ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
Tactic: rwa [degreeOf_eq_sup, Finset.sup_lt_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
rwa : (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) < d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
rwa₁ : (∀ b ∈ f.support, (b : (a : σ) → ℕ) n < d) ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
⊢ degreeOf n f < d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
have rwa₂ : ⊥ < d
Tactic: rwa [degreeOf_eq_sup, Finset.sup_lt_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
⊢ degreeOf n f ≤ d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n ≤ d
have rw : (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) ≤ d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n ≤ d
Tactic: rw [degreeOf_eq_sup, Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
rw : (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) ≤ d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n ≤ d
⊢ degreeOf n f ≤ d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n ≤ d
have rw₁ : (∀ b ∈ f.support, (b : (a : σ) → ℕ) n ≤ d) ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n ≤ d
Tactic: rw [degreeOf_eq_sup, Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
inst_2 : Nontrivial R
⊢ degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
have pos : ∀ (c : i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
Tactic: by_cases c : i = j
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
inst_2 : Nontrivial R
pos : ∀ (c : i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
⊢ degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
have neg : ∀ (c : ¬i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
Tactic: by_cases c : i = j
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
inst_2 : Nontrivial R
⊢ degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
have pos : ∀ (c : i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
Tactic: classical
  by_cases c : i = j
  · simp only [c, if_true, degreeOf_def, degrees_X, Multiset.count_singleton]
  simp [c, degreeOf_def, degrees_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
inst_2 : Nontrivial R
pos : ∀ (c : i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
⊢ degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
have neg : ∀ (c : ¬i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
Tactic: classical
  by_cases c : i = j
  · simp only [c, if_true, degreeOf_def, degrees_X, Multiset.count_singleton]
  simp [c, degreeOf_def, degrees_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
have simp_rw : LE.le (α := ℕ) ((f + g).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
  (max (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) (g.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n))
Tactic: simp_rw [degreeOf_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ (m : (a : σ) → ℕ) i ≤ degreeOf i f
have rw : LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i : ℕ)
Tactic: rw [degreeOf_eq_sup i]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ degreeOf.{u, u_1} (R := R) i ((monomial s : (a : R) → MvPolynomial σ R) a) = (s : (a : σ) → ℕ) i
have rw : Multiset.count i (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) = (s : (a : σ) → ℕ) i
Tactic: rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
rw : Multiset.count i (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) = (s : (a : σ) → ℕ) i
⊢ degreeOf.{u, u_1} (R := R) i ((monomial s : (a : R) → MvPolynomial σ R) a) = (s : (a : σ) → ℕ) i
have rw₁ : Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = (s : (a : σ) → ℕ) i
Tactic: rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
rw : Multiset.count i (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) = (s : (a : σ) → ℕ) i
rw₁ : Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = (s : (a : σ) → ℕ) i
⊢ degreeOf.{u, u_1} (R := R) i ((monomial s : (a : R) → MvPolynomial σ R) a) = (s : (a : σ) → ℕ) i
have rw₂ : Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
Tactic: rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ degreeOf.{u, u_1} (R := R) i ((monomial s : (a : R) → MvPolynomial σ R) a) = (s : (a : σ) → ℕ) i
have classical : Multiset.count i (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) = (s : (a : σ) → ℕ) i
Tactic: classical rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
classical :
  Multiset.count i (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) = (s : (a : σ) → ℕ) i
⊢ degreeOf.{u, u_1} (R := R) i ((monomial s : (a : R) → MvPolynomial σ R) a) = (s : (a : σ) → ℕ) i
have classical₁ : Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = (s : (a : σ) → ℕ) i
Tactic: classical rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
classical :
  Multiset.count i (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) = (s : (a : σ) → ℕ) i
classical₁ : Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = (s : (a : σ) → ℕ) i
⊢ degreeOf.{u, u_1} (R := R) i ((monomial s : (a : R) → MvPolynomial σ R) a) = (s : (a : σ) → ℕ) i
have classical₂ : Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
Tactic: classical rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
i : σ
k : ℕ
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X i) k) = k
have rw : degreeOf.{u, u_1} (R := R) i ((monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1) = k
Tactic: rw [X_pow_eq_monomial, degreeOf_monomial_eq _ _ one_ne_zero, Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
i : σ
k : ℕ
rw : degreeOf.{u, u_1} (R := R) i ((monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1) = k
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X i) k) = k
have rw₁ : (Finsupp.single i k : (a : σ) → ℕ) i = k
Tactic: rw [X_pow_eq_monomial, degreeOf_monomial_eq _ _ one_ne_zero, Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
i : σ
k : ℕ
rw : degreeOf.{u, u_1} (R := R) i ((monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1) = k
rw₁ : (Finsupp.single i k : (a : σ) → ℕ) i = k
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X i) k) = k
have rw₂ : k = k
Tactic: rw [X_pow_eq_monomial, degreeOf_monomial_eq _ _ one_ne_zero, Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i p
have inl : ∀ (si : Eq (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)), (s : (a : σ) → ℕ) i ≤ degreeOf i p
Tactic: obtain si | si := eq_or_lt_of_le <| Nat.zero_le (s i)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
inl : ∀ (si : Eq (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)), (s : (a : σ) → ℕ) i ≤ degreeOf i p
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i p
have inr : ∀ (si : LT.lt (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)), (s : (a : σ) → ℕ) i ≤ degreeOf i p
Tactic: obtain si | si := eq_or_lt_of_le <| Nat.zero_le (s i)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : LT.lt (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i p
have inr : ∃ b ∈ p.support, LE.le (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((b : (a : σ) → ℕ) i : ℕ)
Tactic: rw [degreeOf_eq_sup, Finset.le_sup_iff si]