-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem coeff_rename_mapDomain (f : σ → τ) (hf : Injective f) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) :
    (rename f φ).coeff (d.mapDomain f) = φ.coeff d

Proof state:
case h2
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (p q : MvPolynomial σ R),
    coeff (Finsupp.mapDomain f d) ((rename f) p) = coeff d p →
      coeff (Finsupp.mapDomain f d) ((rename f) q) = coeff d q →
        coeff (Finsupp.mapDomain f d) ((rename f) (p + q)) = coeff d (p + q)

Tactic:
intros

Result:
case h2
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (Finsupp.mapDomain f d) ((rename f) p✝) = coeff d p✝
a✝ : coeff (Finsupp.mapDomain f d) ((rename f) q✝) = coeff d q✝
⊢ coeff (Finsupp.mapDomain f d) ((rename f) (p✝ + q✝)) = coeff d (p✝ + q✝)

Proof state:
case h1
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d u : σ →₀ ℕ
r : R
⊢ coeff (Finsupp.mapDomain f d) ((rename f) ((monomial u) r)) = coeff d ((monomial u) r)

Tactic:
rw [rename_monomial, coeff_monomial, coeff_monomial]

Result:
case h1
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d u : σ →₀ ℕ
r : R
⊢ (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = if u = d then r else 0

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) ((rename f) φ) = coeff d φ

Tactic:
apply φ.induction_on' (P := fun ψ => coeff (Finsupp.mapDomain f d) ((rename f) ψ) = coeff d ψ)

Result:
case h1
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (u : σ →₀ ℕ) (a : R), coeff (Finsupp.mapDomain f d) ((rename f) ((monomial u) a)) = coeff d ((monomial u) a)

case h2
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (p q : MvPolynomial σ R),
    coeff (Finsupp.mapDomain f d) ((rename f) p) = coeff d p →
      coeff (Finsupp.mapDomain f d) ((rename f) q) = coeff d q →
        coeff (Finsupp.mapDomain f d) ((rename f) (p + q)) = coeff d (p + q)

Proof state:
case h1
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d u : σ →₀ ℕ
r : R
⊢ (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = if u = d then r else 0

Tactic:
simp only [(Finsupp.mapDomain_injective hf).eq_iff]

Result:
no goals

Proof state:
case h2
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (Finsupp.mapDomain f d) ((rename f) p✝) = coeff d p✝
a✝ : coeff (Finsupp.mapDomain f d) ((rename f) q✝) = coeff d q✝
⊢ coeff (Finsupp.mapDomain f d) ((rename f) (p✝ + q✝)) = coeff d (p✝ + q✝)

Tactic:
simp only [*, map_add, coeff_add]

Result:
no goals

Proof state:
case h1
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (u : σ →₀ ℕ) (a : R), coeff (Finsupp.mapDomain f d) ((rename f) ((monomial u) a)) = coeff d ((monomial u) a)

Tactic:
intro u r

Result:
case h1
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d u : σ →₀ ℕ
r : R
⊢ coeff (Finsupp.mapDomain f d) ((rename f) ((monomial u) r)) = coeff d ((monomial u) r)