awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
t s : Fin n →₀ ℕ
⊢ esymmAlgHomMonomial σ (t + s) r =
    HMul.hMul (α := MvPolynomial σ R) (esymmAlgHomMonomial σ t r) (esymmAlgHomMonomial σ s 1)
have simp_rw : (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
        ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r)) :
    MvPolynomial σ R) =
  HMul.hMul (α := MvPolynomial σ R)
    (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          ((monomial t : (a : R) → MvPolynomial (Fin n) R) r)) :
      MvPolynomial σ R)
    (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1)) :
      MvPolynomial σ R)
Tactic: simp_rw [esymmAlgHomMonomial, esymmAlgHom_apply, ← map_mul, monomial_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
t s : Fin n →₀ ℕ
simp_rw :
  (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r)) :
      MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R)
      (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R)
      (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1)) :
        MvPolynomial σ R)
⊢ esymmAlgHomMonomial σ (t + s) r =
    HMul.hMul (α := MvPolynomial σ R) (esymmAlgHomMonomial σ t r) (esymmAlgHomMonomial σ s 1)
have simp_rw₁ : (aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
    ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((monomial t : (a : R) → MvPolynomial (Fin n) R) r) :
      MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1) :
      MvPolynomial σ R)
Tactic: simp_rw [esymmAlgHomMonomial, esymmAlgHom_apply, ← map_mul, monomial_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
t s : Fin n →₀ ℕ
simp_rw :
  (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r)) :
      MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R)
      (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R)
      (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1)) :
        MvPolynomial σ R)
simp_rw₁ :
  (aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
          ((monomial t : (a : R) → MvPolynomial (Fin n) R) r) :
        MvPolynomial σ R)
      ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
          ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1) :
        MvPolynomial σ R)
⊢ esymmAlgHomMonomial σ (t + s) r =
    HMul.hMul (α := MvPolynomial σ R) (esymmAlgHomMonomial σ t r) (esymmAlgHomMonomial σ s 1)
have simp_rw₂ : Eq (α := MvPolynomial σ R)
  ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) :
    MvPolynomial σ R)
  ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial (Fin n) R) (β := MvPolynomial (Fin n) R)
        ((monomial t : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)
        ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1 : MvPolynomial (Fin n) R)) :
    MvPolynomial σ R)
Tactic: simp_rw [esymmAlgHomMonomial, esymmAlgHom_apply, ← map_mul, monomial_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
t s : Fin n →₀ ℕ
simp_rw :
  (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r)) :
      MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R)
      (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R)
      (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1)) :
        MvPolynomial σ R)
simp_rw₁ :
  (aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
          ((monomial t : (a : R) → MvPolynomial (Fin n) R) r) :
        MvPolynomial σ R)
      ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
          ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1) :
        MvPolynomial σ R)
simp_rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) :
      MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        (HMul.hMul (α := MvPolynomial (Fin n) R) (β := MvPolynomial (Fin n) R)
          ((monomial t : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)
          ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1 : MvPolynomial (Fin n) R)) :
      MvPolynomial σ R)
⊢ esymmAlgHomMonomial σ (t + s) r =
    HMul.hMul (α := MvPolynomial σ R) (esymmAlgHomMonomial σ t r) (esymmAlgHomMonomial σ s 1)
have simp_rw₃ : Eq (α := MvPolynomial σ R)
  ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) :
    MvPolynomial σ R)
  ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) (r * 1)) :
    MvPolynomial σ R)
Tactic: simp_rw [esymmAlgHomMonomial, esymmAlgHom_apply, ← map_mul, monomial_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
⊢ Eq (α := MvPolynomial σ R) (esymmAlgHomMonomial σ (n := n) 0 r) ((C : (a : R) → MvPolynomial σ R) r)
have rw : Eq (α := MvPolynomial σ R)
  ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          ((monomial 0 : (a : R) → MvPolynomial (Fin n) R) r)) :
      MvPolynomial σ R) :
    MvPolynomial σ R)
  ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
rw :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial 0 : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) (esymmAlgHomMonomial σ (n := n) 0 r) ((C : (a : R) → MvPolynomial σ R) r)
have rw₁ : Eq (α := MvPolynomial σ R)
  ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          ((C : (a : R) → MvPolynomial (Fin n) R) r)) :
      MvPolynomial σ R) :
    MvPolynomial σ R)
  ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
rw :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial 0 : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((C : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) (esymmAlgHomMonomial σ (n := n) 0 r) ((C : (a : R) → MvPolynomial σ R) r)
have rw₂ : Eq (α := MvPolynomial σ R)
  ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial (Fin n) R) r) :
    MvPolynomial σ R)
  ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
rw :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial 0 : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((C : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial (Fin n) R) r) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) (esymmAlgHomMonomial σ (n := n) 0 r) ((C : (a : R) → MvPolynomial σ R) r)
have rw₃ : Eq (α := MvPolynomial σ R) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
  ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
rw :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial 0 : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((C : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial (Fin n) R) r) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₃ :
  Eq (α := MvPolynomial σ R) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) (esymmAlgHomMonomial σ (n := n) 0 r) ((C : (a : R) → MvPolynomial σ R) r)
have rw₄ : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
  ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
⊢ Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
        Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
        Lex (Fin m →₀ ℕ)) ∧
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymm (Fin m) R (i + 1))
have refine_3 : ∀
  (this :
    Eq (α := Lex (Fin m →₀ ℕ))
        (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
        (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1)) ∧
      Eq.{u_3 + 1} (α := R)
        (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
        (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))),
  Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
        Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
        Lex (Fin m →₀ ℕ)) ∧
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymm (Fin m) R (i + 1))
Tactic: have := supDegree_leadingCoeff_sum_eq (D := toLex) (s := univ.powersetCard (i + 1))
    (i := Iic (⟨i, him⟩ : Fin m)) ?_ (f := fun s ↦ monomial (∑ j ∈ s, fun₀ | j => 1) (1 : R)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
refine_3 :
  ∀
    (this :
      Eq (α := Lex (Fin m →₀ ℕ))
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1)) ∧
        Eq.{u_3 + 1} (α := R)
          (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
          (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))),
    Eq (α := Lex (Fin m →₀ ℕ))
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
          Lex (Fin m →₀ ℕ))
        ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
          Lex (Fin m →₀ ℕ)) ∧
      Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (esymm (Fin m) R (i + 1))
⊢ Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
        Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
        Lex (Fin m →₀ ℕ)) ∧
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymm (Fin m) R (i + 1))
have refine_1 : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) (Iic (⟨i, him⟩ : Fin m))
Tactic: have := supDegree_leadingCoeff_sum_eq (D := toLex) (s := univ.powersetCard (i + 1))
    (i := Iic (⟨i, him⟩ : Fin m)) ?_ (f := fun s ↦ monomial (∑ j ∈ s, fun₀ | j => 1) (1 : R)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
refine_3 :
  ∀
    (this :
      Eq (α := Lex (Fin m →₀ ℕ))
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1)) ∧
        Eq.{u_3 + 1} (α := R)
          (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
          (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))),
    Eq (α := Lex (Fin m →₀ ℕ))
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
          Lex (Fin m →₀ ℕ))
        ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
          Lex (Fin m →₀ ℕ)) ∧
      Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (esymm (Fin m) R (i + 1))
refine_1 : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) (Iic (⟨i, him⟩ : Fin m))
⊢ Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
        Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
        Lex (Fin m →₀ ℕ)) ∧
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymm (Fin m) R (i + 1))
have refine_2 : ∀ (j : Finset (Fin m)),
  Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) j →
    j ≠ Iic ⟨i, him⟩ →
      LT.lt (α := Lex (Fin m →₀ ℕ))
        (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          ((fun (s : Finset (Fin m)) ↦
              ((monomial (∑ j ∈ s, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1 : MvPolynomial (Fin m) R))
            j))
        (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          ((fun (s : Finset (Fin m)) ↦
              ((monomial (∑ j ∈ s, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1 : MvPolynomial (Fin m) R))
            (Iic ⟨i, him⟩)))
Tactic: have := supDegree_leadingCoeff_sum_eq (D := toLex) (s := univ.powersetCard (i + 1))
    (i := Iic (⟨i, him⟩ : Fin m)) ?_ (f := fun s ↦ monomial (∑ j ∈ s, fun₀ | j => 1) (1 : R)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
this :
  Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
      (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1)) ∧
    Eq.{u_3 + 1} (α := R)
      (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
      (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
⊢ Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
        Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
        Lex (Fin m →₀ ℕ)) ∧
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymm (Fin m) R (i + 1))
have refine_3 : ∀
  (this :
    Eq (α := Lex (Fin m →₀ ℕ))
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)))
        (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1)) ∧
      leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (esymm (Fin m) R (i + 1)) =
        leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1)),
  Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
        Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
        Lex (Fin m →₀ ℕ)) ∧
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymm (Fin m) R (i + 1))
Tactic: rwa [← esymm_eq_sum_monomial, ← Finsupp.indicator_eq_sum_single, ← single_eq_monomial,
      supDegree_single_ne_zero _ one_ne_zero, leadingCoeff_single toLex.injective] at this
Cleared hypotheses: this