-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
let :
  Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
let₁ :
  Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
let₂ :
  let eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
    AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
      (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)));
  ∀
    (this :
      AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) =
        (↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C),
    Prime p ↔
      Prime (M := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
            p :
          MvPolynomial σ R)
let₃ :
  let eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
    AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
      (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)));
  ∀
    (this :
      Eq (α := MvPolynomial σ R)
        ((AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) :
              (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
            p :
          MvPolynomial σ R)
        (((↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C :
              (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
            p :
          MvPolynomial σ R)),
    Prime p ↔
      Prime (M := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
            p :
          MvPolynomial σ R)
let₄ :
  let eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
    AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
      (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)));
  ∀
    (this :
      Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R) p :
          MvPolynomial σ R)
        ((eqv : (a : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) → MvPolynomial σ R)
            ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p) :
          MvPolynomial σ R)),
    Prime p ↔
      Prime (M := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
            p :
          MvPolynomial σ R)
⊢ Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R) ↔
    Prime p

Tactic:
classical
    symm
    let eqv :=
      (sumAlgEquiv R (↥sᶜ) s).symm.trans
        (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s)
    have : (rename (↑)).toRingHom = eqv.toAlgHom.toRingHom.comp C := by
      apply ringHom_ext
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_C,
          AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans,
          Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_C,
          renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply]
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_X,
          AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans,
          Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_X,
          renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply, Sum.swap_inr,
          Equiv.Set.sumCompl_apply_inl]
    apply_fun (· p) at this
    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgEquiv.toAlgHom_toRingHom,
      RingHom.coe_comp, Function.comp_apply] at this
    rw [this, MulEquiv.prime_iff, prime_C_iff]

Premises used: AlgEquiv.toAlgHom_toRingHom, RingHom.coe_coe, MulEquiv.prime_iff, MvPolynomial.prime_C_iff, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, Function.comp_apply