awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)
revert :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
have refine_1 : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (φ i).IsHomogeneous (n i)),
  IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
Tactic: classical
  revert h
  refine Finset.induction_on s ?_ ?_
  · intro
    simp only [isHomogeneous_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 (by grind)).mul (IH _)
    grind
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)
revert :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
refine_1 :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (φ i).IsHomogeneous (n i)),
    IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)),
        IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
      ∀ (h : ∀ i ∈ insert a s, (φ i).IsHomogeneous (n i)),
        IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)
Tactic: classical
  revert h
  refine Finset.induction_on s ?_ ?_
  · intro
    simp only [isHomogeneous_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 (by grind)).mul (IH _)
    grind
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (φ ^ n).IsHomogeneous (m * n)
have rw : IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ _i ∈ Finset.range n, φ) (m * n)
Tactic: rw [show φ ^ n = ∏ _i ∈ Finset.range n, φ by simp]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ _i ∈ Finset.range n, φ) (m * n)
have rw : IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ _i ∈ Finset.range n, φ) (∑ _i ∈ Finset.range n, m)
Tactic: rw [show m * n = ∑ _i ∈ Finset.range n, m by simp [mul_comm]]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
⊢ (MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
have h : ∀ i ∈ (AddMonoidAlgebra.coeff φ).support,
  IsHomogeneous.{u_2, u_4} (σ := τ) (R := S)
    ((fun (s : σ →₀ ℕ) (a : R) ↦
        HMul.hMul (α := MvPolynomial τ S) (β := MvPolynomial τ S)
          ((f : (a : R) → MvPolynomial τ S) a : MvPolynomial τ S)
          (s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : MvPolynomial τ S))
      i ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i))
    (n * m)
Tactic: apply IsHomogeneous.sum
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
⊢ IsHomogeneous.{u_2, u_4} (σ := τ) (R := S)
    ((fun (s : σ →₀ ℕ) (a : R) ↦
        HMul.hMul (α := MvPolynomial τ S) (β := MvPolynomial τ S)
          ((f : (a : R) → MvPolynomial τ S) a : MvPolynomial τ S)
          (s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : MvPolynomial τ S))
      i ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i))
    (n * m)
have h : IsHomogeneous.{u_2, u_4} (σ := τ) (R := S)
  ((fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ S) (β := MvPolynomial τ S) ((f : (a : R) → MvPolynomial τ S) a : MvPolynomial τ S)
        (s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : MvPolynomial τ S))
    i ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i))
  (0 + n * m)
Tactic: rw [← zero_add (n * m)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
⊢ IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) (i.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) (n * m)
have h : n * m = ∑ i_1 ∈ i.support, HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) i_1 : ℕ)
Tactic: convert! IsHomogeneous.prod _ _ (fun k ↦ n * i k) _
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
h : n * m = ∑ i_1 ∈ i.support, HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) i_1 : ℕ)
⊢ IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) (i.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) (n * m)
have convert_6 : ∀ i_1 ∈ i.support,
  IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((fun (n : σ) (e : ℕ) ↦ g n ^ e) i_1 ((i : (a : σ) → ℕ) i_1))
    ((fun (k : σ) ↦ HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) k : ℕ)) i_1)
Tactic: convert! IsHomogeneous.prod _ _ (fun k ↦ n * i k) _
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
⊢ n * m = ∑ i_1 ∈ i.support, HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) i_1 : ℕ)
have hi₁ : Ne.{u_3 + 1} (α := R) ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i : R) (0 : R)
Tactic: rw [Finsupp.mem_support_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : Ne.{u_3 + 1} (α := R) ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i : R) (0 : R)
⊢ n * m = ∑ i_1 ∈ i.support, HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) i_1 : ℕ)
have h : (n * i.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i)) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
Tactic: rw [← Finset.mul_sum, ← hφ hi, weight_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : Ne.{u_3 + 1} (α := R) ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i : R) (0 : R)
⊢ (n * i.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i)) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
have h : (n * i.sum fun (i : σ) (c : ℕ) ↦ c * 1 i) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
Tactic: simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : Ne.{u_3 + 1} (α := R) ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i : R) (0 : R)
h : (n * i.sum fun (i : σ) (c : ℕ) ↦ c * 1 i) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
⊢ (n * i.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i)) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
have h₁ : n * ∑ x ∈ i.support, HMul.hMul (α := ℕ) (β := ℕ) ((i : (a : σ) → ℕ) x : ℕ) (1 x : ℕ) =
  n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
Tactic: simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : Ne.{u_3 + 1} (α := R) ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i : R) (0 : R)
h : (n * i.sum fun (i : σ) (c : ℕ) ↦ c * 1 i) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
h₁ :
  n * ∑ x ∈ i.support, HMul.hMul (α := ℕ) (β := ℕ) ((i : (a : σ) → ℕ) x : ℕ) (1 x : ℕ) =
    n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
⊢ (n * i.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i)) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
have h₂ : n * ∑ x ∈ i.support, HMul.hMul (α := ℕ) (β := ℕ) ((i : (a : σ) → ℕ) x : ℕ) (1 : ℕ) =
  n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
Tactic: simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
f : R →+* S
⊢ IsHomogeneous.{u_1, u_4} (σ := σ) (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) n
have rw : IsHomogeneous.{u_1, u_4} (σ := σ) (R := S)
  ((eval₂Hom (RingHom.comp C f) X : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) n
Tactic: rw [map_eq_eval₂Hom_C_comp]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
⊢ φ.totalDegree ≤ n
have a : ∀ b ∈ φ.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
have hd₁ : coeff d φ ≠ 0
Tactic: rw [mem_support_iff] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
have a : ∑ x ∈ d.support, (d : (a : σ) → ℕ) x ≤ n
Tactic: simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
    le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
a : ∑ x ∈ d.support, (d : (a : σ) → ℕ) x ≤ n
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
have a₁ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
Tactic: simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
    le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
a : ∑ x ∈ d.support, (d : (a : σ) → ℕ) x ≤ n
a₁ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
have a₂ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i))
Tactic: simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
    le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
a : ∑ x ∈ d.support, (d : (a : σ) → ℕ) x ≤ n
a₁ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
a₂ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i))
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
have a₃ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c 1)
Tactic: simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
    le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
a : ∑ x ∈ d.support, (d : (a : σ) → ℕ) x ≤ n
a₁ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
a₂ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i))
a₃ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c 1)
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
have a₄ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ c * 1)
Tactic: simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
    le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
a : ∑ x ∈ d.support, (d : (a : σ) → ℕ) x ≤ n
a₁ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
a₂ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i))
a₃ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c 1)
a₄ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ c * 1)
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
have a₅ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ c)
Tactic: simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
    le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
a : ∑ x ∈ d.support, (d : (a : σ) → ℕ) x ≤ n
a₁ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
a₂ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i))
a₃ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c 1)
a₄ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ c * 1)
a₅ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ c)
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
have a₆ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x)
Tactic: simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
    le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ φ.totalDegree = n
have apply : n ≤ φ.totalDegree
Tactic: apply le_antisymm hφ.totalDegree_le
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ n ≤ φ.totalDegree
have obtain : ∀ (d : σ →₀ ℕ) (hd : coeff d φ ≠ 0), n ≤ φ.totalDegree
Tactic: obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ n ≤ φ.totalDegree
have simp : LE.le (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
  (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x : ℕ)
Tactic: simp only [← hφ hd, MvPolynomial.totalDegree, Finsupp.sum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ LE.le (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
    (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x : ℕ)
have hd₁ : d ∈ φ.support
Tactic: replace hd := Finsupp.mem_support_iff.mpr hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ LE.le (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
    (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x : ℕ)
have simp : LE.le (α := ℕ) (d.sum fun (i : σ) (c : ℕ) ↦ c) (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x)
Tactic: simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
have rw : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R)
  (∑ x ∈ φ.support,
    (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ)))
  n
Tactic: rw [← φ.support_sum_monomial_coeff, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R)
    (∑ x ∈ φ.support,
      (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ)))
    n
have simp_rw : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R)
  (∑ x ∈ φ.support, (monomial (mapDomain f x) : (a : R) → MvPolynomial τ R) (coeff x φ)) n
Tactic: simp_rw [rename_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R)
    (∑ x ∈ φ.support, (monomial (mapDomain f x) : (a : R) → MvPolynomial τ R) (coeff x φ)) n
have apply : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support), (degree : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) = n
Tactic: apply IsHomogeneous.sum _ _ _ fun d hd ↦ isHomogeneous_monomial _ _
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (degree : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) = n
have apply : (d.sum fun (a : σ) (m : ℕ) ↦ (AddMonoidHom.id ℕ : (a : ℕ) → ℕ) m) = n
Tactic: apply (Finsupp.sum_mapDomain_index_addMonoidHom fun _ ↦ .id ℕ).trans
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun (a : σ) (m : ℕ) ↦ (AddMonoidHom.id ℕ : (a : ℕ) → ℕ) m) = n
have h₁ : Eq (α := ℕ) (d.sum fun (a : σ) (m : ℕ) ↦ (AddMonoidHom.id ℕ : (a : ℕ) → ℕ) m : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
Tactic: convert! h (mem_support_iff.mp hd)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n ↔
    φ.IsHomogeneous n
have refine : ∀ (h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n)
  (d : σ →₀ ℕ) (hd : coeff d φ ≠ 0), (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
Tactic: refine ⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
have h₁ : Eq (α := ℕ) ((weight 1 : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
Tactic: convert! ← @h (d.mapDomain f) _
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
h₁ : Eq (α := ℕ) ((weight 1 : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
have convert! : Ne.{u_3 + 1} (α := R) (coeff (mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
Tactic: convert! ← @h (d.mapDomain f) _
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ Eq (α := ℕ) ((weight 1 : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
have h₁ : Eq (α := ℕ) ((mapDomain f d).sum fun (i : τ) (c : ℕ) ↦ c) (d.sum fun (i : σ) (c : ℕ) ↦ c)
Tactic: simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]