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

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

case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ ∀ (p : MvPolynomial S₂ R) (n : S₂),
    ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p) →
      ↑(map f) (eval₂ C g (p * X n)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (p * X n))
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p)
apply MvPolynomial.induction_on p
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
r : R
⊢ ↑(map f) (eval₂ C g (↑C r)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (↑C r))
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ ∀ (a : R), ↑(map f) (eval₂ C g (↑C a)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (↑C a))
intro r
no goals
case h_C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
r : R
⊢ ↑(map f) (eval₂ C g (↑C r)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (↑C r))
rw [eval₂_C, map_C, map_C, eval₂_C]
case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝¹ q✝ : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
hp : ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p)
hq : ↑(map f) (eval₂ C g q) = eval₂ C (↑(map f) ∘ g) (↑(map f) q)
⊢ ↑(map f) (eval₂ C g (p + q)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (p + q))
case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ ∀ (p q : MvPolynomial S₂ R),
    ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p) →
      ↑(map f) (eval₂ C g q) = eval₂ C (↑(map f) ∘ g) (↑(map f) q) →
        ↑(map f) (eval₂ C g (p + q)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (p + q))
intro p q hp hq
no goals
case h_add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝¹ q✝ : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
hp : ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p)
hq : ↑(map f) (eval₂ C g q) = eval₂ C (↑(map f) ∘ g) (↑(map f) q)
⊢ ↑(map f) (eval₂ C g (p + q)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (p + q))
rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝¹ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p)
⊢ ↑(map f) (eval₂ C g (p * X s)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (p * X s))
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ ∀ (p : MvPolynomial S₂ R) (n : S₂),
    ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p) →
      ↑(map f) (eval₂ C g (p * X n)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (p * X n))
intro p s hp
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝¹ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p)
⊢ eval₂ C (↑(map f) ∘ g) (↑(map f) p) * ↑(map f) (g s) = eval₂ C (↑(map f) ∘ g) (↑(map f) p) * (↑(map f) ∘ g) s
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝¹ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p)
⊢ ↑(map f) (eval₂ C g (p * X s)) = eval₂ C (↑(map f) ∘ g) (↑(map f) (p * X s))
rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X]
no goals
case h_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.3339071
a a' a₁ a₂ : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝¹ q : MvPolynomial σ R
f✝ f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : ↑(map f) (eval₂ C g p) = eval₂ C (↑(map f) ∘ g) (↑(map f) p)
⊢ eval₂ C (↑(map f) ∘ g) (↑(map f) p) * ↑(map f) (g s) = eval₂ C (↑(map f) ∘ g) (↑(map f) p) * (↑(map f) ∘ g) s
rfl