awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
h : coeff c a = 0
a₁ : r • coeff c a = 0
⊢ False

Tactic:
apply hc
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
h : coeff c a = 0
a₁ : HSMul.hSMul (β := R) r 0 = 0
⊢ r • coeff c a = 0

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
h : coeff c a = 0
⊢ HSMul.hSMul (β := R) r 0 = 0

Tactic:
smul_zero r

Premises used: smul_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
h : coeff c a = 0
⊢ HSMul.hSMul (β := R) r 0 = 0

Tactic:
exact smul_zero r

Premises used: smul_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R 1 n) (homogeneousSubmodule σ R n)

Tactic:
rfl

Premises used: MvPolynomial.weightedHomogeneousSubmodule, MvPolynomial.homogeneousSubmodule, setOf, MvPolynomial.IsHomogeneous, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n) p ↔ p.IsHomogeneous n

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MvPolynomial.IsWeightedHomogeneous, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
simp_rw :
  Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n)
    (supported R R {d : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n})
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n)
    (supported R R {d : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) d = n})

Tactic:
simp_rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n)
    (supported R R {d : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n})

Tactic:
weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n

Premises used: MvPolynomial.weightedHomogeneousSubmodule, MvPolynomial.homogeneousSubmodule, setOf, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, OfNat.ofNat, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n)
    (supported R R {d : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n})

Tactic:
exact weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n

Premises used: MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
rw :
  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))
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) (Submodule.span R (Set.range X))

Tactic:
rw [MvPolynomial.homogeneousSubmodule_eq_finsupp_supported, Finsupp.supported_eq_span_single]

Premises used: Finsupp.supported_eq_span_single, MvPolynomial.homogeneousSubmodule_eq_finsupp_supported
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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))
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))
⊢ 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))

Tactic:
simp_rw [MvPolynomial.single_eq_monomial, ← Finsupp.range_single_one, ← Set.range_comp,
    Function.comp_def, ← X_pow_eq_monomial, pow_one]

Premises used: Set.range_comp, MvPolynomial.X_pow_eq_monomial, MvPolynomial.single_eq_monomial, Function.comp_def, pow_one, Finsupp.range_single_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : (degree : (a : σ →₀ ℕ) → ℕ) d = n
⊢ (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n

Tactic:
rw [degree_eq_weight_one] at hn

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) ((monomial d : (a : R) → MvPolynomial σ R) r) n

Tactic:
isWeightedHomogeneous_monomial 1 d r hn

Premises used: MvPolynomial.isWeightedHomogeneous_monomial, OfNat.ofNat, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) ((monomial d : (a : R) → MvPolynomial σ R) r) n

Tactic:
exact isWeightedHomogeneous_monomial 1 d r hn

Premises used: MvPolynomial.isWeightedHomogeneous_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : MvPolynomial σ R
rw : NonTorsionWeight.{0, u_1} (M := ℕ) (σ := σ) 1
⊢ p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
rw [← weightedTotalDegree_one, weightedTotalDegree_eq_zero_iff _ p]

Premises used: MvPolynomial.weightedTotalDegree_eq_zero_iff, MvPolynomial.weightedTotalDegree_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : MvPolynomial σ R
⊢ NonTorsionWeight.{0, u_1} (M := ℕ) (σ := σ) 1

Tactic:
nonTorsionWeight_of (Function.const σ one_ne_zero)

Premises used: MvPolynomial.nonTorsionWeight_of, Function.const, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : MvPolynomial σ R
⊢ NonTorsionWeight.{0, u_1} (M := ℕ) (σ := σ) 1

Tactic:
exact nonTorsionWeight_of (Function.const σ one_ne_zero)

Premises used: MvPolynomial.nonTorsionWeight_of, Function.const, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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
rw₂ rw₃ : IsWeightedHomogeneous (M := ℕ) 1 p 0 ↔ IsWeightedHomogeneous (M := ℕ) 1 p 0
⊢ p.totalDegree = 0 ↔ p.IsHomogeneous 0

Tactic:
rw [← weightedTotalDegree_one,
    ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]

Premises used: MvPolynomial.isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, MvPolynomial.weightedTotalDegree_one, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
h :
  ∀ (x : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 0) x ↔
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 0) 1

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
x : MvPolynomial σ R
h : x = (C : (a : R) → MvPolynomial σ R) (coeff 0 x) ↔ ∃ (y : R), (C : (a : R) → MvPolynomial σ R) y = x
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 0) x ↔
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x

Tactic:
rw [MvPolynomial.mem_homogeneousSubmodule,
    ← MvPolynomial.totalDegree_zero_iff_isHomogeneous, Submodule.mem_one,
    MvPolynomial.algebraMap_eq, MvPolynomial.totalDegree_eq_zero_iff_eq_C]

Premises used: MvPolynomial.totalDegree_eq_zero_iff_eq_C, MvPolynomial.mem_homogeneousSubmodule, Submodule.mem_one, MvPolynomial.algebraMap_eq, MvPolynomial.totalDegree_zero_iff_isHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
x : MvPolynomial σ R
⊢ x = (C : (a : R) → MvPolynomial σ R) (coeff 0 x) ↔ ∃ (y : R), (C : (a : R) → MvPolynomial σ R) y = x

Tactic:
grind [coeff_zero_C]

Premises used: MvPolynomial.coeff_zero_C
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
hn : Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) ((C : (a : R) → MvPolynomial σ R) r) 0

Tactic:
apply isHomogeneous_monomial

Premises used: MvPolynomial.isHomogeneous_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
⊢ Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) 0 : ℕ) (0 : ℕ)

Tactic:
simp only [degree_apply, Finsupp.support_zero, zero_apply, Finset.sum_const_zero]

Premises used: Finsupp.support_zero, Finsupp.degree_apply, Finset.sum_const_zero, Finsupp.zero_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) 0 n

Tactic:
(homogeneousSubmodule σ R n).zero_mem

Premises used: Set.Mem, MvPolynomial.homogeneousSubmodule, setOf, Submodule.zero_mem, MvPolynomial.IsWeightedHomogeneous, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) 1 0

Tactic:
isHomogeneous_C _ _

Premises used: MvPolynomial.isHomogeneous_C, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
i : σ
hn : Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (single i 1) : ℕ) (1 : ℕ)
⊢ IsHomogeneous.{u_1, u_3} (R := R) (X i) 1

Tactic:
apply isHomogeneous_monomial

Premises used: MvPolynomial.isHomogeneous_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
i : σ
⊢ Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (single i 1) : ℕ) (1 : ℕ)

Tactic:
simp only [degree_apply, Finsupp.support_single _ one_ne_zero, Finset.sum_singleton,
    single_eq_same]

Premises used: Finsupp.support_single, Finsupp.single_eq_same, Finsupp.degree_apply, Finset.sum_singleton, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
⊢ 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:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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)
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 : ℕ)
⊢ 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:
rw [map_add, Finsupp.degree_single, monomial_single_add, pow_add]

Premises used: pow_add, map_add, Finsupp.degree_single, MvPolynomial.monomial_single_add
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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)
⊢ 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:
Submodule.mul_mem_mul (Submodule.pow_mem_pow _ (isHomogeneous_X R a) _) h

Premises used: Submodule.mul_mem_mul, Set.Mem, Submodule.pow_mem_pow
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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)
⊢ 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:
exact Submodule.mul_mem_mul (Submodule.pow_mem_pow _ (isHomogeneous_X R a) _) h

Premises used: Submodule.mul_mem_mul, Submodule.pow_mem_pow
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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)
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)
⊢ 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)

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

Premises used: pow_add, map_add, Finsupp.single_add, Finsupp.degree_single, MvPolynomial.monomial_single_add
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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

Tactic:
le_antisymm ?_ fun x hx ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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
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
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n = homogeneousSubmodule σ R n

Tactic:
refine le_antisymm ?_ fun x hx ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (homogeneousSubmodule σ R 1) 0 ≤ homogeneousSubmodule σ R 0

Tactic:
simp [homogeneousSubmodule_zero]

Premises used: MvPolynomial.homogeneousSubmodule_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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
refine_1 :
  HMul.hMul (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n) (homogeneousSubmodule σ R 1) ≤
    homogeneousSubmodule σ R (n + 1)
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) (n + 1) ≤
    homogeneousSubmodule σ R (n + 1)

Tactic:
grw [pow_add, pow_one, ih]

Premises used: pow_add, pow_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n) (homogeneousSubmodule σ R 1) ≤
    homogeneousSubmodule σ R (n + 1)

Tactic:
apply homogeneousSubmodule_mul

Premises used: MvPolynomial.homogeneousSubmodule_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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
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)
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n ≤ homogeneousSubmodule σ R n

Tactic:
induction n with
    | zero => simp [homogeneousSubmodule_zero]
    | succ n ih =>
      grw [pow_add, pow_one, ih]
      apply homogeneousSubmodule_mul

Premises used: pow_add, MvPolynomial.homogeneousSubmodule_zero, pow_one, MvPolynomial.homogeneousSubmodule_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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.IsHomogeneous n

Tactic:
simp only [mem_homogeneousSubmodule] at hx

Premises used: MvPolynomial.mem_homogeneousSubmodule
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
⊢ 0 ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x p q : MvPolynomial σ R
hp_1 : IsWeightedHomogeneous 1 p n
hq_1 : 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:
Submodule.add_mem _ hp hq

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x p q : MvPolynomial σ R
hp_1 : IsWeightedHomogeneous 1 p n
hq_1 : 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:
exact Submodule.add_mem _ hp hq

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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)
      ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ))
    ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
monomial_mem_homogeneousSubmodule_pow_degree _ _

Premises used: MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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 = (degree : (a : σ →₀ ℕ) → ℕ) d
⊢ Membership.mem (α := MvPolynomial σ R)
    (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n)
    ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
convert! monomial_mem_homogeneousSubmodule_pow_degree _ _

Premises used: MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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
h₂ h₃ : Eq (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
⊢ n = (degree : (a : σ →₀ ℕ) → ℕ) d

Tactic:
rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]

Premises used: Finsupp.degree_eq_weight_one, Pi.one_def