-- 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))
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))
⊢ 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)) :
          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))
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