R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
⊢ Prime p ↔ Prime (↑(rename Subtype.val) p)
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
⊢ Prime (↑(rename Subtype.val) p) ↔ Prime p
symm
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
⊢ Prime p ↔ Prime (↑(rename Subtype.val) p)
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
⊢ Prime p ↔ Prime (↑(rename Subtype.val) p)
let eqv :=
  (sumAlgEquiv R (↥(sᶜ)) s).symm.trans
    (renameEquiv R <| (Equiv.sumComm (↥(sᶜ)) s).trans <| Equiv.Set.sumCompl s)
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime (↑C p) ↔ Prime (↑(rename Subtype.val) p)
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime p ↔ Prime (↑(rename Subtype.val) p)
rw [← @prime_C_iff (MvPolynomial s R) (↥(sᶜ)) instCommRingMvPolynomialToCommSemiring p]
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime (↑?e (↑C p)) ↔ Prime (↑(rename Subtype.val) p)

case e
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃* MvPolynomial σ R

R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ CommMonoidWithZero (MvPolynomial σ R)
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime (↑C p) ↔ Prime (↑(rename Subtype.val) p)
rw [@MulEquiv.prime_iff (MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R)) (MvPolynomial σ R) (_) (_)]
case e
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃* MvPolynomial σ R

R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ CommMonoidWithZero (MvPolynomial σ R)

R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime (↑?e (↑C p)) ↔ Prime (↑(rename Subtype.val) p)
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime (↑?e (↑C p)) ↔ Prime (↑(rename Subtype.val) p)

case e
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃* MvPolynomial σ R

R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ CommMonoidWithZero (MvPolynomial σ R)
rotate_left
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime (↑(AlgEquiv.toMulEquiv eqv) (↑C p)) ↔ Prime (↑(rename Subtype.val) p)
case e
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃* MvPolynomial σ R

R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ CommMonoidWithZero (MvPolynomial σ R)

R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime (↑?e (↑C p)) ↔ Prime (↑(rename Subtype.val) p)
exact eqv.toMulEquiv
case h.e'_2.h.e'_3
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ ↑(rename Subtype.val) p = ↑(AlgEquiv.toMulEquiv eqv) (↑C p)
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ Prime (↑(AlgEquiv.toMulEquiv eqv) (↑C p)) ↔ Prime (↑(rename Subtype.val) p)
convert Iff.rfl
no goals
case h.e'_2.h.e'_3
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
this : ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
⊢ ↑(rename Subtype.val) p = ↑(AlgEquiv.toMulEquiv eqv) (↑C p)
apply RingHom.congr_fun this p
case hC
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ∀ (r : R), ↑↑(rename Subtype.val) (↑C r) = ↑(RingHom.comp (↑↑eqv) C) (↑C r)

case hX
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ∀ (i : ↑s), ↑↑(rename Subtype.val) (X i) = ↑(RingHom.comp (↑↑eqv) C) (X i)
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ↑(rename Subtype.val) = RingHom.comp (↑↑eqv) C
apply ringHom_ext
case hC
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
r✝ : R
⊢ ↑↑(rename Subtype.val) (↑C r✝) = ↑(RingHom.comp (↑↑eqv) C) (↑C r✝)
case hC
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ∀ (r : R), ↑↑(rename Subtype.val) (↑C r) = ↑(RingHom.comp (↑↑eqv) C) (↑C r)
intro
case hC
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
r✝ : R
⊢ ↑(rename Subtype.val) (↑C r✝) =
    ↑(rename (↑(Equiv.Set.sumCompl s) ∘ Sum.swap)) (↑(AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s)) (↑C (↑C r✝)))
case hC
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
r✝ : R
⊢ ↑↑(rename Subtype.val) (↑C r✝) = ↑(RingHom.comp (↑↑eqv) C) (↑C r✝)
dsimp
no goals
case hC
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
r✝ : R
⊢ ↑(rename Subtype.val) (↑C r✝) =
    ↑(rename (↑(Equiv.Set.sumCompl s) ∘ Sum.swap)) (↑(AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s)) (↑C (↑C r✝)))
erw [iterToSum_C_C, rename_C, rename_C]
case hX
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
i✝ : ↑s
⊢ ↑↑(rename Subtype.val) (X i✝) = ↑(RingHom.comp (↑↑eqv) C) (X i✝)
case hX
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
⊢ ∀ (i : ↑s), ↑↑(rename Subtype.val) (X i) = ↑(RingHom.comp (↑↑eqv) C) (X i)
intro
case hX
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
i✝ : ↑s
⊢ ↑(rename Subtype.val) (X i✝) =
    ↑(rename (↑(Equiv.Set.sumCompl s) ∘ Sum.swap)) (↑(AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s)) (↑C (X i✝)))
case hX
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
i✝ : ↑s
⊢ ↑↑(rename Subtype.val) (X i✝) = ↑(RingHom.comp (↑↑eqv) C) (X i✝)
dsimp
case hX
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
i✝ : ↑s
⊢ X ↑i✝ = X ((↑(Equiv.Set.sumCompl s) ∘ Sum.swap) (Sum.inr i✝))
case hX
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
i✝ : ↑s
⊢ ↑(rename Subtype.val) (X i✝) =
    ↑(rename (↑(Equiv.Set.sumCompl s) ∘ Sum.swap)) (↑(AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s)) (↑C (X i✝)))
erw [iterToSum_C_X, rename_X, rename_X]
no goals
case hX
R : Type u
S : Type ?u.606815
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑(sᶜ)) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R ↑(sᶜ) ↑s))
    (renameEquiv R ((Equiv.sumComm ↑(sᶜ) ↑s).trans (Equiv.Set.sumCompl s)))
i✝ : ↑s
⊢ X ↑i✝ = X ((↑(Equiv.Set.sumCompl s) ∘ Sum.swap) (Sum.inr i✝))
rfl