-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
e : σ ≃ τ
i : Fin n
hf :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i))) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
hf₁ :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          ((aeval fun (i : Fin n) ↦
                Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                  Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
                  (esymm σ R ((↑i : ℕ) + 1)) ⋯ :
              (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            (X i))) :
      MvPolynomial τ R)
    (↑((aeval fun (i : Fin n) ↦
              Subtype.mk (p := fun (x : MvPolynomial τ R) ↦
                Membership.mem (γ := Subalgebra R (MvPolynomial τ R)) (symmetricSubalgebra τ R) x)
                (esymm τ R ((↑i : ℕ) + 1)) ⋯ :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
hf₂ :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
            (esymm σ R ((↑i : ℕ) + 1)) ⋯)) :
      MvPolynomial τ R)
    (esymm τ R ((↑i : ℕ) + 1))
hf₃ :
  Eq (α := MvPolynomial τ R)
    (↑((renameSymmetricSubalgebra e : (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
            (esymm σ R ((↑i : ℕ) + 1)) ⋯)) :
      MvPolynomial τ R)
    (esymm τ R ((↑i : ℕ) + 1))
hf₄ :
  Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (esymm σ R ((↑i : ℕ) + 1)) :
      MvPolynomial τ R)
    (esymm τ R ((↑i : ℕ) + 1) : MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    (↑((AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
              (esymmAlgHom σ R n) :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)

Tactic:
simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.coe_algHom,
    renameSymmetricSubalgebra_apply_coe, rename_esymm]

Premises used: MvPolynomial.aeval_X, AlgHom.comp_apply, MvPolynomial.rename_esymm, MvPolynomial.esymmAlgHom, AlgEquiv.coe_algHom, MvPolynomial.renameSymmetricSubalgebra_apply_coe