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
simp_rw :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) ''
        {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
simp_rw₁ :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) '' Set.range fun (a : σ) ↦ single a 1))
    (Submodule.span R (Set.range X))
simp_rw₂ :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      (Set.range (ι := σ)
        ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) ∘ fun (a : σ) ↦ single a 1)))
    (Submodule.span R (Set.range X))
⊢ Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
have simp_rw₃ : Eq (α := Submodule R (MvPolynomial σ R))
  (Submodule.span R (Set.range fun (x : σ) ↦ (monomial (single x 1) : (a : R) → MvPolynomial σ R) 1))
  (Submodule.span R (Set.range X))
Tactic: simp_rw [MvPolynomial.single_eq_monomial, ← Finsupp.range_single_one, ← Set.range_comp,
    Function.comp_def, ← X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
simp_rw :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) ''
        {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
simp_rw₁ :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) '' Set.range fun (a : σ) ↦ single a 1))
    (Submodule.span R (Set.range X))
simp_rw₂ :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      (Set.range (ι := σ)
        ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) ∘ fun (a : σ) ↦ single a 1)))
    (Submodule.span R (Set.range X))
simp_rw₃ :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R (Set.range fun (x : σ) ↦ (monomial (single x 1) : (a : R) → MvPolynomial σ R) 1))
    (Submodule.span R (Set.range X))
⊢ Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
have simp_rw₄ : Eq (α := Submodule R (MvPolynomial σ R))
  (Submodule.span R (Set.range fun (x : σ) ↦ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x) 1))
  (Submodule.span R (Set.range X))
Tactic: simp_rw [MvPolynomial.single_eq_monomial, ← Finsupp.range_single_one, ← Set.range_comp,
    Function.comp_def, ← X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : (degree : (a : σ →₀ ℕ) → ℕ) d = n
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) ((monomial d : (a : R) → MvPolynomial σ R) r) n
have hn₁ : (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n
Tactic: rw [degree_eq_weight_one] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have rw : NonTorsionWeight.{0, u_1} (M := ℕ) (σ := σ) 1
Tactic: rw [← weightedTotalDegree_one, weightedTotalDegree_eq_zero_iff _ p]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p.IsHomogeneous 0
have rw : Eq (α := ℕ) (weightedTotalDegree 1 p) 0 ↔ p.IsHomogeneous 0
Tactic: rw [← weightedTotalDegree_one,
    ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : MvPolynomial σ R
rw : Eq (α := ℕ) (weightedTotalDegree 1 p) 0 ↔ p.IsHomogeneous 0
⊢ p.totalDegree = 0 ↔ p.IsHomogeneous 0
have rw₁ : IsWeightedHomogeneous (M := ℕ) 1 p 0 ↔ p.IsHomogeneous 0
Tactic: rw [← weightedTotalDegree_one,
    ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : MvPolynomial σ R
rw : Eq (α := ℕ) (weightedTotalDegree 1 p) 0 ↔ p.IsHomogeneous 0
rw₁ : IsWeightedHomogeneous (M := ℕ) 1 p 0 ↔ p.IsHomogeneous 0
⊢ p.totalDegree = 0 ↔ p.IsHomogeneous 0
have rw₂ : IsWeightedHomogeneous (M := ℕ) 1 p 0 ↔ IsWeightedHomogeneous (M := ℕ) 1 p 0
Tactic: rw [← weightedTotalDegree_one,
    ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 0) 1
have h : ∀ (x : MvPolynomial σ R),
  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 0) x ↔
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
x : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 0) x ↔
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x
have h : x = (C : (a : R) → MvPolynomial σ R) (coeff 0 x) ↔ ∃ (y : R), (C : (a : R) → MvPolynomial σ R) y = x
Tactic: rw [MvPolynomial.mem_homogeneousSubmodule,
    ← MvPolynomial.totalDegree_zero_iff_isHomogeneous, Submodule.mem_one,
    MvPolynomial.algebraMap_eq, MvPolynomial.totalDegree_eq_zero_iff_eq_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) ((C : (a : R) → MvPolynomial σ R) r) 0
have hn : Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
Tactic: apply isHomogeneous_monomial
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
i : σ
⊢ IsHomogeneous.{u_1, u_3} (R := R) (X i) 1
have hn : Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (single i 1) : ℕ) (1 : ℕ)
Tactic: apply isHomogeneous_monomial
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
a : σ
b : ℕ
f : σ →₀ ℕ
h_1 : a ∉ f.support
h_2 : b ≠ 0
h :
  Membership.mem (α := MvPolynomial σ R)
    (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
      ((degree : (a : σ →₀ ℕ) → ℕ) f : ℕ))
    ((monomial f : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ Membership.mem (α := MvPolynomial σ R)
    (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
      ((degree : (a : σ →₀ ℕ) → ℕ) (single a b + f) : ℕ))
    ((monomial (single a b + f) : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
have single_add : HMul.hMul (β := MvPolynomial σ R) (HPow.hPow (α := MvPolynomial σ R) (X a) b)
    ((monomial f : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ∈
  HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) b *
    HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
      ((degree : (a : σ →₀ ℕ) → ℕ) f : ℕ)
Tactic: rw [map_add, Finsupp.degree_single, monomial_single_add, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
s : σ →₀ ℕ
⊢ Membership.mem (α := MvPolynomial σ R)
    (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
      ((degree : (a : σ →₀ ℕ) → ℕ) s : ℕ))
    ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
have zero : Membership.mem (α := MvPolynomial σ R)
  (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
    ((degree : (a : σ →₀ ℕ) → ℕ) 0 : ℕ))
  ((monomial 0 : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: induction s using Finsupp.induction with
  | zero => simp
  | single_add a b f _ _ h =>
    rw [map_add, Finsupp.degree_single, monomial_single_add, pow_add]
    exact Submodule.mul_mem_mul (Submodule.pow_mem_pow _ (isHomogeneous_X R a) _) h
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
s : σ →₀ ℕ
zero :
  Membership.mem (α := MvPolynomial σ R)
    (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
      ((degree : (a : σ →₀ ℕ) → ℕ) 0 : ℕ))
    ((monomial 0 : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ Membership.mem (α := MvPolynomial σ R)
    (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
      ((degree : (a : σ →₀ ℕ) → ℕ) s : ℕ))
    ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
have single_add : ∀ (a : σ) (b : ℕ) (f : σ →₀ ℕ),
  a ∉ f.support →
    b ≠ 0 →
      ∀
        (h :
          Membership.mem (α := MvPolynomial σ R)
            (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
              ((degree : (a : σ →₀ ℕ) → ℕ) f : ℕ))
            ((monomial f : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)),
        Membership.mem (α := MvPolynomial σ R)
          (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1)
            ((degree : (a : σ →₀ ℕ) → ℕ) (single a b + f) : ℕ))
          ((monomial (single a b + f) : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: induction s using Finsupp.induction with
  | zero => simp
  | single_add a b f _ _ h =>
    rw [map_add, Finsupp.degree_single, monomial_single_add, pow_add]
    exact Submodule.mul_mem_mul (Submodule.pow_mem_pow _ (isHomogeneous_X R a) _) h
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n = homogeneousSubmodule σ R n
have refine_1 : HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n ≤ homogeneousSubmodule σ R n
Tactic: refine le_antisymm ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
refine_1 : HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n ≤ homogeneousSubmodule σ R n
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n = homogeneousSubmodule σ R n
have refine_2 : ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n) x),
  x ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
Tactic: refine le_antisymm ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
ih : HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n ≤ homogeneousSubmodule σ R n
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) (n + 1) ≤
    homogeneousSubmodule σ R (n + 1)
have refine_1 : HMul.hMul (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n) (homogeneousSubmodule σ R 1) ≤
  homogeneousSubmodule σ R (n + 1)
Tactic: grw [pow_add, pow_one, ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n ≤ homogeneousSubmodule σ R n
have refine_1 : HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1) 0 ≤ homogeneousSubmodule σ R 0
Tactic: induction n with
    | zero => simp [homogeneousSubmodule_zero]
    | succ n ih =>
      grw [pow_add, pow_one, ih]
      apply homogeneousSubmodule_mul
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
refine_1 :
  HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1) 0 ≤ homogeneousSubmodule σ R 0
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n ≤ homogeneousSubmodule σ R n
have refine_1₁ : ∀ (n : ℕ)
  (ih : HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n ≤ homogeneousSubmodule σ R n),
  HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) (n + 1) ≤
    homogeneousSubmodule σ R (n + 1)
Tactic: induction n with
    | zero => simp [homogeneousSubmodule_zero]
    | succ n ih =>
      grw [pow_add, pow_one, ih]
      apply homogeneousSubmodule_mul
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n) x
⊢ x ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
have hx₁ : x.IsHomogeneous n
Tactic: simp only [mem_homogeneousSubmodule] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
r : R
hr : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
⊢ Membership.mem (α := MvPolynomial σ R)
    (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n)
    ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
have h : n = (degree : (a : σ →₀ ℕ) → ℕ) d
Tactic: convert! monomial_mem_homogeneousSubmodule_pow_degree _ _
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
r : R
hr : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
⊢ n = (degree : (a : σ →₀ ℕ) → ℕ) d
have h : n = (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d
Tactic: rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
r : R
hr : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
h : n = (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d
⊢ n = (degree : (a : σ →₀ ℕ) → ℕ) d
have h₁ : n = (weight 1 : (a : σ →₀ ℕ) → ℕ) d
Tactic: rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
r : R
hr : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
h : n = (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d
h₁ : n = (weight 1 : (a : σ →₀ ℕ) → ℕ) d
⊢ n = (degree : (a : σ →₀ ℕ) → ℕ) d
have h₂ : Eq (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
Tactic: rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : x.IsHomogeneous n
⊢ x ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
have refine_2 : 0 ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
Tactic: induction hx using IsWeightedHomogeneous.induction_on with
    | zero => simp
    | add p q _ _ hp hq => exact Submodule.add_mem _ hp hq
    | monomial d r hr =>
      convert! monomial_mem_homogeneousSubmodule_pow_degree _ _
      rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : x.IsHomogeneous n
refine_2 : 0 ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
⊢ x ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
have refine_2₁ : ∀ (p q : MvPolynomial σ R),
  IsWeightedHomogeneous 1 p n →
    IsWeightedHomogeneous 1 q n →
      ∀ (hp : p ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n)
        (hq : q ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n),
        p + q ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
Tactic: induction hx using IsWeightedHomogeneous.induction_on with
    | zero => simp
    | add p q _ _ hp hq => exact Submodule.add_mem _ hp hq
    | monomial d r hr =>
      convert! monomial_mem_homogeneousSubmodule_pow_degree _ _
      rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : x.IsHomogeneous n
refine_2 : 0 ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
refine_2₁ :
  ∀ (p q : MvPolynomial σ R),
    IsWeightedHomogeneous 1 p n →
      IsWeightedHomogeneous 1 q n →
        ∀ (hp : p ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n)
          (hq : q ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n),
          p + q ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
⊢ x ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
have refine_2₂ : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n),
  Membership.mem (α := MvPolynomial σ R)
    (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n)
    ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: induction hx using IsWeightedHomogeneous.induction_on with
    | zero => simp
    | add p q _ _ hp hq => exact Submodule.add_mem _ hp hq
    | monomial d r hr =>
      convert! monomial_mem_homogeneousSubmodule_pow_degree _ _
      rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]
Cleared hypotheses: hx
-- 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 : (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ coeff d φ = 0
have hd₁ : (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ n
Tactic: rw [degree_eq_weight_one] 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
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
⊢ 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.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n
have rw : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
Tactic: rw [← hm hd, ← hn hd]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
rw : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
⊢ m = n
have rw₁ : Eq (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
Tactic: rw [← hm hd, ← hn hd]
-- 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)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
have revert : ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
Tactic: revert h
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)), 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: refine Finset.induction_on s ?_ ?_
-- 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 : ι → ℕ
refine_1 :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (φ i).IsHomogeneous (n i)),
    IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
⊢ ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (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: refine Finset.induction_on s ?_ ?_
-- 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_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)
have refine_2 : (φ i * ∏ i ∈ s, φ i).IsHomogeneous (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.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
⊢ (φ i * ∏ i ∈ s, φ i).IsHomogeneous (n i + ∑ i ∈ s, n i)
have apply : ∀ i ∈ s, (φ i).IsHomogeneous (n i)
Tactic: apply (h i (by grind)).mul (IH _)
-- 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)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
have revert : ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ 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