awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
c : σ →₀ ℕ
hc : (if d = c then r else 0) ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m
have pos : ∀ (h : d = c) (hc : r ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
Tactic: split_ifs at hc with h
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
c : σ →₀ ℕ
hc : (if d = c then r else 0) ≠ 0
pos : ∀ (h : d = c) (hc : r ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m
have neg : ∀ (h : ¬d = c) (hc : Ne.{u_1 + 1} (α := R) 0 0), (weight w : (a : σ →₀ ℕ) → M) c = m
Tactic: split_ifs at hc with h
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w ((monomial d : (a : R) → MvPolynomial σ R) r) m
have intro : ∀ ⦃c : σ →₀ ℕ⦄,
  Ne.{u_1 + 1} (α := R) (coeff c ((monomial d : (a : R) → MvPolynomial σ R) r)) 0 → (weight w : (a : σ →₀ ℕ) → M) c = m
Tactic: classical
  intro c hc
  rw [coeff_monomial] at hc
  split_ifs at hc with h
  · subst c
    exact hm
  · contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
intro intro₁ :
  ∀ ⦃c : σ →₀ ℕ⦄ (hc : Ne.{u_1 + 1} (α := R) (coeff c ((monomial d : (a : R) → MvPolynomial σ R) r)) 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w ((monomial d : (a : R) → MvPolynomial σ R) r) m
have intro₂ : ∀ ⦃c : σ →₀ ℕ⦄ (hc : (if d = c then r else 0) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
Tactic: classical
  intro c hc
  rw [coeff_monomial] at hc
  split_ifs at hc with h
  · subst c
    exact hm
  · contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
intro intro₁ :
  ∀ ⦃c : σ →₀ ℕ⦄ (hc : Ne.{u_1 + 1} (α := R) (coeff c ((monomial d : (a : R) → MvPolynomial σ R) r)) 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m
intro₂ : ∀ ⦃c : σ →₀ ℕ⦄ (hc : (if d = c then r else 0) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w ((monomial d : (a : R) → MvPolynomial σ R) r) m
have pos : ∀ ⦃c : σ →₀ ℕ⦄ (h : d = c) (hc : r ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
Tactic: classical
  intro c hc
  rw [coeff_monomial] at hc
  split_ifs at hc with h
  · subst c
    exact hm
  · contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
intro intro₁ :
  ∀ ⦃c : σ →₀ ℕ⦄ (hc : Ne.{u_1 + 1} (α := R) (coeff c ((monomial d : (a : R) → MvPolynomial σ R) r)) 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m
intro₂ : ∀ ⦃c : σ →₀ ℕ⦄ (hc : (if d = c then r else 0) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
pos : ∀ ⦃c : σ →₀ ℕ⦄ (h : d = c) (hc : r ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w ((monomial d : (a : R) → MvPolynomial σ R) r) m
have neg : ∀ ⦃c : σ →₀ ℕ⦄ (h : ¬d = c) (hc : Ne.{u_1 + 1} (α := R) 0 0), (weight w : (a : σ →₀ ℕ) → M) c = m
Tactic: classical
  intro c hc
  rw [coeff_monomial] at hc
  split_ifs at hc with h
  · subst c
    exact hm
  · contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (⊥ : M)
have h : weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
Tactic: have h := weightedTotalDegree_coe w p (MvPolynomial.ne_zero_iff.mpr ⟨d, hd⟩)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h : weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (⊥ : M)
have h₁ : Eq.{u_2 + 1} (α := WithBot M) (p.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M))
  (↑⊥ : WithBot M)
Tactic: simp only [weightedTotalDegree', hp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h :
  Eq.{u_2 + 1} (α := WithBot M) (p.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M))
    (↑⊥ : WithBot M)
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (⊥ : M)
have rw : LE.le.{u_2} (α := WithBot M) ((↑((weight w : (a : σ →₀ ℕ) → M) d) : WithBot M) : WithBot M)
  (p.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) : WithBot M)
Tactic: rw [eq_bot_iff, ← WithBot.coe_le_coe, ← h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
i : σ
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (X i) (w i)
have hm : (weight w : (a : σ →₀ ℕ) → M) (Finsupp.single i 1) = w i
Tactic: apply isWeightedHomogeneous_monomial
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n
⊢ coeff d φ = 0
have aux : ¬coeff d φ ≠ 0
Tactic: have aux := mt (@hφ d) hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0
have rwa : ∀ (aux : coeff d φ = 0), coeff d φ = 0
Tactic: rwa [Classical.not_not] at aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
⊢ m = n
have obtain : ∀ (d : σ →₀ ℕ) (hd : coeff d φ ≠ 0), m = n
Tactic: obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n
have rw : (weight w : (a : σ →₀ ℕ) → M) d = n
Tactic: rw [← hm hd, ← hn hd]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
rw : (weight w : (a : σ →₀ ℕ) → M) d = n
⊢ m = n
have rw₁ : Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M)
Tactic: rw [← hm hd, ← hn hd]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
r : R
⊢ IsWeightedHomogeneous w (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ)
    m
have rw : IsWeightedHomogeneous w (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ)
  (0 + m)
Tactic: rw [← zero_add m]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
⊢ IsWeightedHomogeneous w (HPow.hPow (β := ℕ) φ 0) (HSMul.hSMul (α := ℕ) 0 m)
have zero : IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w 1 0
Tactic: rw [pow_zero, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
⊢ IsWeightedHomogeneous w (φ ^ (n + 1)) ((n + 1) • m)
have succ : IsWeightedHomogeneous w (φ ^ n * φ) (n • m + m)
Tactic: rw [pow_succ, succ_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
⊢ IsWeightedHomogeneous w (φ ^ n) (n • m)
have zero : IsWeightedHomogeneous w (HPow.hPow (β := ℕ) φ 0) (HSMul.hSMul (α := ℕ) 0 m)
Tactic: induction n with
  | zero => rw [pow_zero, zero_smul]; exact isWeightedHomogeneous_one R w
  | succ n ih => rw [pow_succ, succ_nsmul]; exact ih.mul hφ
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
zero : IsWeightedHomogeneous w (HPow.hPow (β := ℕ) φ 0) (HSMul.hSMul (α := ℕ) 0 m)
⊢ IsWeightedHomogeneous w (φ ^ n) (n • m)
have succ : ∀ (n : ℕ) (ih : IsWeightedHomogeneous w (φ ^ n) (n • m)), IsWeightedHomogeneous w (φ ^ (n + 1)) ((n + 1) • m)
Tactic: induction n with
  | zero => rw [pow_zero, zero_smul]; exact isWeightedHomogeneous_one R w
  | succ n ih => rw [pow_succ, succ_nsmul]; exact ih.mul hφ
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
have refine_1 : (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsWeightedHomogeneous w (φ i) (n i)) →
  IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
refine_1 :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
⊢ (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ((∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
        IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
      (∀ i ∈ insert a s, IsWeightedHomogeneous w (φ i) (n i)) →
        IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH :
  (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)
have refine_2 : IsWeightedHomogeneous w (φ i * ∏ i ∈ s, φ i) (n i + ∑ i ∈ s, n i)
Tactic: simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH :
  (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (φ i * ∏ i ∈ s, φ i) (n i + ∑ i ∈ s, n i)
have apply : ∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)
Tactic: apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
have refine_1 : (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsWeightedHomogeneous w (φ i) (n i)) →
  IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
Tactic: classical
  refine Finset.induction_on s ?_ ?_
  · intro
    simp only [isWeightedHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
  · intro i s his IH h
    simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
    apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
    intro j hjs
    exact h j (Finset.mem_insert_of_mem hjs)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
refine_1 :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
⊢ (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ((∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
        IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
      (∀ i ∈ insert a s, IsWeightedHomogeneous w (φ i) (n i)) →
        IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)
Tactic: classical
  refine Finset.induction_on s ?_ ?_
  · intro
    simp only [isWeightedHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
  · intro i s his IH h
    simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
    apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
    intro j hjs
    exact h j (Finset.mem_insert_of_mem hjs)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)) = (↑n : WithBot M)
have a : (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)) ≤ (↑n : WithBot M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
a : (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)) ≤ (↑n : WithBot M)
⊢ (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)) = (↑n : WithBot M)
have a₁ : (↑n : WithBot M) ≤ φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)) ≤ (↑n : WithBot M)
have a : ∀ (b : σ →₀ ℕ), coeff b φ ≠ 0 → (weight w : (a : σ →₀ ℕ) → M) b ≤ n
Tactic: simp only [Finset.sup_le_iff, mem_support_iff, WithBot.coe_le_coe]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ (↑n : WithBot M) ≤ φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)
have a : ∀ (d : σ →₀ ℕ) (hd : coeff d φ ≠ 0),
  (↑n : WithBot M) ≤ φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)
Tactic: obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (↑n : WithBot M) ≤ φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)
have a : LE.le.{u_2} (α := WithBot M) ((↑((weight w : (a : σ →₀ ℕ) → M) d) : WithBot M) : WithBot M)
  (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) : WithBot M)
Tactic: simp only [← hφ hd]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ LE.le.{u_2} (α := WithBot M) ((↑((weight w : (a : σ →₀ ℕ) → M) d) : WithBot M) : WithBot M)
    (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) : WithBot M)
have hd₁ : d ∈ φ.support
Tactic: replace hd := Finsupp.mem_support_iff.mpr hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial :
  ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w : (a : σ →₀ ℕ) → M) d = m),
    motive ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
⊢ motive p hp
have suffices : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) sorry
Tactic: suffices h : ∀ a, motive (C a * p) (.C_mul hp _) by simpa using h 1
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial :
  ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w : (a : σ →₀ ℕ) → M) d = m),
    motive ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
a_1 : R
x : MvPolynomial σ R
h :
  Membership.mem (γ := Set (MvPolynomial σ R))
    {p : MvPolynomial σ R |
      ∃ (hp : IsWeightedHomogeneous w p m),
        ∀ (a : R),
          motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯}
    x
w_1 : IsWeightedHomogeneous w x m
hx : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x) ⋯
a : R
⊢ motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) (a_1 • x)) ⋯
have simp_rw : motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (a * a_1) : MvPolynomial σ R) x) sorry
Tactic: simp_rw [Algebra.smul_def, algebraMap_eq, ← mul_assoc, ← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial :
  ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w : (a : σ →₀ ℕ) → M) d = m),
    motive ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
A : Submodule R (MvPolynomial σ R) :=
  {
    carrier :=
      {p : MvPolynomial σ R |
        ∃ (hp : IsWeightedHomogeneous w p m),
          ∀ (a : R),
            motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯},
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯
have hp₁ : Membership.mem (γ := Submodule R (MvPolynomial σ R))
  (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m})) p
Tactic: rw [← mem_weightedHomogeneousSubmodule, weightedHomogeneousSubmodule_eq_finsupp_supported,
    Finsupp.supported_eq_span_single] at hp
Cleared hypotheses: A