-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_eq_eval_map (g : σ → S₁) (p : MvPolynomial σ R) : p.eval₂ f g = eval g (map f p)

Proof state:
case e_f
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ f = (eval₂Hom (RingHom.id S₁) g).comp (C.comp f)

Tactic:
ext1 a

Result:
case e_f.a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
a : R
⊢ f a = ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) a

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = (eval g) ((map f) p)

Tactic:
unfold map eval

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = (eval₂Hom (RingHom.id S₁) g) ((eval₂Hom (C.comp f) X) p)

Proof state:
case e_f.a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
a : R
⊢ f a = ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) a

Tactic:
simp only [coe_eval₂Hom, RingHom.id_apply, comp_apply, eval₂_C, RingHom.coe_comp]

Result:
no goals

Proof state:
case e_g
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ g = eval₂ (RingHom.id S₁) g ∘ X

Tactic:
ext1 n

Result:
case e_g.h
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
n : σ
⊢ g n = (eval₂ (RingHom.id S₁) g ∘ X) n

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  (eval₂Hom (RingHom.id S₁) g) (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (⇑(eval₂Hom (RingHom.id S₁) g) ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)

Tactic:
dsimp [-eval₂_id] at h

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)

Tactic:
rw [h]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ eval₂ f g p = eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = (eval₂Hom (RingHom.id S₁) g) ((eval₂Hom (C.comp f) X) p)

Tactic:
simp only [coe_eval₂Hom]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ eval₂ f g p = eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p

Tactic:
congr

Result:
case e_f
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ f = (eval₂Hom (RingHom.id S₁) g).comp (C.comp f)

case e_g
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ g = eval₂ (RingHom.id S₁) g ∘ X

Proof state:
case e_g.h
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p
n : σ
⊢ g n = (eval₂ (RingHom.id S₁) g ∘ X) n

Tactic:
simp only [comp_apply, eval₂_X]

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)

Tactic:
have h := eval₂_comp_left (eval₂Hom (RingHom.id S₁) g) (C.comp f) X p

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
h :
  (eval₂Hom (RingHom.id S₁) g) (eval₂ (C.comp f) X p) =
    eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (⇑(eval₂Hom (RingHom.id S₁) g) ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)