-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem prime_rename_iff (s : Set σ) {p : MvPolynomial s R} :
    Prime (rename ((↑) : s → σ) p) ↔ Prime (p : MvPolynomial s R)

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
⊢ (rename Subtype.val).toRingHom = (↑eqv).comp C

Tactic:
apply ringHom_ext

Result:
case hC
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ∀ (r : R), (rename Subtype.val).toRingHom (C r) = ((↑eqv).comp C) (C r)

case hX
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ∀ (i : ↑s), (rename Subtype.val).toRingHom (X i) = ((↑eqv).comp C) (X i)

Proof state:
case hC
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ∀ (r : R), (rename Subtype.val).toRingHom (C r) = ((↑eqv).comp C) (C r)

Tactic:
intro

Result:
case hC
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
r✝ : R
⊢ (rename Subtype.val).toRingHom (C r✝) = ((↑eqv).comp C) (C r✝)

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
⊢ Prime ((rename Subtype.val) p) ↔ Prime p

Tactic:
symm

Result:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Proof state:
case hC
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
r✝ : R
⊢ (rename Subtype.val).toRingHom (C r✝) = ((↑eqv).comp C) (C r✝)

Tactic:
simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_C,
  AlgEquiv.toAlgHom_eq_coe, 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]

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
this : (rename Subtype.val).toRingHom p = ((↑eqv).comp C) p
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgEquiv.toAlgHom_eq_coe,
  AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, Function.comp_apply] at this

Result:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
this : (rename Subtype.val) p = eqv (C p)
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Proof state:
case hX
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
i✝ : ↑s
⊢ (rename Subtype.val).toRingHom (X i✝) = ((↑eqv).comp C) (X i✝)

Tactic:
simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_X,
  AlgEquiv.toAlgHom_eq_coe, 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]

Result:
no goals

Proof state:
case hX
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ∀ (i : ↑s), (rename Subtype.val).toRingHom (X i) = ((↑eqv).comp C) (X i)

Tactic:
intro

Result:
case hX
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
i✝ : ↑s
⊢ (rename Subtype.val).toRingHom (X i✝) = ((↑eqv).comp C) (X i✝)

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Tactic:
let eqv :=
  (sumAlgEquiv R (↥sᶜ) s).symm.trans
    (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s)

Result:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
this : (rename Subtype.val) p = eqv (C p)
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Tactic:
rw [this, MulEquiv.prime_iff, prime_C_iff]

Result:
no goals