-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  Eq (α := Lex (Fin m →₀ ℕ))
    (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R) (coeff t p))) :
        MvPolynomial (Fin m) R))
    (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
            ((monomial s : (a : R) → MvPolynomial (Fin n) R) (coeff s p))) :
        MvPolynomial (Fin m) R))
refine_2 :
  ∀
    (he :
      Eq (α := Lex (Fin m →₀ ℕ))
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (esymmAlgHomMonomial (Fin m) t (coeff t p)))
        (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
                ((monomial s : (a : R) → MvPolynomial (Fin n) R) (coeff s p))) :
            MvPolynomial (Fin m) R))),
    Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)
refine_2₁ :
  ∀
    (he :
      Eq (α := Lex (Fin m →₀ ℕ))
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (esymmAlgHomMonomial (Fin m) t (coeff t p)))
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (esymmAlgHomMonomial (Fin m) s (coeff s p)))),
    Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)
refine_2₂ :
  ∀
    (he :
      Eq (α := Fin m →₀ ℕ)
        ((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) t (coeff t p))))
        ((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) s (coeff s p))))),
    Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)
refine_2₃ :
  ∀
    (he :
      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 (coeff t p)))) :
          (a : Fin m) → ℕ)
        (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
              (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
                (esymmAlgHomMonomial (Fin m) s (coeff s p)))) :
          (a : Fin m) → ℕ)),
    Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)
refine_2₄ :
  ∀
    (he :
      Eq (α := (a : Fin m) → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
        ((⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
                (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
                  (esymmAlgHomMonomial (Fin m) s (coeff s p)))) :
            (a : Fin m) → ℕ) :
          (a : Fin m) → ℕ)),
    Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)
refine_2₅ refine_2₆ refine_2₇ refine_2₈ :
  ∀
    (he :
      Eq (α := (a : Fin m) → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
        ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)),
    Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)
⊢ Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)

Tactic:
rwa [← esymmAlgHomMonomial, ← esymmAlgHomMonomial, ← ofLex_inj, DFunLike.ext'_iff,
       supDegree_esymmAlgHomMonomial ht t h, supDegree_esymmAlgHomMonomial hs s h] at he

Premises used: MvPolynomial.esymmAlgHomMonomial, MvPolynomial.supDegree_esymmAlgHomMonomial, DFunLike.ext'_iff, ofLex_inj