-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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))
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))
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 (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 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 (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 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_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 →₀ ℕ))
            fun₀ | Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1 => 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 →₀ ℕ))
            fun₀ | Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1 => 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_3₃ :
  ∀
    (this :
      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 →₀ ℕ)) ∧
        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 →₀ ℕ))
            fun₀ | Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1 => 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_3₄ refine_3₅ refine_3₆ refine_3₇ :
  ∀
    (this :
      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 →₀ ℕ)) ∧
        leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymm (Fin m) R (i + 1)) =
          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))

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

Premises used: MvPolynomial.single_eq_monomial, AddMonoidAlgebra.leadingCoeff_single, MvPolynomial.esymm_eq_sum_monomial, AddMonoidAlgebra.supDegree_single_ne_zero, Finsupp.indicator_eq_sum_single, Equiv.injective, one_ne_zero, toLex