-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
hd :
  Eq (α := Lex (Fin n →₀ ℕ))
    (supDegree (A := Fin n →₀ ℕ) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
hne :
  p ≠
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
this :
  LT.lt (α := Lex (Fin n →₀ ℕ))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (p -
        esymmAlgHomMonomial (Fin n) t
          (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
right :
  p -
      esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p) ≠
    0
right₁ :
  ∀
    (ih :
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x)
          (p -
            esymmAlgHomMonomial (Fin n) t
              (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p))
          ⋯)),
    Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
      (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
        Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)

Tactic:
specialize ih _ this _ (Subalgebra.sub_mem _ hp <| isSymmetric_esymmAlgHomMonomial _ _) _ rfl

Premises used: MvPolynomial.isSymmetric_esymmAlgHomMonomial, Subalgebra.sub_mem, rfl