-- Mathlib/Algebra/MvPolynomial/Equiv.lean
/-- Consider a multivariate polynomial `φ` whose variables are indexed by `Option σ`,
and suppose that `σ ≃ Fin n`.
Then one may view `φ` as a polynomial over `MvPolynomial (Fin n) R`, by

1. renaming the variables via `Option σ ≃ Fin (n+1)`, and then singling out the `0`-th variable
    via `MvPolynomial.finSuccEquiv`;
2. first viewing it as polynomial over `MvPolynomial σ R` via `MvPolynomial.optionEquivLeft`,
    and then renaming the variables.

This lemma shows that both constructions are the same. -/
lemma finSuccEquiv_rename_finSuccEquiv (e : σ ≃ Fin n) (φ : MvPolynomial (Option σ) R) :
    ((finSuccEquiv R n) ((rename ((Equiv.optionCongr e).trans (_root_.finSuccEquiv n).symm)) φ)) =
      Polynomial.map (rename e).toRingHom (optionEquivLeft R σ φ)

Proof state:
case hX
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ∀ (i : Option σ),
    ((finSuccEquiv R n).toRingEquiv.toRingHom.comp
          (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
        (X i) =
      ((mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X i)

Tactic:
rintro (i|i) <;> simp [finSuccEquiv_apply]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ (finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) =
    Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)

Tactic:
suffices (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ((Equiv.optionCongr e).trans
      (_root_.finSuccEquiv n).symm)).toRingHom =
    (Polynomial.mapRingHom (rename e).toRingHom).comp (optionEquivLeft R σ) by
  exact DFunLike.congr_fun this φ

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom =
    (mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)

Proof state:
case hC
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ∀ (r : R),
    ((finSuccEquiv R n).toRingEquiv.toRingHom.comp
          (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
        (C r) =
      ((mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (C r)

Tactic:
simp [Polynomial.algebraMap_apply, algebraMap_eq, finSuccEquiv_apply]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
this :
  (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom =
    (mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)
⊢ (finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) =
    Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)

Tactic:
exact DFunLike.congr_fun this φ

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom =
    (mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)

Tactic:
apply ringHom_ext

Result:
case hC
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ∀ (r : R),
    ((finSuccEquiv R n).toRingEquiv.toRingHom.comp
          (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
        (C r) =
      ((mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (C r)

case hX
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ∀ (i : Option σ),
    ((finSuccEquiv R n).toRingEquiv.toRingHom.comp
          (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
        (X i) =
      ((mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X i)