case h.e'_2.h.e'_5
σ : Type u_2
τ : Type ?u.140744
υ : Type ?u.140747
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
⊢ f = AlgHom.id R (MvPolynomial σ R)
σ : Type u_2
τ : Type ?u.140744
υ : Type ?u.140747
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
⊢ comap f x = x
convert comap_id_apply x
case h.e'_2.h.e'_5.hf
σ : Type u_2
τ : Type ?u.140744
υ : Type ?u.140747
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
φ : σ
⊢ ↑f (X φ) = ↑(AlgHom.id R (MvPolynomial σ R)) (X φ)
case h.e'_2.h.e'_5
σ : Type u_2
τ : Type ?u.140744
υ : Type ?u.140747
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
⊢ f = AlgHom.id R (MvPolynomial σ R)
ext1 φ
no goals
case h.e'_2.h.e'_5.hf
σ : Type u_2
τ : Type ?u.140744
υ : Type ?u.140747
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
φ : σ
⊢ ↑f (X φ) = ↑(AlgHom.id R (MvPolynomial σ R)) (X φ)
simp [hf, AlgHom.id_apply]