awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ (aeval x : (a : MvPolynomial υ R) → R)
      ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
            (a : MvPolynomial τ R) → MvPolynomial υ R)
          ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
        MvPolynomial υ R) =
    comap f (comap g x) i
have simp : Eq.{u_4 + 1} (α := R)
  ((eval₂Hom (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
          fun (i : τ) ↦
          (eval₂Hom (algebraMap R R) x : (a : MvPolynomial υ R) → R)
            ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R) :
        (a : MvPolynomial τ R) → R)
      ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
    R)
  ((eval₂Hom (algebraMap R R) (comap g x) : (a : MvPolynomial τ R) → R)
      ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
    R)
Tactic: simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ Eq.{u_4 + 1} (α := R)
    ((eval₂Hom (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
            fun (i : τ) ↦
            (eval₂Hom (algebraMap R R) x : (a : MvPolynomial υ R) → R)
              ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R) :
          (a : MvPolynomial τ R) → R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
      R)
    ((eval₂Hom (algebraMap R R) (comap g x) : (a : MvPolynomial τ R) → R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
      R)
have refine : Eq (α := R →+* R) (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
  (algebraMap R R)
Tactic: refine eval₂Hom_congr ?_ rfl rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ Eq (α := R →+* R)
    (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
    (algebraMap R R)
have a : ∀ (r : R),
  Eq (α := R)
    ((RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)) :
          (a : R) → R)
        r :
      R)
    ((algebraMap R R : (a : R) → R) r : R)
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
⊢ comap (g.comp f) = comap f ∘ comap g
have h : ∀ (x : υ → R), comap (g.comp f) x = (comap f ∘ comap g) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), (f : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
x : σ → R
⊢ comap f x = x
have h : f = AlgHom.id R (MvPolynomial σ R)
Tactic: convert! comap_id_apply x
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), (f : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
x : σ → R
⊢ f = AlgHom.id R (MvPolynomial σ R)
have h : ∀ (φ : σ),
  Eq (α := MvPolynomial σ R) ((f : (a : MvPolynomial σ R) → MvPolynomial σ R) (X φ) : MvPolynomial σ R)
    ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X φ) : MvPolynomial σ R)
Tactic: ext1 φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
x : τ → R
⊢ comap (rename f) x = x ∘ f
have h : ∀ (x_1 : σ), comap (rename f) x x_1 = (x ∘ f) x_1
Tactic: funext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ comap (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (comap (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) x) = x
have rw : comap ((↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R).comp (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R)) x = x
Tactic: rw [← comap_comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ comap ((↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R).comp (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R)) x = x
have hf : ∀ (φ : MvPolynomial τ R),
  ((↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R).comp (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R) :
        (a : MvPolynomial τ R) → MvPolynomial τ R)
      φ =
    φ
Tactic: apply comap_eq_id_of_eq_id
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ comap (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (comap (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R) x) = x
have rw : comap ((↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R).comp (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)) x = x
Tactic: rw [← comap_comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Comap (goal)
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ comap ((↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R).comp (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)) x = x
have hf : ∀ (φ : MvPolynomial σ R),
  ((↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R).comp (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) :
        (a : MvPolynomial σ R) → MvPolynomial σ R)
      φ =
    φ
Tactic: apply comap_eq_id_of_eq_id
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
⊢ (-p).degrees = p.degrees
have rw : (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = p.degrees
Tactic: rw [degrees, support_neg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
i : σ
p : MvPolynomial σ R
⊢ degreeOf i (-p) = degreeOf i p
have rw : Multiset.count i (-p).degrees = degreeOf i p
Tactic: rw [degreeOf, degreeOf, degrees_neg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
i : σ
p : MvPolynomial σ R
rw : Multiset.count i (-p).degrees = degreeOf i p
⊢ degreeOf i (-p) = degreeOf i p
have rw₁ : Multiset.count i (-p).degrees = Multiset.count i p.degrees
Tactic: rw [degreeOf, degreeOf, degrees_neg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
i : σ
p : MvPolynomial σ R
rw : Multiset.count i (-p).degrees = degreeOf i p
rw₁ : Multiset.count i (-p).degrees = Multiset.count i p.degrees
⊢ degreeOf i (-p) = degreeOf i p
have rw₂ : Multiset.count i p.degrees = Multiset.count i p.degrees
Tactic: rw [degreeOf, degreeOf, degrees_neg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ (p - q).vars ⊆ p.vars ∪ q.vars
have h : p - q = p + -q
Tactic: convert! vars_add_subset p (-q) using 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
h : p - q = p + -q
⊢ (p - q).vars ⊆ p.vars ∪ q.vars
have h₁ : q.vars = (-q).vars
Tactic: convert! vars_add_subset p (-q) using 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
hpq : Disjoint p.vars q.vars
⊢ (p - q).vars = p.vars ∪ q.vars
have hpq₁ : Disjoint p.vars (-q).vars
Tactic: rw [← vars_neg q] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ (p - q).vars = p.vars ∪ q.vars
have h : p - q = p + -q
Tactic: convert! vars_add_of_disjoint hpq using 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
h : p - q = p + -q
⊢ (p - q).vars = p.vars ∪ q.vars
have h₁ : q.vars = (-q).vars
Tactic: convert! vars_add_of_disjoint hpq using 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x : MvPolynomial R ℤ
n : ℤ
⊢ eval₂.{0, v, u} (σ := R) c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X)
      ((C : (a : ℤ) → MvPolynomial R ℤ) n) =
    (f : (a : MvPolynomial R ℤ) → S) ((C : (a : ℤ) → MvPolynomial R ℤ) n : MvPolynomial R ℤ)
have rw : Eq (α := S) ((c : (a : ℤ) → S) n : S) ((↑n : S) : S)
Tactic: rw [hom_C f, eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x p q : MvPolynomial R ℤ
hp : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) p = (f : (a : MvPolynomial R ℤ) → S) p
hq : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) q = (f : (a : MvPolynomial R ℤ) → S) q
⊢ eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) (p + q) =
    (f : (a : MvPolynomial R ℤ) → S) (p + q)
have rw : HAdd.hAdd (α := S) (β := S) ((f : (a : MvPolynomial R ℤ) → S) p : S) ((f : (a : MvPolynomial R ℤ) → S) q : S) =
  (f : (a : MvPolynomial R ℤ) → S) (p + q)
Tactic: rw [eval₂_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) p = (f : (a : MvPolynomial R ℤ) → S) p
⊢ eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) (p * X n) =
    (f : (a : MvPolynomial R ℤ) → S) (p * X n)
have rw : HMul.hMul (α := S) (β := S) ((f : (a : MvPolynomial R ℤ) → S) p : S)
    (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X n : S) =
  (f : (a : MvPolynomial R ℤ) → S) (p * X n)
Tactic: rw [eval₂_mul, eval₂_X, hp]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ (m : (a : σ) → ℕ) x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ (m : (a : σ) → ℕ) x → coeff m f = coeff m g
⊢ degreeOf x (f - g) < k
have rw : ∀ m ∈ (f - g).support, (m : (a : σ) → ℕ) x < k
Tactic: rw [degreeOf_lt_iff h]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
a b : MvPolynomial σ R
⊢ (a - b).totalDegree = (a + -b).totalDegree
have rw : (a + -b).totalDegree = (a + -b).totalDegree
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
a b : MvPolynomial σ R
⊢ max a.totalDegree (-b).totalDegree = max a.totalDegree b.totalDegree
have rw : max a.totalDegree b.totalDegree = max a.totalDegree b.totalDegree
Tactic: rw [totalDegree_neg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
r : R
⊢ max p.totalDegree (totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) = p.totalDegree
have rw : max p.totalDegree 0 = p.totalDegree
Tactic: rw [totalDegree_C, Nat.max_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.CommRing (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
r : R
rw : max p.totalDegree 0 = p.totalDegree
⊢ max p.totalDegree (totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) = p.totalDegree
have rw₁ : p.totalDegree = p.totalDegree
Tactic: rw [totalDegree_C, Nat.max_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
have refine : LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
  ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
Tactic: refine (supDegree_single s a).trans_le ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
have pos : a = 0 → LE.le (α := Multiset σ) (⊥ : Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
pos : a = 0 → LE.le (α := Multiset σ) (⊥ : Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
⊢ LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
have neg : ¬a = 0 →
  LE.le (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
have refine : LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
  ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
Tactic: classical
    refine (supDegree_single s a).trans_le ?_
    split_ifs
    exacts [bot_le, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
refine :
  LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
have pos : a = 0 → LE.le (α := Multiset σ) (⊥ : Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
Tactic: classical
    refine (supDegree_single s a).trans_le ?_
    split_ifs
    exacts [bot_le, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
refine :
  LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
pos : a = 0 → LE.le (α := Multiset σ) (⊥ : Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
have neg : ¬a = 0 →
  LE.le (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
Tactic: classical
    refine (supDegree_single s a).trans_le ?_
    split_ifs
    exacts [bot_le, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) 0) 0
have rw : Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) 0)) 0
Tactic: rw [← C_0]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p + q).degrees ≤ p.degrees ⊔ q.degrees
have simp_rw : LE.le (α := Multiset σ) ((p + q).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
  ((p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) ⊔
    q.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
Tactic: simp_rw [degrees_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) (∑ i ∈ s, f i)) (s.sup fun (i : ι) ↦ (f i).degrees)
have simp_rw : LE.le.{u_1} (α := Multiset σ)
  (Finset.sup (support.{u, u_1} (R := R) (∑ i ∈ s, f i)) fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
  (s.sup fun (i : ι) ↦ (f i).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
Tactic: simp_rw [degrees_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.degrees = 0 ↔ p.support ⊆ {0}
have rw : (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0
Tactic: rw [Finset.subset_singleton_iff', Multiset.eq_zero_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0
have refine_1 : ∀ (h : ∀ (a : σ), a ∉ p.degrees) (s : σ →₀ ℕ) (hs : s ∈ p.support), s = 0
Tactic: refine ⟨fun h s hs ↦ ?_, fun h i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
refine_1 : ∀ (h : ∀ (a : σ), a ∉ p.degrees) (s : σ →₀ ℕ) (hs : s ∈ p.support), s = 0
⊢ (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0
have refine_2 : ∀ (h : ∀ b ∈ p.support, b = 0) (i : σ) (hi : i ∈ p.degrees), False
Tactic: refine ⟨fun h s hs ↦ ?_, fun h i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ s = 0
have refine_1 : s.support = ∅
Tactic: rw [← Finsupp.support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ s.support = ∅
have h₁ : ∀ (a : σ), ¬∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ a ∈ d.support
Tactic: simp only [mem_degrees] 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
p : MvPolynomial σ R
h : ∀ b ∈ p.support, b = 0
i : σ
hi : i ∈ p.degrees
⊢ False
have refine_2 : ∀ (s : σ →₀ ℕ) (hs1 : coeff s p ≠ 0) (hs2 : i ∈ s.support), False
Tactic: rcases mem_degrees.mp hi with ⟨s, hs1, hs2⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : ∀ b ∈ p.support, b = 0
i : σ
hi : i ∈ p.degrees
s : σ →₀ ℕ
hs1 : coeff s p ≠ 0
hs2 : i ∈ s.support
⊢ False
have this : Membership.mem (γ := Finset σ) ∅ i
Tactic: have := Finsupp.support_eq_empty.mpr (h s <| mem_support_iff.mpr hs1) ▸ hs2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ p.degrees ≤ (p + q).degrees
have a : ∀ b ∈ p.support, (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ (p + q).degrees
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
have a : ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (d : σ →₀ ℕ) (hd : d ∈ p.support),
  (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
Tactic: rw [Multiset.disjoint_iff_ne] at h
Cleared hypotheses: h, d, hd
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
have a : ∀ (hd : 0 ∈ p.support), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) 0 ≤ (p + q).degrees
Tactic: obtain rfl | h0 := eq_or_ne d 0
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
a : ∀ (hd : 0 ∈ p.support), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) 0 ≤ (p + q).degrees
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
have a₁ : ∀ (h0 : d ≠ 0), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
Tactic: obtain rfl | h0 := eq_or_ne d 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
have a : d ∈ (p + q).support
Tactic: refine Finset.le_sup_of_le (b := d) ?_ le_rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ d ∈ (p + q).support
have a : coeff d p + coeff d q ≠ 0
Tactic: rw [mem_support_iff, coeff_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
⊢ coeff d p + coeff d q ≠ 0
have rwa : coeff d p + 0 ≠ 0
Tactic: rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
rwa : coeff d p + 0 ≠ 0
⊢ coeff d p + coeff d q ≠ 0
have rwa₁ : coeff d p ≠ 0
Tactic: rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
rwa : coeff d p + 0 ≠ 0
rwa₁ : coeff d p ≠ 0
⊢ coeff d p + coeff d q ≠ 0
have rwa₂ : Ne.{u + 1} (α := R) ((p : (a : σ →₀ ℕ) → R) d : R) (0 : R)
Tactic: rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]