case h
σ : Type u_1
τ : Type u_3
υ : Type ?u.158664
R : Type u_2
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
x✝ : σ
⊢ comap (rename f) x x✝ = (x ∘ f) x✝
σ : Type u_1
τ : Type u_3
υ : Type ?u.158664
R : Type u_2
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
⊢ comap (rename f) x = x ∘ f
funext
no goals
case h
σ : Type u_1
τ : Type u_3
υ : Type ?u.158664
R : Type u_2
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
x✝ : σ
⊢ comap (rename f) x x✝ = (x ∘ f) x✝
simp [rename_X, comap_apply, aeval_X]