awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
k : ℕ
h : i ≠ j
zero : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = 0
succ :
  ∀ (k : ℕ) (hk : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0),
    degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0

Tactic:
induction k with
  | zero => rw [pow_zero, ← C_1, degreeOf_C]
  | succ k hk => rw [pow_add, pow_one, degreeOf_mul_X_of_ne _ h, hk]

Premises used: MvPolynomial.degreeOf_C, pow_add, MvPolynomial.C_1, pow_zero, AddMonoidAlgebra.zero, pow_one, MvPolynomial.degreeOf_mul_X_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
h : i ≠ j
⊢ degreeOf.{u, u_1} (R := R) i (X j) = 0

Tactic:
pow_one (X j : MvPolynomial σ R) ▸ degreeOf_X_pow_of_ne 1 h

Premises used: MvPolynomial.X, Eq.rec, MvPolynomial.degreeOf_X_pow_of_ne, pow_one, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : degreeOf j (f * X j) = degreeOf j f + 1
by_contra : ∀ (ha : f = 0), False
⊢ f ≠ 0

Tactic:
by_contra ha
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : degreeOf j (f * X j) = degreeOf j f + 1
ha : f = 0
⊢ False

Tactic:
simp [ha] at h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
refine : ∀ (h : f ≠ 0), degreeOf j (f * X j) = degreeOf j f + 1
⊢ degreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0

Tactic:
refine ⟨fun h => by by_contra ha; simp [ha] at h, fun h => ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
apply : degreeOf j f + 1 ≤ degreeOf j (f * X j)
⊢ degreeOf j (f * X j) = degreeOf j f + 1

Tactic:
apply Nat.le_antisymm (degreeOf_mul_X_self j f)

Premises used: MvPolynomial.degreeOf_mul_X_self, Nat.le_antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
⊢ HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)

Tactic:
have : (f.support.sup fun m ↦ m j) + 1 = (f.support.sup fun m ↦ (m j + 1)) :=
    Finset.apply_sup_eq_sup_comp_of_nonempty @Nat.succ_le_succ (support_nonempty.mpr h)
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
simp :
  LE.le (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ))
    ((Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j)
⊢ degreeOf j f + 1 ≤ degreeOf j (f * X j)

Tactic:
simp only [degreeOf_eq_sup, support_mul_X, this]

Premises used: MvPolynomial.support_mul_X, MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
a :
  ∀ b ∈ f.support,
    HAdd.hAdd (α := ℕ) (β := ℕ) ((b : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
      (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j
⊢ LE.le (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ))
    ((Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j)

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
x : σ →₀ ℕ
hx : x ∈ f.support
a :
  ∃ b ∈ f.support,
    HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)) b
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
    (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j

Tactic:
simp only [Finset.sup_map, bot_eq_zero', add_pos_iff, zero_lt_one, or_true, Finset.le_sup_iff]

Premises used: Finset.le_sup_iff, zero_lt_one, Finset.sup_map, add_pos_iff, or_true, bot_eq_zero'
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
x : σ →₀ ℕ
hx : x ∈ f.support
h₁ :
  x ∈ f.support ∧
    HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)) x
⊢ ∃ b ∈ f.support,
    HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)) b

Tactic:
use x
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ x ∈ f.support ∧
    HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)) x

Tactic:
simpa using mem_support_iff.mp hx

Premises used: MvPolynomial.mem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
zero : degreeOf i (p * 1) = degreeOf i p + 0
zero₁ : degreeOf i p = degreeOf i p + 0
zero₂ zero₃ : degreeOf i p = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0) = degreeOf i p + 0

Tactic:
rw [pow_zero, mul_one, add_zero]

Premises used: pow_zero, mul_one, add_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
rcases : ∀ (s : σ →₀ ℕ) (hs : coeff s p ≠ 0), p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
⊢ p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0

Tactic:
rcases ne_zero_iff.mp h with ⟨s, hs⟩

Premises used: MvPolynomial.ne_zero_iff, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
⊢ p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0

Tactic:
ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩

Premises used: Iff.mpr, MvPolynomial.ne_zero_iff, HAdd.hAdd, Exists.intro, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
refine : coeff (s + Finsupp.single i k) (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) ≠ 0
⊢ p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0

Tactic:
refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩

Premises used: Iff.mpr, MvPolynomial.ne_zero_iff, HAdd.hAdd, Exists.intro, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
rwa : coeff (s + Finsupp.single i k) (p * (monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1) ≠ 0
rwa₁ : coeff s p * 1 ≠ 0
rwa₂ rwa₃ rwa₄ rwa₅ : coeff s p ≠ 0
⊢ coeff (s + Finsupp.single i k) (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) ≠ 0

Tactic:
rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.coeff_mul_monomial, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
⊢ p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0

Tactic:
have : p * X i ^ k ≠ 0 := by
      rcases ne_zero_iff.mp h with ⟨s, hs⟩
      refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩
      rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
this : p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)) =
    degreeOf i p + (k + 1)
succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * X i)) = degreeOf i p + (k + 1)
succ₂ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k * X i) = degreeOf i p + (k + 1)
succ₃ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) + 1 = degreeOf i p + (k + 1)
succ₄ : degreeOf i p + k + 1 = degreeOf i p + (k + 1)
succ₅ succ₆ : degreeOf i p + (k + 1) = degreeOf i p + (k + 1)
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)

Tactic:
rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]

Premises used: Iff.mpr, add_assoc, mul_assoc, pow_add, MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff, pow_one
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
k : ℕ
h : p ≠ 0
zero : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0) = degreeOf i p + 0
succ :
  ∀ (k : ℕ) (hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k),
    degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k

Tactic:
induction k with
  | zero => rw [pow_zero, mul_one, add_zero]
  | succ k hk =>
    have : p * X i ^ k ≠ 0 := by
      rcases ne_zero_iff.mp h with ⟨s, hs⟩
      refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩
      rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]
    rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]

Premises used: add_assoc, mul_assoc, pow_add, pow_zero, AddMonoidAlgebra.zero, pow_one, mul_one, add_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
zero : degreeOf i (p * 1) = degreeOf i p
zero₁ zero₂ : degreeOf i p = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = degreeOf i p

Tactic:
rw [pow_zero, mul_one]

Premises used: pow_zero, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1)) =
    degreeOf i p
succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * X j)) = degreeOf i p
succ₂ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k * X j) = degreeOf i p
succ₃ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
succ₄ succ₅ : degreeOf i p = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = degreeOf i p

Tactic:
rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]

Premises used: mul_assoc, pow_add, pow_one, MvPolynomial.degreeOf_mul_X_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
k : ℕ
h : i ≠ j
zero : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = degreeOf i p
succ :
  ∀ (k : ℕ) (hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p),
    degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p

Tactic:
induction k with
  | zero => rw [pow_zero, mul_one]
  | succ k hk => rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]

Premises used: mul_assoc, pow_add, pow_zero, AddMonoidAlgebra.zero, pow_one, mul_one, MvPolynomial.degreeOf_mul_X_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
a : degreeOf i (p + q) ≤ degreeOf i p
a₁ : degreeOf i p ≤ degreeOf i (p + q)
⊢ degreeOf i (p + q) = degreeOf i p

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
a : degreeOf i (p + q) ≤ max (degreeOf i p) (degreeOf i q)
⊢ degreeOf i (p + q) ≤ degreeOf i p

Tactic:
rw [← max_eq_left_of_lt h]

Premises used: max_eq_left_of_lt
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) ≤ max (degreeOf i p) (degreeOf i q)

Tactic:
degreeOf_add_le i p q

Premises used: MvPolynomial.degreeOf_add_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) ≤ max (degreeOf i p) (degreeOf i q)

Tactic:
exact degreeOf_add_le i p q

Premises used: MvPolynomial.degreeOf_add_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
a : degreeOf i p ≤ (p + q).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
⊢ degreeOf i p ≤ degreeOf i (p + q)

Tactic:
nth_rw 2 [degreeOf_eq_sup]

Premises used: MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
a : ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i
⊢ degreeOf i p ≤ (p + q).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i

Tactic:
apply (Finset.le_sup_iff <| Nat.zero_lt_of_lt h).mpr

Premises used: Iff.mpr, Nat.zero_lt_of_lt, Finset.le_sup_iff
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ p.support.Nonempty

Tactic:
aesop
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ p.support.Nonempty

Tactic:
have : p.support.Nonempty := by aesop
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
a :
  ∀ (s : σ →₀ ℕ) (hs1 : s ∈ p.support)
    (hs2 : Eq (α := ℕ) (p.support.sup fun (s : σ →₀ ℕ) ↦ (s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)),
    ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i
⊢ ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i

Tactic:
have ⟨s, hs1, hs2⟩ := Finset.exists_mem_eq_sup _ this (fun s ↦ s i)
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : Eq (α := ℕ) (p.support.sup fun (s : σ →₀ ℕ) ↦ (s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
⊢ degreeOf i p = (s : (a : σ) → ℕ) i

Tactic:
rw [← degreeOf_eq_sup i p] at hs2

Premises used: MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
rw rw₁ : LE.le (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
⊢ degreeOf i p ≤ (s : (a : σ) → ℕ) i

Tactic:
rw [hs2]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
a : s ∈ (p + q).support
⊢ ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i

Tactic:
refine ⟨s, ?_, by rw [hs2]⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
contrapose! : ∀ (h : s ∈ q.support), degreeOf i p ≤ degreeOf i q
⊢ s ∉ q.support

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
h : s ∈ q.support
rw : (s : (a : σ) → ℕ) i ≤ degreeOf i q
⊢ degreeOf i p ≤ degreeOf i q

Tactic:
rw [hs2]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
h : s ∈ q.support
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i q

Tactic:
le_degreeOf_of_mem_support i h

Premises used: MvPolynomial.le_degreeOf_of_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
h : s ∈ q.support
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i q

Tactic:
exact le_degreeOf_of_mem_support i h

Premises used: MvPolynomial.le_degreeOf_of_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
⊢ s ∉ q.support

Tactic:
have : s ∉ q.support := by
    contrapose! h
    rw [hs2]
    exact le_degreeOf_of_mem_support i h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this_1 : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
this : s ∉ q.support
a : ∀ (hs1 : ¬coeff s p = 0) (this : coeff s q = 0), ¬coeff s p + coeff s q = 0
⊢ s ∈ (p + q).support

Tactic:
simp only [mem_support_iff, ne_eq, coeff_add, not_not] at hs1 ⊢ this

Premises used: MvPolynomial.mem_support_iff, Classical.not_not, ne_eq, MvPolynomial.coeff_add
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this_1 : p.support.Nonempty
s : σ →₀ ℕ
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
hs1 : ¬coeff s p = 0
this : coeff s q = 0
a : ¬coeff s p + 0 = 0
a₁ a₂ a₃ a₄ : ¬coeff s p = 0
⊢ ¬coeff s p + coeff s q = 0

Tactic:
rwa [this, add_zero]

Premises used: add_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i (p + q) < degreeOf i p
contrapose! : ∀ (h : degreeOf i p ≠ degreeOf i q), degreeOf i p ≤ degreeOf i (p + q)
⊢ degreeOf i p = degreeOf i q

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i p ≠ degreeOf i q
apply : max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
⊢ degreeOf i p ≤ degreeOf i (p + q)

Tactic:
apply le_trans (Nat.le_max_left _ (q.degreeOf i))

Premises used: Nat.le_max_left, le_trans, MvPolynomial.degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i p ≠ degreeOf i q
inl : ∀ (h : degreeOf i p < degreeOf i q), max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
inr : ∀ (h : degreeOf i q < degreeOf i p), max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)

Tactic:
rcases Nat.lt_or_lt_of_ne h with h | h

Premises used: Nat.lt_or_lt_of_ne
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h_1 : degreeOf i p ≠ degreeOf i q
h : degreeOf i p < degreeOf i q
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)

Tactic:
simp [add_comm p q, degreeOf_add_eq_of_degreeOf_lt h, max_eq_right_of_lt h]

Premises used: max_eq_right_of_lt, MvPolynomial.degreeOf_add_eq_of_degreeOf_lt, add_comm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h_1 : degreeOf i p ≠ degreeOf i q
h : degreeOf i q < degreeOf i p
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)

Tactic:
simp [degreeOf_add_eq_of_degreeOf_lt h, max_eq_left_of_lt h]

Premises used: MvPolynomial.degreeOf_add_eq_of_degreeOf_lt, max_eq_left_of_lt
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ Multiset.count i
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p).degrees ≤
    Multiset.count i (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c) + p.degrees)

Tactic:
Multiset.count_le_of_le i degrees_mul_le

Premises used: Multiset.count_le_of_le, MvPolynomial.degrees_mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
h : p.degrees = degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c) + p.degrees
⊢ Multiset.count i
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p).degrees ≤
    Multiset.count i p.degrees

Tactic:
convert! Multiset.count_le_of_le i degrees_mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ p.degrees = degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c) + p.degrees

Tactic:
simp only [degrees_C, zero_add]

Premises used: MvPolynomial.degrees_C, zero_add