case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
⊢ ∀ (a : R) (m : σ →₀ ℕ), coeff m (↑(map f) (↑C a)) = ↑f (coeff m (↑C a))

case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m (↑(map f) q) = ↑f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m (↑(map f) (p + q)) = ↑f (coeff m (p + q))

case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m (↑(map f) (p * X n)) = ↑f (coeff m (p * X n))
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
apply MvPolynomial.induction_on p <;> clear p
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ coeff m (↑(map f) (↑C r)) = ↑f (coeff m (↑C r))
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
⊢ ∀ (a : R) (m : σ →₀ ℕ), coeff m (↑(map f) (↑C a)) = ↑f (coeff m (↑C a))
intro r m
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ coeff m (↑C (↑f r)) = ↑f (coeff m (↑C r))
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ coeff m (↑(map f) (↑C r)) = ↑f (coeff m (↑C r))
rw [map_C]
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ (if 0 = m then ↑f r else 0) = ↑f (if 0 = m then r else 0)
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ coeff m (↑C (↑f r)) = ↑f (coeff m (↑C r))
simp only [coeff_C]
case h_C.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
h✝ : 0 = m
⊢ ↑f r = ↑f r

case h_C.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
h✝ : ¬0 = m
⊢ 0 = ↑f 0
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ (if 0 = m then ↑f r else 0) = ↑f (if 0 = m then r else 0)
split_ifs
no goals
case h_C.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
h✝ : ¬0 = m
⊢ 0 = ↑f 0
rw [f.map_zero]
no goals
case h_C.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
r : R
m : σ →₀ ℕ
h✝ : 0 = m
⊢ ↑f r = ↑f r
rfl
case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
p q : MvPolynomial σ R
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
hq : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) q) = ↑f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m (↑(map f) (p + q)) = ↑f (coeff m (p + q))
case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m (↑(map f) q) = ↑f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m (↑(map f) (p + q)) = ↑f (coeff m (p + q))
intro p q hp hq m
case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
p q : MvPolynomial σ R
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
hq : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) q) = ↑f (coeff m q)
m : σ →₀ ℕ
⊢ ↑f (coeff m p) + ↑f (coeff m q) = ↑f (coeff m p + coeff m q)
case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
p q : MvPolynomial σ R
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
hq : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) q) = ↑f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m (↑(map f) (p + q)) = ↑f (coeff m (p + q))
simp only [hp, hq, (map f).map_add, coeff_add]
no goals
case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
p q : MvPolynomial σ R
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
hq : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) q) = ↑f (coeff m q)
m : σ →₀ ℕ
⊢ ↑f (coeff m p) + ↑f (coeff m q) = ↑f (coeff m p + coeff m q)
rw [f.map_add]
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
⊢ coeff m (↑(map f) (p * X i)) = ↑f (coeff m (p * X i))
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m (↑(map f) (p * X n)) = ↑f (coeff m (p * X n))
intro p i hp m
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
⊢ coeff m (↑(map f) p * X i) = ↑f (coeff m (p * X i))
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
⊢ coeff m (↑(map f) (p * X i)) = ↑f (coeff m (p * X i))
simp only [hp, (map f).map_mul, map_X]
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
⊢ (if i ∈ m.support then ↑f (coeff (m - Finsupp.single i 1) p) else 0) =
    ↑f (if i ∈ m.support then coeff (m - Finsupp.single i 1) p else 0)
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
⊢ coeff m (↑(map f) p * X i) = ↑f (coeff m (p * X i))
simp only [hp, mem_support_iff, coeff_mul_X']
case h_X.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
h✝ : i ∈ m.support
⊢ ↑f (coeff (m - Finsupp.single i 1) p) = ↑f (coeff (m - Finsupp.single i 1) p)

case h_X.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
h✝ : ¬i ∈ m.support
⊢ 0 = ↑f 0
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
⊢ (if i ∈ m.support then ↑f (coeff (m - Finsupp.single i 1) p) else 0) =
    ↑f (if i ∈ m.support then coeff (m - Finsupp.single i 1) p else 0)
split_ifs
no goals
case h_X.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
h✝ : ¬i ∈ m.support
⊢ 0 = ↑f 0
rw [f.map_zero]
no goals
case h_X.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
p : MvPolynomial σ R
i : σ
hp : ∀ (m : σ →₀ ℕ), coeff m (↑(map f) p) = ↑f (coeff m p)
m : σ →₀ ℕ
h✝ : i ∈ m.support
⊢ ↑f (coeff (m - Finsupp.single i 1) p) = ↑f (coeff (m - Finsupp.single i 1) p)
rfl