case h_C
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (a : R), ↑constantCoeff (↑(rename f) (↑C a)) = ↑constantCoeff (↑C a)

case h_add
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
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_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p →
      ↑constantCoeff (↑(rename f) (p * X n)) = ↑constantCoeff (p * X n)
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ : MvPolynomial σ R
⊢ ↑constantCoeff (↑(rename f) φ) = ↑constantCoeff φ
apply φ.induction_on
case h_C
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ : MvPolynomial σ R
a : R
⊢ ↑constantCoeff (↑(rename f) (↑C a)) = ↑constantCoeff (↑C a)
case h_C
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (a : R), ↑constantCoeff (↑(rename f) (↑C a)) = ↑constantCoeff (↑C a)
intro a
no goals
case h_C
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ : MvPolynomial σ R
a : R
⊢ ↑constantCoeff (↑(rename f) (↑C a)) = ↑constantCoeff (↑C a)
simp only [constantCoeff_C, rename_C]
case h_add
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
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)
case h_add
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
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)
intro p q hp hq
no goals
case h_add
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
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)
simp only [hp, hq, RingHom.map_add, AlgHom.map_add]
case h_X
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ p : MvPolynomial σ R
n : σ
hp : ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p
⊢ ↑constantCoeff (↑(rename f) (p * X n)) = ↑constantCoeff (p * X n)
case h_X
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p →
      ↑constantCoeff (↑(rename f) (p * X n)) = ↑constantCoeff (p * X n)
intro p n hp
no goals
case h_X
σ : Type u_2
τ✝ : Type ?u.978943
α : Type ?u.978946
R : Type u_3
S : Type ?u.978952
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_1
f : σ → τ
φ p : MvPolynomial σ R
n : σ
hp : ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p
⊢ ↑constantCoeff (↑(rename f) (p * X n)) = ↑constantCoeff (p * X n)
simp only [hp, rename_X, constantCoeff_X, RingHom.map_mul, AlgHom.map_mul]