-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem rename_rename (f : σ → τ) (g : τ → α) (p : MvPolynomial σ R) :
    rename g (rename f p) = rename (g ∘ f) p :=
  show rename g (eval₂ C (X ∘ f) p) = _ by
    simp only [rename, aeval_eq_eval₂Hom]
    -- Porting note: the Lean 3 proof of this was very fragile and included a nonterminal `simp`.
    -- Hopefully this is less prone to breaking
    rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]
    simp only [comp_def, eval₂Hom_X']
    refine eval₂Hom_congr ?_ rfl rfl
    ext1; simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]

Proof state:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) (eval₂ C (X ∘ f) p) =
    (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p

Tactic:
rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]

Result:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)).comp C)
      (⇑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) ∘ X ∘ f) p =
    (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p

Proof state:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ (rename g) (eval₂ C (X ∘ f) p) = (rename (g ∘ f)) p

Tactic:
simp only [rename, aeval_eq_eval₂Hom]

Result:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) (eval₂ C (X ∘ f) p) =
    (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p

Proof state:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)).comp C)
      (⇑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) ∘ X ∘ f) p =
    (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p

Tactic:
simp only [comp_def, eval₂Hom_X']

Result:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C) (fun x => X (g (f x))) p =
    (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g (f x))) p

Proof state:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C = algebraMap R (MvPolynomial α R)

Tactic:
ext1

Result:
case a
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
x✝ : R
⊢ ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C) x✝ = (algebraMap R (MvPolynomial α R)) x✝

Proof state:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C) (fun x => X (g (f x))) p =
    (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g (f x))) p

Tactic:
refine eval₂Hom_congr ?_ rfl rfl

Result:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C = algebraMap R (MvPolynomial α R)

Proof state:
case a
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
x✝ : R
⊢ ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C) x✝ = (algebraMap R (MvPolynomial α R)) x✝

Tactic:
simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]

Result:
no goals