awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
i : ℕ
hi :
  Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
hin_1 : i ≤ n
hFn :
  Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) :
      R)
    (0 : R)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ₀ : φ ≠ 0
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have hφR : (↑φ.natDegree : Cardinal.{u_5}) < #R
Tactic: have hφR : φ.natDegree < #R := by
      refine lt_of_lt_of_le ?_ hnR
      norm_cast
      refine lt_of_le_of_lt natDegree_map_le ?_
      suffices (finSuccEquiv _ _ F).natDegree ≠ n by lia
      rintro rfl
      refine leadingCoeff_ne_zero.mpr ?_ hFn
      simpa using (finSuccEquiv R N).injective.ne hF₀
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
i : ℕ
hi :
  Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
hin_1 : i ≤ n
hFn :
  Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) :
      R)
    (0 : R)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ₀ : φ ≠ 0
hφR : (↑φ.natDegree : Cardinal.{u_5}) < #R
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have succ : ∀ (r₀ : R) (hr₀ : Polynomial.eval r₀ φ ≠ 0),
  ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
Tactic: obtain ⟨r₀, hr₀⟩ : ∃ r₀, Polynomial.eval r₀ φ ≠ 0 :=
      φ.exists_eval_ne_zero_of_natDegree_lt_card hφ₀ hφR
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
i : ℕ
hi :
  Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
hin_1 : i ≤ n
hFn :
  Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) :
      R)
    (0 : R)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ₀ : φ ≠ 0
hφR : (↑φ.natDegree : Cardinal.{u_5}) < #R
r₀ : R
hr₀ : Polynomial.eval r₀ φ ≠ 0
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have h : Ne (α := R) ((eval (Fin.cons (α := fun (a : Fin (N + 1)) ↦ R) r₀ r) : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R)
  (0 : R)
Tactic: use Fin.cons r₀ r
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain 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)
hnR : (↑n : Cardinal.{u_5}) ≤ #R
⊢ F = 0
have contrapose! : ∀ (h : F ≠ 0), ∃ (r : σ → R), Ne.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) (0 : R)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ ∃ (r : σ → R), Ne.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) (0 : R)
have 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)
Tactic: obtain ⟨k, f, hf, F, rfl⟩ := exists_fin_rename F
Cleared hypotheses: F, hF, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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)
⊢ ∃ (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)
have hF₀ : F ≠ 0
Tactic: have hF₀ : F ≠ 0 := by rintro rfl; simp at h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
have 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
Tactic: rwa [rename_isHomogeneous_iff hf] at hF
Cleared hypotheses: hF, h, hF₀
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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
⊢ ∃ (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)
have hF₁ : F.IsHomogeneous n
Tactic: have hF : F.IsHomogeneous n := by rwa [rename_isHomogeneous_iff hf] at hF
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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),
    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)
have 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)
Tactic: obtain ⟨r, hr⟩ := exists_eval_ne_zero_of_totalDegree_le_card_aux hF hF₀ hnR
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨r, rfl⟩ := (Function.factorsThrough_iff _).mp <| (hf.factorsThrough r)
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use r
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ F = G
have rw : F - G = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ F - G = 0
have apply : ∀ (r : σ → R), Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) (F - G) : R) (0 : R)
Tactic: apply eq_zero_of_forall_eval_eq_zero_of_le_card (hF.sub hG) _ hnR
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
⊢ F = 0
have apply : (↑n : Cardinal.{u_5}) ≤ #R
Tactic: apply eq_zero_of_forall_eval_eq_zero_of_le_card hF h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
⊢ F = G
have apply : (↑n : Cardinal.{u_5}) ≤ #R
Tactic: apply funext_of_le_card hF hG h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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 (degree : (a : σ →₀ ℕ) → ℕ) d = n then coeff d φ else 0
have rw : coeff d ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
  if (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n then coeff d φ else 0
Tactic: rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
    (∑ d ∈ φ.support with (degree : (a : σ →₀ ℕ) → ℕ) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) :
      MvPolynomial σ R)
have 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)
Tactic: simp_rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ Eq (α := MvPolynomial σ R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have h₁ : ∀ d ∈ φ.support, (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ n
Tactic: simp_rw [degree_eq_weight_one] at 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
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ Eq (α := MvPolynomial σ R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have h₁ : ∀ d ∈ φ.support, (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n
Tactic: apply homogeneousComponent_eq_zero'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ ∀ d ∈ φ.support, (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n
have h₁ : ∀ 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
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
⊢ ∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
have a : ∀ (d : σ →₀ ℕ),
  coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    coeff d φ
Tactic: ext1 d
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    coeff d φ
have a : φ.totalDegree < d.support.sum (⇑d : (a : σ) → ℕ) → 0 = coeff d φ
Tactic: suffices φ.totalDegree < d.support.sum d → 0 = coeff d φ by
    simpa [coeff_sum, coeff_homogeneousComponent]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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 | (degree : (a : σ →₀ ℕ) → ℕ) c = n}
have 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}
Tactic: rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R → DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
    (@DirectSum.Decomposition.decompose' _ _ _ instDecidableEqNat _ _ _ _ _) fun (φ : MvPolynomial σ R) ↦
    ((DirectSum.mk (fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑degree : (a : σ →₀ ℕ) → ℕ) φ.support) :
          ((i : (↑(↑(Finset.image (⇑degree : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
              ↥(homogeneousSubmodule σ R (↑i : ℕ))) →+
            DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i)) :
        (a :
            (i : (↑(↑(Finset.image (⇑degree : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
              ↥(homogeneousSubmodule σ R (↑i : ℕ))) →
          DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
      fun (m : (↑(↑(Finset.image (⇑degree : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) ↦
      Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R (↑m : ℕ)) x)
        ((homogeneousComponent (↑m : ℕ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯
have rw : Eq (α := MvPolynomial σ R → DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
  (@DirectSum.Decomposition.decompose' _ _ _ instDecidableEqNat _ _ _ _ _) fun (φ : MvPolynomial σ R) ↦
  ((DirectSum.mk (fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
          (Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) :
        ((i : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
            ↥(homogeneousSubmodule σ R (↑i : ℕ))) →+
          DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i)) :
      (a :
          (i : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
            ↥(homogeneousSubmodule σ R (↑i : ℕ))) →
        DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
    fun (m : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) ↦
    Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R (↑m : ℕ)) x)
      ((homogeneousComponent (↑m : ℕ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) sorry
Tactic: rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
x : ι → R
n : ℕ
⊢ HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R n)
have rw : HPow.hPow (α := Ideal R) (span (Set.range x)) n =
  Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x))
    (HPow.hPow (α := Submodule R (MvPolynomial ι R)) (MvPolynomial.homogeneousSubmodule ι R 1) n)
Tactic: rw [← MvPolynomial.homogeneousSubmodule_one_pow, Submodule.map_pow,
    Ideal.span_eq_map_homogeneousSubmodule]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
x : ι → R
n : ℕ
rw :
  HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x))
      (HPow.hPow (α := Submodule R (MvPolynomial ι R)) (MvPolynomial.homogeneousSubmodule ι R 1) n)
⊢ HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R n)
have rw₁ : HPow.hPow (α := Ideal R) (span (Set.range x)) n =
  HPow.hPow (α := Submodule R R)
    (Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R 1)) n
Tactic: rw [← MvPolynomial.homogeneousSubmodule_one_pow, Submodule.map_pow,
    Ideal.span_eq_map_homogeneousSubmodule]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
x : ι → R
n : ℕ
rw :
  HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x))
      (HPow.hPow (α := Submodule R (MvPolynomial ι R)) (MvPolynomial.homogeneousSubmodule ι R 1) n)
rw₁ :
  HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    HPow.hPow (α := Submodule R R)
      (Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R 1)) n
⊢ HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R n)
have rw₂ : HPow.hPow (α := Ideal R)
    (Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R 1)) n =
  HPow.hPow (α := Submodule R R)
    (Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R 1)) n
Tactic: rw [← MvPolynomial.homogeneousSubmodule_one_pow, Submodule.map_pow,
    Ideal.span_eq_map_homogeneousSubmodule]