awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hnR : (↑n : Cardinal.{u_5}) ≤ #R
h : F ≠ 0
obtain :
  ∀ (k : ℕ) (f : Fin k → σ) (hf : Function.Injective f) (F : MvPolynomial (Fin k) R)
    (hF : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F) n)
    (h :
      Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
        (0 : MvPolynomial σ R)),
    ∃ (r : σ → R),
      Ne.{u_5 + 1} (α := R)
        ((eval r : (a : MvPolynomial σ R) → R)
            ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R) :
          R)
        (0 : R)
⊢ ∃ (r : σ → R), Ne.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) (0 : R)

Tactic:
obtain ⟨k, f, hf, F, rfl⟩ := exists_fin_rename F

Premises used: MvPolynomial.exists_fin_rename, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hnR : (↑n : Cardinal.{u_5}) ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
hF : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) 0) n
h : Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) 0) 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hnR : (↑n : Cardinal.{u_5}) ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F) n
h :
  Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
⊢ F ≠ 0

Tactic:
have hF₀ : F ≠ 0 := by rintro rfl; simp at h
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hnR : (↑n : Cardinal.{u_5}) ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F) n
h :
  Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
hF₀ : F ≠ 0
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hF : F.IsHomogeneous n)
    (h :
      Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
        (0 : MvPolynomial σ R))
    (hF₀ : F ≠ 0), F.IsHomogeneous n
⊢ F.IsHomogeneous n

Tactic:
rwa [rename_isHomogeneous_iff hf] at hF

Premises used: MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hnR : (↑n : Cardinal.{u_5}) ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F) n
h :
  Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
hF₀ : F ≠ 0
⊢ F.IsHomogeneous n

Tactic:
have hF : F.IsHomogeneous n := by rwa [rename_isHomogeneous_iff hf] at hF
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hnR : (↑n : Cardinal.{u_5}) ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF_1 : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F) n
h :
  Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
hF₀ : F ≠ 0
hF : F.IsHomogeneous n
obtain :
  ∀ (r : Fin k → R) (hr : Ne (α := R) ((eval r : (a : MvPolynomial (Fin k) R) → R) F : R) (0 : R)),
    ∃ (r : σ → R),
      Ne.{u_5 + 1} (α := R)
        ((eval r : (a : MvPolynomial σ R) → R)
            ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R) :
          R)
        (0 : R)
⊢ ∃ (r : σ → R),
    Ne.{u_5 + 1} (α := R)
      ((eval r : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R) :
        R)
      (0 : R)

Tactic:
obtain ⟨r, hr⟩ := exists_eval_ne_zero_of_totalDegree_le_card_aux hF hF₀ hnR

Premises used: _private.0.MvPolynomial.IsHomogeneous.exists_eval_ne_zero_of_totalDegree_le_card_aux
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hnR : (↑n : Cardinal.{u_5}) ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF_1 : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F) n
h :
  Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
hF₀ : F ≠ 0
hF : F.IsHomogeneous n
r : Fin k → R
hr : Ne (α := R) ((eval r : (a : MvPolynomial (Fin k) R) → R) F : R) (0 : R)
obtain :
  ∀ (r : σ → R) (hr : Ne (α := R) ((eval (r ∘ f) : (a : MvPolynomial (Fin k) R) → R) F : R) (0 : R)),
    ∃ (r : σ → R),
      Ne.{u_5 + 1} (α := R)
        ((eval r : (a : MvPolynomial σ R) → R)
            ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R) :
          R)
        (0 : R)
⊢ ∃ (r : σ → R),
    Ne.{u_5 + 1} (α := R)
      ((eval r : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R) :
        R)
      (0 : R)

Tactic:
obtain ⟨r, rfl⟩ := (Function.factorsThrough_iff _).mp <| (hf.factorsThrough r)

Premises used: Iff.mp, Function.factorsThrough_iff, rfl, Function.Injective.factorsThrough
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hnR : (↑n : Cardinal.{u_5}) ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF_1 : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F) n
h :
  Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
hF₀ : F ≠ 0
hF : F.IsHomogeneous n
r : σ → R
hr : Ne (α := R) ((eval (r ∘ f) : (a : MvPolynomial (Fin k) R) → R) F : R) (0 : R)
h₁ :
  Ne.{u_5 + 1} (α := R)
    ((eval r : (a : MvPolynomial σ R) → R)
        ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R) :
      R)
    (0 : R)
⊢ ∃ (r : σ → R),
    Ne.{u_5 + 1} (α := R)
      ((eval r : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R) :
        R)
      (0 : R)

Tactic:
use r
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hnR : (↑n : Cardinal.{u_5}) ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF_1 : IsHomogeneous.{u_6, u_5} (σ := σ) (R := R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F) n
h :
  Ne (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
hF₀ : F ≠ 0
hF : F.IsHomogeneous n
r : σ → R
hr : Ne (α := R) ((eval (r ∘ f) : (a : MvPolynomial (Fin k) R) → R) F : R) (0 : R)
h₁ h₂ h₃ h₄ : Ne (α := R) ((eval (r ∘ f) : (a : MvPolynomial (Fin k) R) → R) F : R) (0 : R)
⊢ Ne.{u_5 + 1} (α := R)
    ((eval r : (a : MvPolynomial σ R) → R)
        ((rename f : (a : MvPolynomial (Fin k) R) → MvPolynomial σ R) F : MvPolynomial σ R) :
      R)
    (0 : R)

Tactic:
rwa [eval_rename]

Premises used: MvPolynomial.eval_rename
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h :
  ∀ (r : σ → R),
    Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) ((eval r : (a : MvPolynomial σ R) → R) G : R)
hnR : (↑n : Cardinal.{u_5}) ≤ #R
rw : F - G = 0
⊢ F = G

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h :
  ∀ (r : σ → R),
    Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) ((eval r : (a : MvPolynomial σ R) → R) G : R)
hnR : (↑n : Cardinal.{u_5}) ≤ #R
apply : ∀ (r : σ → R), Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) (F - G) : R) (0 : R)
⊢ F - G = 0

Tactic:
apply eq_zero_of_forall_eval_eq_zero_of_le_card (hF.sub hG) _ hnR

Premises used: MvPolynomial.IsHomogeneous.sub, MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h :
  ∀ (r : σ → R),
    Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) ((eval r : (a : MvPolynomial σ R) → R) G : R)
hnR : (↑n : Cardinal.{u_5}) ≤ #R
⊢ ∀ (r : σ → R), Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) (F - G) : R) (0 : R)

Tactic:
simpa [sub_eq_zero] using h

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) (0 : R)
apply : (↑n : Cardinal.{u_5}) ≤ #R
⊢ F = 0

Tactic:
apply eq_zero_of_forall_eval_eq_zero_of_le_card hF h

Premises used: MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) (0 : R)
⊢ (↑n : Cardinal.{u_5}) ≤ #R

Tactic:
Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Premises used: Cardinal.infinite_iff, Iff.mp, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) (0 : R)
⊢ (↑n : Cardinal.{u_5}) ≤ #R

Tactic:
exact Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Premises used: Cardinal.infinite_iff, Iff.mp, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h :
  ∀ (r : σ → R),
    Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) ((eval r : (a : MvPolynomial σ R) → R) G : R)
apply : (↑n : Cardinal.{u_5}) ≤ #R
⊢ F = G

Tactic:
apply funext_of_le_card hF hG h

Premises used: MvPolynomial.IsHomogeneous.funext_of_le_card
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h :
  ∀ (r : σ → R),
    Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) ((eval r : (a : MvPolynomial σ R) → R) G : R)
⊢ (↑n : Cardinal.{u_5}) ≤ #R

Tactic:
Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Premises used: Cardinal.infinite_iff, Iff.mp, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h :
  ∀ (r : σ → R),
    Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) ((eval r : (a : MvPolynomial σ R) → R) G : R)
⊢ (↑n : Cardinal.{u_5}) ≤ #R

Tactic:
exact Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Premises used: Cardinal.infinite_iff, Iff.mp, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n)
    ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)

Tactic:
weightedHomogeneousComponent_mem _ φ n

Premises used: Set.Mem, setOf, MvPolynomial.weightedHomogeneousComponent_mem, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
rw :
  coeff d ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    if (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n then coeff d φ else 0
⊢ coeff d ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    if (degree : (a : σ →₀ ℕ) → ℕ) d = n then coeff d φ else 0

Tactic:
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 : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((weightedHomogeneousComponent 1 n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    if (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n then coeff d φ else 0

Tactic:
coeff_weightedHomogeneousComponent n φ d

Premises used: MvPolynomial.coeff_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    if (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n then coeff d φ else 0

Tactic:
convert! coeff_weightedHomogeneousComponent n φ d

Premises used: MvPolynomial.coeff_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
simp_rw :
  Eq (α := MvPolynomial σ R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (∑ x ∈ φ.support with (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) x = n,
        (monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) :
      MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (∑ d ∈ φ.support with (degree : (a : σ →₀ ℕ) → ℕ) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) :
      MvPolynomial σ R)

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 : ℕ
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent 1 n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (∑ d ∈ φ.support with (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) :
      MvPolynomial σ R)

Tactic:
weightedHomogeneousComponent_apply n φ

Premises used: MvPolynomial.weightedHomogeneousComponent_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (∑ x ∈ φ.support with (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) x = n,
        (monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) :
      MvPolynomial σ R)

Tactic:
convert! weightedHomogeneousComponent_apply n φ

Premises used: MvPolynomial.weightedHomogeneousComponent_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n

Tactic:
weightedHomogeneousComponent_isWeightedHomogeneous n φ

Premises used: MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R) ((homogeneousComponent 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ) : MvPolynomial σ R)

Tactic:
weightedHomogeneousComponent_zero φ (fun _ => Nat.succ_ne_zero Nat.zero)

Premises used: Set.Mem, MvPolynomial.weightedHomogeneousComponent_zero, setOf, Nat.succ_ne_zero, Nat.zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
r : R
⊢ (homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)

Tactic:
weightedHomogeneousComponent_C_mul φ n r

Premises used: MvPolynomial.weightedHomogeneousComponent_C_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ ∀ d ∈ φ.support, (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ n

Tactic:
simp_rw [degree_eq_weight_one] at h

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ Eq (α := MvPolynomial σ R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
weightedHomogeneousComponent_eq_zero' n φ h

Premises used: MvPolynomial.weightedHomogeneousComponent_eq_zero'
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ Eq (α := MvPolynomial σ R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
exact weightedHomogeneousComponent_eq_zero' n φ h

Premises used: MvPolynomial.weightedHomogeneousComponent_eq_zero'
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
h₁ : ∀ d ∈ φ.support, (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ Eq (α := MvPolynomial σ R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
apply homogeneousComponent_eq_zero'

Premises used: MvPolynomial.homogeneousComponent_eq_zero'
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ ∀ b ∈ φ.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) < n

Tactic:
rw [totalDegree, Finset.sup_lt_iff (lt_of_le_of_lt (Nat.zero_le _) h)] at h

Premises used: Nat.zero_le, lt_of_le_of_lt, Finset.sup_lt_iff, MvPolynomial.totalDegree
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) < n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n

Tactic:
ne_of_lt (h d hd)

Premises used: ne_of_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) < n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n

Tactic:
exact ne_of_lt (h d hd)

Premises used: ne_of_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
a :
  ∀ (d : σ →₀ ℕ),
    coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
      coeff d φ
⊢ ∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ

Tactic:
ext1 d
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
this : φ.totalDegree < d.support.sum (⇑d : (a : σ) → ℕ) → 0 = coeff d φ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    coeff d φ

Tactic:
simpa [coeff_sum, coeff_homogeneousComponent]

Premises used: MvPolynomial.coeff_homogeneousComponent, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
a : φ.totalDegree < d.support.sum (⇑d : (a : σ) → ℕ) → 0 = coeff d φ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    coeff d φ

Tactic:
suffices φ.totalDegree < d.support.sum d → 0 = coeff d φ by
    simpa [coeff_sum, coeff_homogeneousComponent]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < d.support.sum (⇑d : (a : σ) → ℕ) → 0 = coeff d φ

Tactic:
fun h => (coeff_eq_zero_of_totalDegree_lt h).symm

Premises used: Eq.symm, MvPolynomial.coeff_eq_zero_of_totalDegree_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < d.support.sum (⇑d : (a : σ) → ℕ) → 0 = coeff d φ

Tactic:
exact fun h => (coeff_eq_zero_of_totalDegree_lt h).symm

Premises used: Eq.symm, MvPolynomial.coeff_eq_zero_of_totalDegree_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
m n : ℕ
p : MvPolynomial σ R
h : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n) p
⊢ (homogeneousComponent m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = if m = n then p else 0

Tactic:
weightedHomogeneousComponent_of_mem h

Premises used: MvPolynomial.weightedHomogeneousComponent_of_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
p : MvPolynomial σ R
rw :
  support.{u_3, u_1} (R := R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    {c ∈ p.support | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) c = n}
⊢ support.{u_3, u_1} (R := R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    {c ∈ p.support | (degree : (a : σ →₀ ℕ) → ℕ) c = n}

Tactic:
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 : ℕ
p : MvPolynomial σ R
⊢ support.{u_3, u_1} (R := R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    {c ∈ p.support | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) c = n}

Tactic:
support_weightedHomogeneousComponent n p

Premises used: MvPolynomial.support_weightedHomogeneousComponent