case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type ?u.347378
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
φ : σ
⊢ ↑(AlgHom.comp (rename f) (expand p)) (X φ) = ↑(AlgHom.comp (expand p) (rename f)) (X φ)
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type ?u.347378
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
⊢ AlgHom.comp (rename f) (expand p) = AlgHom.comp (expand p) (rename f)
ext1 φ
no goals
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type ?u.347378
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
φ : σ
⊢ ↑(AlgHom.comp (rename f) (expand p)) (X φ) = ↑(AlgHom.comp (expand p) (rename f)) (X φ)
simp only [rename_expand, AlgHom.comp_apply]