case hf
σ : Type u_1
τ : Type ?u.78653
R : Type u_2
S : Type ?u.78659
T : Type ?u.78662
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
i : σ
⊢ ↑(bind₁ X) (X i) = ↑(AlgHom.id R (MvPolynomial σ R)) (X i)
σ : Type u_1
τ : Type ?u.78653
R : Type u_2
S : Type ?u.78659
T : Type ?u.78662
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
⊢ bind₁ X = AlgHom.id R (MvPolynomial σ R)
ext1 i
no goals
case hf
σ : Type u_1
τ : Type ?u.78653
R : Type u_2
S : Type ?u.78659
T : Type ?u.78662
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
i : σ
⊢ ↑(bind₁ X) (X i) = ↑(AlgHom.id R (MvPolynomial σ R)) (X i)
simp