awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support
⊢ s ≤ m
have neg : ∀ (j : σ →₀ ℕ)
  (h :
    j + s ∈
      (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support),
  s ≤ j + s
Tactic: obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0
have pos : ∀ (h : s ≤ m),
  coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff (m - s) p * r
Tactic: classical
  split_ifs with h
  · conv_rhs => rw [← coeff_mul_monomial _ s]
    rw [tsub_add_cancel_of_le h]
  · contrapose! h
    rw [← mem_support_iff] at h
    obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
    exact le_add_left le_rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
pos :
  ∀ (h : s ≤ m),
    coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
      coeff (m - s) p * r
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0
have neg : ∀ (h : ¬s ≤ m),
  coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) = 0
Tactic: classical
  split_ifs with h
  · conv_rhs => rw [← coeff_mul_monomial _ s]
    rw [tsub_add_cancel_of_le h]
  · contrapose! h
    rw [← mem_support_iff] at h
    obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
    exact le_add_left le_rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) p) =
    if s ≤ m then r * coeff (m - s) p else 0
have rw : coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
  if s ≤ m then coeff (m - s) p * r else 0
Tactic: rw [mul_comm, mul_comm r]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (p * X s) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have refine : (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
  if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
Tactic: refine (coeff_mul_monomial' _ _ _ _).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have simp_rw : (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
  if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
Tactic: simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
simp_rw :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have simp_rw₁ : (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
  if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
Tactic: simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
simp_rw :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
simp_rw₁ :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have simp_rw₂ : (if LT.lt (α := ℕ) (0 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
  if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
Tactic: simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
simp_rw :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
simp_rw₁ :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
simp_rw₂ :
  (if LT.lt (α := ℕ) (0 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have simp_rw₃ : (if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
  if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
Tactic: simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have refine : (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
  if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
Tactic: refine (coeff_monomial_mul' _ _ _ _).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have simp_rw : (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
  if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
Tactic: simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
simp_rw :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have simp_rw₁ : (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
  if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
Tactic: simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
simp_rw :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
simp_rw₁ :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have simp_rw₂ : (if LT.lt (α := ℕ) (0 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
  if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
Tactic: simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
simp_rw :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
simp_rw₁ :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
simp_rw₂ :
  (if LT.lt (α := ℕ) (0 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
have simp_rw₃ : (if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then 1 * coeff (m - Finsupp.single s 1) p else 0) =
  if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
Tactic: simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p = 0 ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
have rw : (∀ (m : σ →₀ ℕ), coeff m p = coeff m 0) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
Tactic: rw [MvPolynomial.ext_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p ≠ 0 ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0
have rw : (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0
Tactic: rw [Ne, eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0
have push : (∃ (d : σ →₀ ℕ), coeff d p ≠ 0) ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
⊢ Ne (α := MvPolynomial σ R) (X s) 0
have rw : ∃ (d : σ →₀ ℕ), Ne.{u + 1} (α := R) (coeff d (X s)) 0
Tactic: rw [ne_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
⊢ ∃ (d : σ →₀ ℕ), Ne.{u + 1} (α := R) (coeff d (X s)) 0
have h : Ne.{u + 1} (α := R) (coeff (Finsupp.single s 1) (X s)) 0
Tactic: use Finsupp.single s 1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.support.Nonempty ↔ p ≠ 0
have rw : p.support ≠ ∅ ↔ p ≠ 0
Tactic: rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
rw : p.support ≠ ∅ ↔ p ≠ 0
⊢ p.support.Nonempty ↔ p ≠ 0
have rw₁ : ¬p.support = ∅ ↔ p ≠ 0
Tactic: rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
rw : p.support ≠ ∅ ↔ p ≠ 0
rw₁ : ¬p.support = ∅ ↔ p ≠ 0
⊢ p.support.Nonempty ↔ p ≠ 0
have rw₂ : ¬p = 0 ↔ p ≠ 0
Tactic: rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
⊢ IsRegular (R := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
have rw : IsLeftRegular (R := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
Tactic: rw [← isLeftRegular_iff_isRegular]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q)
⊢ p = q
have a₁ : ∀ (d : σ →₀ ℕ), coeff d p = coeff d q
Tactic: ext d
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q)
d : σ →₀ ℕ
⊢ coeff d p = coeff d q
have h' : Eq.{u + 1} (α := R)
  (coeff (m + d)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p))
  (coeff (m + d)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q))
Tactic: have h' := congr_arg (coeff (m + d)) h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q)
d : σ →₀ ℕ
h' :
  Eq.{u + 1} (α := R)
    (coeff (m + d)
      ((fun (x : MvPolynomial σ R) ↦
          HMul.hMul (α := MvPolynomial σ R)
            ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x)
        p))
    (coeff (m + d)
      ((fun (x : MvPolynomial σ R) ↦
          HMul.hMul (α := MvPolynomial σ R)
            ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x)
        q))
⊢ coeff d p = coeff d q
have h'₁ : a * coeff d p = a * coeff d q
Tactic: simp only [coeff_monomial_mul] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      p)
    ((fun (x : MvPolynomial σ R) ↦
        HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial m : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          x)
      q)
d : σ →₀ ℕ
h' a₁ : a * coeff d p = a * coeff d q
⊢ coeff d p = coeff d q
have a₂ : a * coeff d q = a * coeff d q
Tactic: rw [← ha.left.eq_iff, h']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ coeff i φ
have mp : (C : (a : R) → MvPolynomial σ R) r ∣ φ → ∀ (i : σ →₀ ℕ), r ∣ coeff i φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
mp : (C : (a : R) → MvPolynomial σ R) r ∣ φ → ∀ (i : σ →₀ ℕ), r ∣ coeff i φ
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ coeff i φ
have mpr : (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) → (C : (a : R) → MvPolynomial σ R) r ∣ φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ coeff c (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ)
have mp : r ∣ r * coeff c φ
Tactic: rw [coeff_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
h : ∀ (i : σ →₀ ℕ), r ∣ coeff i φ
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ φ
have mpr : ∀ (C : (i : σ →₀ ℕ) → R) (hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i), (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
Tactic: choose C hc using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
⊢ (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
have h : φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
Tactic: use ψ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
⊢ φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
have h : ∀ (m : σ →₀ ℕ),
  coeff m φ =
    coeff m (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)
Tactic: apply MvPolynomial.ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
⊢ coeff i φ =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)
have h : coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0
Tactic: simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
⊢ coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0
have pos : ∀ (hi : i ∈ φ.support), coeff i φ = r * C i
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
pos : ∀ (hi : i ∈ φ.support), coeff i φ = r * C i
⊢ coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0
have neg : ∀ (hi : i ∉ φ.support), coeff i φ = r * 0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
hi : i ∈ φ.support
⊢ coeff i φ = r * C i
have pos : r * C i = r * C i
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i)
i : σ →₀ ℕ
hi : i ∉ φ.support
⊢ coeff i φ = r * 0
have hi₁ : coeff i φ = 0
Tactic: rw [notMem_support_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
mpr mpr₁ mpr₂ mpr₃ : (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
⊢ (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
have h : let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
Tactic: classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]