awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
i : Fin n
inst_1 : Nontrivial R
him : (↑i : ℕ) < m
j : Fin m
h :
  Eq (α := ℕ) (if hi : j ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m) then 1 else 0 : ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)
h₁ :
  Eq (α := ℕ) (if j ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m) then 1 else 0 : ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)
h₂ :
  Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0 : ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)
h₃ :
  Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0)
    (∑ i_1 : Fin n with (↑j : ℕ) ≤ (↑i_1 : ℕ), (fun₀ | i => 1 : (a : Fin n) → ℕ) i_1)
h₄ : Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0) (∑ x : Fin n with (↑j : ℕ) ≤ (↑x : ℕ), if i = x then 1 else 0)
h₅ :
  Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0)
    (if Membership.mem (γ := Finset (Fin n)) {i : Fin n | (↑j : ℕ) ≤ (↑i : ℕ)} i then 1 else 0)
⊢ Eq (α := ℕ)
    ((Finsupp.indicator (Iic ⟨(↑i : ℕ), him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m)) ↦ 1 :
          (a : Fin m) → ℕ)
        j :
      ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)
have h₆ : Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0) (if (↑j : ℕ) ≤ (↑i : ℕ) then 1 else 0)
Tactic: simp_rw [Finsupp.indicator_apply, dite_eq_ite, mem_Iic, accumulate_apply, Finsupp.single_apply,
    sum_ite_eq, mem_filter_univ, Fin.le_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
him : 0 ≤ m
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R 0)
have zero : Monic.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) 1
Tactic: rw [esymm_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
i : ℕ
him : i + 1 ≤ m
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R (i + 1))
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
i : ℕ
him : i ≤ m
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R i)
have zero : ∀ (him : 0 ≤ m),
  Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R 0)
Tactic: cases i with
  | zero =>
    rw [esymm_zero]
    exact monic_one toLex.injective
  | succ i =>
    nontriviality R
    exact (supDegree_monic_esymm him).2
Cleared hypotheses: i, him
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
i : ℕ
him : i ≤ m
zero :
  ∀ (him : 0 ≤ m),
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R 0)
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R i)
have succ : ∀ (i : ℕ) (him : i + 1 ≤ m),
  Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R (i + 1))
Tactic: cases i with
  | zero =>
    rw [esymm_zero]
    exact monic_one toLex.injective
  | succ i =>
    nontriviality R
    exact (supDegree_monic_esymm him).2
Cleared hypotheses: i, him
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) (n := n) 0 r) =
    r
have zero : leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    ((C : (a : R) → MvPolynomial (Fin m) R) r) =
  r
Tactic: rw [esymmAlgHom_zero, leadingCoeff_toLex_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
zero :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      ((C : (a : R) → MvPolynomial (Fin m) R) r) =
    r
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) (n := n) 0 r) =
    r
have zero₁ : r = r
Tactic: rw [esymmAlgHom_zero, leadingCoeff_toLex_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) f r) =
    r
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r) =
    r
have add_single : Function.Injective (α := Fin m →₀ ℕ) (β := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
Tactic: rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
        ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) f r) =
    r
add_single : Function.Injective (α := Fin m →₀ ℕ) (β := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r) =
    r
have add_single₁ : ∀ (a1 a2 : Fin m →₀ ℕ),
  (toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (a1 + a2) =
    HAdd.hAdd (α := Lex (Fin m →₀ ℕ)) (β := Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) a1 : Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) a2 : Lex (Fin m →₀ ℕ))
Tactic: rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
        ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
t : Fin n →₀ ℕ
hnm : n ≤ m
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) t r) =
    r
have zero : leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymmAlgHomMonomial (Fin m) (n := n) 0 r) =
  r
Tactic: induction t using Finsupp.induction₂ with
  | zero => rw [esymmAlgHom_zero, leadingCoeff_toLex_C]
  | add_single i _ _ _ _ ih =>
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
        ih]
    exacts [toLex.injective, toLex_add]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
t : Fin n →₀ ℕ
hnm : n ≤ m
zero :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) (n := n) 0 r) =
    r
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) t r) =
    r
have add_single : ∀ (i : Fin n) (b : ℕ) (f : Fin n →₀ ℕ),
  i ∉ f.support →
    b ≠ 0 →
      ∀
        (ih :
          leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
              (esymmAlgHomMonomial (Fin m) f r) =
            r),
        leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r) =
          r
Tactic: induction t using Finsupp.induction₂ with
  | zero => rw [esymmAlgHom_zero, leadingCoeff_toLex_C]
  | add_single i _ _ _ _ ih =>
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
        ih]
    exacts [toLex.injective, toLex_add]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
t : Fin n →₀ ℕ
hnm : n ≤ m
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) t r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ))
have inst : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (n := n) 0 r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
have zero : Eq (α := (a : Fin m) → ℕ)
  (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
        (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          ((C : (a : R) → MvPolynomial (Fin m) R) r))) :
    (a : Fin m) → ℕ)
  ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
Tactic: simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
zero :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((C : (a : R) → MvPolynomial (Fin m) R) r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (n := n) 0 r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
have zero₁ : Eq (α := (a : Fin m) → ℕ) (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ) 0) : (a : Fin m) → ℕ)
  ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
Tactic: simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
zero :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((C : (a : R) → MvPolynomial (Fin m) R) r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
zero₁ :
  Eq (α := (a : Fin m) → ℕ) (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ) 0) : (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (n := n) 0 r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
have zero₂ : Eq (α := (a : Fin m) → ℕ) (⇑0 : (a : Fin m) → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
Tactic: simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
zero :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((C : (a : R) → MvPolynomial (Fin m) R) r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
zero₁ :
  Eq (α := (a : Fin m) → ℕ) (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ) 0) : (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
zero₂ :
  Eq (α := (a : Fin m) → ℕ) (⇑0 : (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (n := n) 0 r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
have zero₃ : Eq (α := (a : Fin m) → ℕ) (0 : (a : Fin m) → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) 0 : Fin m → ℕ)
Tactic: simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) f r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑f : (a : Fin n) → ℕ))
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑(f + fun₀ | i => b) : (a : Fin n) → ℕ))
have this : (↑i : ℕ) < m
Tactic: have := i.2.trans_le hnm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) f r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑f : (a : Fin n) → ℕ))
this : (↑i : ℕ) < m
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑(f + fun₀ | i => b) : (a : Fin n) → ℕ))
have add_single : Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
  (esymm (Fin m) R ((↑i : ℕ) + 1))
Tactic: rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add, ofLex_add, Finsupp.coe_add,
        ih, Finsupp.coe_add, map_add, Monic.supDegree_pow rfl toLex_add toLex.injective, ofLex_smul,
        Finsupp.coe_smul, supDegree_esymm this, ← map_nsmul, ← Finsupp.coe_smul,
        Finsupp.smul_single, nsmul_one, Nat.cast_id]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) f r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑f : (a : Fin n) → ℕ))
this : (↑i : ℕ) < m
add_single :
  Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R ((↑i : ℕ) + 1))
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑(f + fun₀ | i => b) : (a : Fin n) → ℕ))
have add_single₁ : Monic (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
  (HPow.hPow (α := MvPolynomial (Fin m) R) (esymm (Fin m) R ((↑i : ℕ) + 1)) b)
Tactic: rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add, ofLex_add, Finsupp.coe_add,
        ih, Finsupp.coe_add, map_add, Monic.supDegree_pow rfl toLex_add toLex.injective, ofLex_smul,
        Finsupp.coe_smul, supDegree_esymm this, ← map_nsmul, ← Finsupp.coe_smul,
        Finsupp.smul_single, nsmul_one, Nat.cast_id]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) f r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑f : (a : Fin n) → ℕ))
this : (↑i : ℕ) < m
add_single :
  Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R ((↑i : ℕ) + 1))
add_single₁ :
  Monic (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (HPow.hPow (α := MvPolynomial (Fin m) R) (esymm (Fin m) R ((↑i : ℕ) + 1)) b)
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑(f + fun₀ | i => b) : (a : Fin n) → ℕ))
have add_single₂ : Ne (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
Tactic: rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add, ofLex_add, Finsupp.coe_add,
        ih, Finsupp.coe_add, map_add, Monic.supDegree_pow rfl toLex_add toLex.injective, ofLex_smul,
        Finsupp.coe_smul, supDegree_esymm this, ← map_nsmul, ← Finsupp.coe_smul,
        Finsupp.smul_single, nsmul_one, Nat.cast_id]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) f r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑f : (a : Fin n) → ℕ))
this : (↑i : ℕ) < m
⊢ Ne (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
have add_single : ¬Eq (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
Tactic: rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) f r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑f : (a : Fin n) → ℕ))
this : (↑i : ℕ) < m
add_single : ¬Eq (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
⊢ Ne (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
have add_single₁ : ¬leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) f r) =
    0
Tactic: rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) f r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑f : (a : Fin n) → ℕ))
this : (↑i : ℕ) < m
add_single : ¬Eq (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
add_single₁ :
  ¬leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (esymmAlgHomMonomial (Fin m) f r) =
      0
⊢ Ne (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
have add_single₂ : ¬r = 0
Tactic: rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]