-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem constantCoeff_rename {τ : Type*} (f : σ → τ) (φ : MvPolynomial σ R) :
    constantCoeff (rename f φ) = constantCoeff φ

Proof state:
case h_C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
a : R
⊢ constantCoeff ((rename f) (C a)) = constantCoeff (C a)

Tactic:
simp only [constantCoeff_C, rename_C]

Result:
no goals

Proof state:
case h_add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p q : MvPolynomial σ R
hp : constantCoeff ((rename f) p) = constantCoeff p
hq : constantCoeff ((rename f) q) = constantCoeff q
⊢ constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)

Tactic:
simp only [hp, hq, map_add]

Result:
no goals

Proof state:
case h_C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (a : R), constantCoeff ((rename f) (C a)) = constantCoeff (C a)

Tactic:
intro a

Result:
case h_C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
a : R
⊢ constantCoeff ((rename f) (C a)) = constantCoeff (C a)

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ constantCoeff ((rename f) φ) = constantCoeff φ

Tactic:
apply φ.induction_on

Result:
case h_C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (a : R), constantCoeff ((rename f) (C a)) = constantCoeff (C a)

case h_add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    constantCoeff ((rename f) p) = constantCoeff p →
      constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)

case h_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)

Proof state:
case h_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
n : σ
hp : constantCoeff ((rename f) p) = constantCoeff p
⊢ constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)

Tactic:
simp only [hp, rename_X, constantCoeff_X, map_mul]

Result:
no goals

Proof state:
case h_add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    constantCoeff ((rename f) p) = constantCoeff p →
      constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)

Tactic:
intro p q hp hq

Result:
case h_add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p q : MvPolynomial σ R
hp : constantCoeff ((rename f) p) = constantCoeff p
hq : constantCoeff ((rename f) q) = constantCoeff q
⊢ constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)

Proof state:
case h_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)

Tactic:
intro p n hp

Result:
case h_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
n : σ
hp : constantCoeff ((rename f) p) = constantCoeff p
⊢ constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)