Theorem: MvPolynomial.algHom_eval₂_algebraMap (FormalSnarksProject/ToMathlib/OptionEquivRight.lean)

State before:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (⇑f ∘ a) p
Tactic:
simp only [eval₂, sum_def]
State after:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ f (∑ m ∈ p.support, (algebraMap R A) (coeff m p) * m.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e

State before:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ f (∑ m ∈ p.support, (algebraMap R A) (coeff m p) * m.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
simp only [f.map_sum, f.map_mul, f.map_pow, eq_intCast, map_intCast, AlgHom.commutes]
State after:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ ∑ x ∈ p.support, (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e

State before:
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ ∑ x ∈ p.support, (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
congr
State after:
case e_f
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ (fun x => (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e)) = fun m =>
    (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e

State before:
case e_f
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
⊢ (fun x => (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e)) = fun m =>
    (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
ext x
State after:
case e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    (algebraMap R B) (coeff x p) * x.prod fun n e => (⇑f ∘ a) n ^ e

State before:
case e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    (algebraMap R B) (coeff x p) * x.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
congr
State after:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => (⇑f ∘ a) n ^ e

State before:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => (⇑f ∘ a) n ^ e
Tactic:
simp only [Function.comp_apply]
State after:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => f (a n) ^ e

State before:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => f (a n) ^ e
Tactic:
unfold prod
State after:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (∏ a_1 ∈ x.support, (fun n e => a n ^ e) a_1 (x a_1)) = ∏ a_1 ∈ x.support, (fun n e => f (a n) ^ e) a_1 (x a_1)

State before:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (∏ a_1 ∈ x.support, (fun n e => a n ^ e) a_1 (x a_1)) = ∏ a_1 ∈ x.support, (fun n e => f (a n) ^ e) a_1 (x a_1)
Tactic:
rw [f.map_prod]
State after:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ ∏ x_1 ∈ x.support, f ((fun n e => a n ^ e) x_1 (x x_1)) = ∏ a_1 ∈ x.support, (fun n e => f (a n) ^ e) a_1 (x a_1)

State before:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ ∏ x_1 ∈ x.support, f ((fun n e => a n ^ e) x_1 (x x_1)) = ∏ a_1 ∈ x.support, (fun n e => f (a n) ^ e) a_1 (x a_1)
Tactic:
congr
State after:
case e_f.h.e_a.e_f
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (fun x_1 => f ((fun n e => a n ^ e) x_1 (x x_1))) = fun a_1 => (fun n e => f (a n) ^ e) a_1 (x a_1)

State before:
case e_f.h.e_a.e_f
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (fun x_1 => f ((fun n e => a n ^ e) x_1 (x x_1))) = fun a_1 => (fun n e => f (a n) ^ e) a_1 (x a_1)
Tactic:
ext x1
State after:
case e_f.h.e_a.e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
x1 : σ
⊢ f ((fun n e => a n ^ e) x1 (x x1)) = (fun n e => f (a n) ^ e) x1 (x x1)

State before:
case e_f.h.e_a.e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
x1 : σ
⊢ f ((fun n e => a n ^ e) x1 (x x1)) = (fun n e => f (a n) ^ e) x1 (x x1)
Tactic:
simp
State after:
no goals